{-# LANGUAGE TypeOperators, LambdaCase, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, DeriveFunctor, StandaloneDeriving, DeriveAnyClass, Safe #-}
-- | This *is* monad coproducts (due to Luth and Ghani) unlike the other thing.
module Control.Monad.Coproducts3 (module Control.Monad.EtaInverse, module Control.Monad.Free.Class, module Data.Functor.Sum, Free'(..), toF2, execCoproduct) where
-- import Control.Compose
import Data.Functor.Sum
import Control.Monad
import Control.Monad.Free
import Control.Monad.Free.Class
import Data.Functor.Classes
import Data.Maybe
import Control.Monad.EtaInverse

-- | A modified free monad giving efficient access to the topmost layer;
-- but otherwise using the machinery of the free monad 'f2'.
data Free' f f2 t = Free' { unFree' :: f(f2 t) }
	| Pure' t deriving Functor

--
--
--
--
--
--
--
--
--
--
--
--

instance (Functor f, MonadFree f f2) => Monad(Free' f f2) where
	return = Pure'
	Pure' x >>= f = f x
	Free' f>>= f2 = Free'((\x->x>>= \x -> case f2 x of
		Free' x2 -> wrap x2
		Pure' x2-> return x2) <$> f)

instance (Functor f, MonadFree f f2) => Applicative(Free' f f2) where
	pure = return
	(<*>) = ap

-- | A projection into the underlying free monad construction.
toF2 (Free' x) = wrap x
toF2 (Pure' x) = return x

instance (Functor f, MonadFree f f2) => MonadFree f(Free' f f2) where
	-- It wraps the topmost layer contained in the layer of 'f',
	-- then re-wraps, making the layer of 'f' the topmost layer.
	wrap x = Free'$ toF2 <$> x

deriving instance (Show1 f, Show1 f2) => Show1(Free' f f2)

deriving instance (Show(f(f2 t)), Show(f2 t), Show t) => Show(Free' f f2 t)

--
--
--
--
--
--
--
--
--
--
--
--

----------------------------------------

-- This comes from the defining map of a coproduct for layer types f and f2
-- which correspond to layer types T and R in the paper;
-- with the substitution made Q := Free'(Sum f f2) f3 for a free monad
-- f3. It can be seen that this is the map (T+R) Q -> Q,
-- which by costrength is equivalent to the two defining maps
-- of a coproduct TQ -> Q and RQ -> Q. Checking that the diagram
-- commutes is an exercise.
execCoproduct_ ::  (EtaInverse f, EtaInverse f2, MonadFree(Sum f f2) f3)=>
	Sum f f2(Free'(Sum f f2) f3 t) -> Free'(Sum f f2) f3 t
execCoproduct_ = \ case

	-- These lines implement removal of layers that are in the range
	-- of 'eta'; in the paper these are referred to as variable layers.
	-- This is point one on Luth and Ghani's three point checklist.
	InL f | isJust(etaInv f) -> fromJust(etaInv f)

	InR f | isJust(etaInv f) -> fromJust(etaInv f)

	InL f -> Free'$InL$ f >>= \ case
		-- Nested layers of InL are "squashed together"; the same occurs
		-- for InR layers (this is point two).
		Free'(InL x) -> x

		Free' (InR x2) | isJust(etaInv x2) -> return$!fromJust(etaInv x2)
		Free' x@(InR _) -> return$!wrap x
		Pure' x -> return$!return x

	InR f -> Free'$InR$ f >>= \ case
		Free'(InR x) -> x
		Free' (InL x2) | isJust(etaInv x2) -> return$!fromJust(etaInv x2)
		Free' x@(InL _) -> return$!wrap x
		Pure' x -> return$!return x
--
--
--
--
--
--
--
--
--
--
--
--


-- Point three happens "for free"; when multiple free monad constructions are
-- represented nested, and normalized using execCoproduct, I end up finding
-- that the free construction also has a usable notion of 'EtaInverse', and this
-- implements the required normalizing. Although I have to put up with three layers
-- in T1, T2, and T3 being represented in constructors InL.InL, InR.InL, InR.

--
-- | Given a free construction construct a representation of the monad coproduct
-- in a free mona; it picks out one representative element of each equivalence
-- class in the defining quotient of the monad coproduct.
execCoproduct :: (EtaInverse f, EtaInverse f2, MonadFree(Sum f f2) f3)=>
	Free(Sum f f2) t -> Free'(Sum f f2) f3 t
execCoproduct = iter execCoproduct_.(return<$>)