module MonadF
(
    FixF,
    MonadF(unit, bind),
    PseudounitF(pseudounit),
    PseudobindF(pseudobind),
    IdMonadF(IdMonadF),
    Amp(Amp),
    (<<>>), (<<#>>)
)
where

import Isomorphism

infixl 1 <<>>, <<#>>

-- Figure 1: Haskell code for supporting pseudomonads

-- In Steele's paper, pseudomonad type constructors such as TermN
-- take not one argument but two (in other words, TermN is of kind
-- *->*->*, not *->*).  The additional argument "t''" to TermN is
-- the top-level term type Term; it is provided to TermN as a type
-- argument so that terms such as Add can contain subterms located
-- anywhere in the term type tower.  This additional argument is
-- one of the many things that caused Steele trouble with the Haskell
-- type system, as he describes in section 8 of his paper ("Recursive
-- Types in Haskell").

-- FixF takes a type constructor "f", of kind *->*->*, and produces
-- the fixpoint type of "f" in its first argument.  In other words,
-- FixF(f)(a) = FIX(x)[f(x)(a)].  Our FixF has kind (*->*->*)->*->*,
-- unlike the standard fixpoint type constructor, which has kind
-- (*->*)->*.

newtype FixF f a = FixF (f (FixF f a) a)

instance Wrap (f (FixF f a) a) (FixF f a) where
    wiso          = FixF
    wosi (FixF x) = x

-- Our code below defines the type classes MonadF, PseudounitF and
-- PseudobindF to accommodate this additional argument.  Essentially,
-- the type class "MonadF m" means that "m u" is a monad for any type
-- "u".  The type class "PseudounitF p" means that "p" is something
-- that supports pseudounit; the type class "PseudobindF m p" means
-- that "p" supports pseudobind with respect to the monad "m".

-- The reason we need separate type classes for pseudounit and
-- pseudobind is that Steele's "continuation pseudomonad" (figure 15)
-- only supports pseudobind with respect to the identity monad.  For
-- the same reason, we need "PseudobindF" to be a multi-parameter type
-- class.  Multi-parameter type classes are not part of the Haskell 98
-- standard.  Oh well.

class MonadF m where
    unit :: a -> m u a
    bind :: m u a -> (a -> m u a) -> m u a
    -- Note that "bind" is not
    --          m u a -> (a -> m u b) -> m u b
    -- Steele unified a and b in his definition of bind, and so do we.
    -- The unification is necessary due to the definition of ValueCBV
    -- (figure 12; module CBV; file CBV.hs) -- note how the type variable
    -- v creeps contravariantly into Fun.

(<<>>) :: (MonadF m) => m u a -> (a -> m u a) -> m u a
(<<>>) = bind

newtype IdMonadF u a = IdMonadF a
instance MonadF IdMonadF where
    unit       = IdMonadF
    bind m_ k_ = IdMonadF $ let IdMonadF m = m_
                                k a = let IdMonadF ka = k_ a in ka
                            in k m

instance Wrap a (IdMonadF u a) where
    wiso              = IdMonadF
    wosi (IdMonadF x) = x

class PseudounitF p where
    pseudounit :: a -> p u a

class (MonadF m, PseudounitF p) => PseudobindF m p where
    pseudobind :: p u a -> (a -> m u (p u a)) -> m u (p u a)

(<<#>>) :: (PseudobindF m p) => p u a -> (a -> m u (p u a)) -> m u (p u a)
(<<#>>) = pseudobind

-- We now define the composition of a monad with a pseudomonad.
-- This operation corresponds to the & operator in Steele's paper.

newtype (MonadF m, PseudobindF m p) => Amp m p u a = Amp (m u (p u a))

instance (MonadF m, PseudobindF m p) => MonadF (Amp m p) where
    unit       = Amp . unit . pseudounit
    bind z_ k_ = Amp $ let Amp z = z_
                           k a   = let Amp ka = k_ a in ka
                       in z <<>> (\w -> w <<#>> k)

-- In composing a monad with a pseudomonad, we introduce a newtype
-- value constructor "Amp"; the type "Amp m p u a" is isomorphic to,
-- but not identical to, the type "m u (p u a)".

instance (MonadF m, PseudobindF m p) => Wrap (m u (p u a)) (Amp m p u a) where
    wiso         = Amp
    wosi (Amp x) = x