Data.IFunctor

Documentation

type family Sing :: k -> Type

Singletons are not used here. I am not sure if singletons can generate the instances I need.

Here is an example: Ping-Pong

data PingPong
  = S0 [Bool]
  | S1
  | S2 [Bool]
  | End

data SPingPong :: PingPong -> Type where
  SS0 :: SPingPong (S0 b)
  SS1 :: SPingPong S1
  SS2 :: SPingPong (S2 b)
  SEnd :: SPingPong End

Note here SS0 :: SPingPong (S0 b)

Using singletons will generate SS0 :: Sing b -> SPingPong (S0 b) which is not what I need.

Please note the following example:

serverPeer ::
  (Monad m) => Peer Role PingPong Server m (At () (Done Server)) (S0 s)
serverPeer = I.do
  -- The server is in a state (S0 s) while it is awaiting a message,
  -- and its state is indeterminate until it receives a message.
  -- SS0 :: SPingPong (S0 b) correctly indicates this indeterminacy.
  Recv msg <- await
  case msg of
    Ping -> I.do
      yield Pong
      serverPeer
    Stop -> returnAt ()

class SingI (a :: k) where

example：Ping-Pong

type instance Sing = SPingPong

instance SingI (S0 b) where
  sing = SS0

instance SingI S1 where
  sing = SS1

instance SingI (S2 b) where
  sing = SS2

instance SingI End where
  sing = SEnd

Methods

sing :: Sing a

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 (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

imap :: forall (a :: ps -> Type) (b :: ps -> Type). (a ~> b) -> Peer role' ps r m a ~> Peer role' ps r m b

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

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

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 (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

ireturn :: forall (a :: ps -> Type). a ~> Peer role' ps r m a

ibind :: forall (a :: ps -> Type) (b :: ps -> Type). (a ~> Peer role' ps r m b) -> Peer role' ps r m a ~> Peer role' ps r m b

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

Methods

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

Instances

Functor m => IMonadFail (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

fail :: forall (a :: ps -> Type) (ix :: ps). String -> Peer role' ps r 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

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