Safe Haskell | None |
---|---|
Language | GHC2021 |
Data.IFunctor
Description
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
Synopsis
- type (~>) (f :: k -> Type) (g :: k -> Type) = forall (x :: k). f x -> g x
- class IFunctor (f :: (k -> Type) -> k1 -> Type) where
- class IFunctor m => IMonad (m :: (k -> Type) -> k -> Type) where
- class IMonad m => IMonadFail (m :: (k -> Type) -> k -> Type) where
- data At a (b :: k) (c :: k) where
- (>>=) :: 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
Documentation
class IFunctor m => IMonad (m :: (k -> Type) -> k -> Type) where Source #
(>>=) :: forall x m (a :: x -> Type) (ix :: x) (b :: x -> Type). IMonad m => m a ix -> (a ~> m b) -> m b ix Source #