Data.IFunctor

Introducing McBride Indexed Monads

Here's Edward Kmett's introduction to Indexed Monads.

As he said, there are at least three indexed monads:

• Bob Atkey

class IMonad m where
  ireturn  ::  a -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

• Conor McBride

type a ~> b = forall i. a i -> b i

class IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b) -> (m a ~> m b)

• Dominic Orchard

No detailed description, just a link to this lecture。

I use the McBride Indexed Monad, the earliest paper here.

The following is my understanding of (~>): through GADT, let the value contain type information, and then use ((~>), pattern match) to pass the type to subsequent functions

data V = A | B

data SV :: V -> Type where  -- GADT, let the value contain type information
   SA :: SV A
   SB :: SV B

data SV1 :: V -> Type where
   SA1 :: SV1 A
   SB1 :: SV1 B

fun :: SV ~> SV1     -- type f ~> g = forall x. f x -> g x
fun sv = case sv of  -- x is arbitrary but f, g must have the same x
     SA -> SA1       -- Pass concrete type state to subsequent functions via pattern matching
     SB -> SB1


class (IFunctor m) => IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b)  -- The type information contained in a will be passed to (m b),
                       -- which is exactly what we need: external input has an impact on the type!
        -> m a ~> m b

Documentation

type (~>) (f :: k -> Type) (g :: k -> Type) = forall (x :: k). f x -> g x infixr 0

class IFunctor (f :: (k -> Type) -> k1 -> Type) where

Methods

imap :: forall (a :: k -> Type) (b :: k -> Type). (a ~> b) -> f a ~> f b

Instances

Functor m => IFunctor (Operate m :: (k1 -> Type) -> k1 -> Type)

Defined in TypedFsm.Core

Methods

imap :: forall (a :: k1 -> Type) (b :: k1 -> Type). (a ~> b) -> Operate m a ~> Operate m b

class IFunctor m => IMonad (m :: (k -> Type) -> k -> Type) where

Methods

ireturn :: forall (a :: k -> Type). a ~> m a

ibind :: forall (a :: k -> Type) (b :: k -> Type). (a ~> m b) -> m a ~> m b

Instances

Functor m => IMonad (Operate m :: (k -> Type) -> k -> Type)

Defined in TypedFsm.Core

Methods

ireturn :: forall (a :: k -> Type). a ~> Operate m a

ibind :: forall (a :: k -> Type) (b :: k -> Type). (a ~> Operate m b) -> Operate m a ~> Operate m b

class IMonad m => IMonadFail (m :: (k -> Type) -> k -> Type) where

Methods

fail :: forall (a :: k -> Type) (ix :: k). String -> m a ix

data At a (b :: k) (c :: k) where

Constructors

At :: forall {k} a (b :: k). a -> At a b b

(>>=) :: forall x m (a :: x -> Type) (ix :: x) (b :: x -> Type). IMonad m => m a ix -> (a ~> m b) -> m b ix

(>>) :: forall x m a (j :: x) (i :: x) (b :: x -> Type). IMonad m => m (At a j) i -> m b j -> m b i

(>>)

Note: (>>) can only be used if the type of left m is `m (At a j) i`.

returnAt :: forall {k1} m a (k2 :: k1). IMonad m => a -> m (At a k2) k2