(Note, this requires a more sophisticated type theory such as System Fω to encode)
This idea is captured by the concept of an indexed monad (and in turn indexed applicative/functor).
Using Haskell as lingua franca, we talk about a typeclass:
class IxMonad (m :: n -> n -> * -> *) where
ireturn :: a -> m i i a
ibind :: m i j a -> (a -> m j k b) -> m i k b
{- alternatively, if it's an IxFunctor, the categorical version:
ireturn :: a -> m i i a
ijoin :: m i j (m j k a) -> m i k a
-}
An action m i j a
makes a connection "from" an index i
"to" an index j
, and wraps some type a
. Actions can be composed only if the respective indices "line up". Sort of like how horizontal oidification turns a monoid into a category: morphisms can be composed only if their endpoint objects "line up".
Analogous definitions of an indexed functor and an indexed applicative can be made:
class IxFunctor (m :: n -> n -> * -> *) where
ifmap :: (a -> b) -> m i j a -> m i j b
class IxApplicative (m :: n -> n -> * -> *) where
ipure :: a -> m i i a
iap :: m i j (a -> b) -> m j k a -> m i k b
{- alternatively, if it's an IxFunctor, the categorical version:
iunit :: () -> m i i ()
iprod :: (m i j a, m j k b) -> m i k (a, b)
-}
Say we wanted to "output" entries of some type, while keeping a type-theoretic witness of how many entries there are, we could define an indexed writer monad.
Here's definitions of natural numbers used to track length, and a length-indexed "log" datatype:
data N = Z | S N
data Vec (n :: N) (a :: *) where
Nil :: Vec 'Z a
Cons :: a -> Vec n a -> Vec ('S n) a
In an indexed monad, the usual intuition is that the indices i
/j
describe the "state" of the system: an action brings the system from "state i
" to "state j
". Here we'll be using the index to track how many entries we've written to the "log", and for completely technical reasons (to do with making the typechecker happy in an easy way), the left index will be the output log length, and the right index will be the input log length:
type family Add (n :: N) (m :: N) :: N where
Add 'Z m = m
Add ('S n) m = 'S (Add n m)
data IxWriter w i j a where
IxWriter :: Vec k w -> a -> IxWriter w (Add k i) i a
instance IxMonad (IxWriter w) where
ireturn x = IxWriter Nil x
ibind (IxWriter xs x) f = case f x of
IxWriter fs y -> iwappend xs fs y
where
iwcons :: w -> IxWriter w i j a -> IxWriter w ('S i) j a
iwcons p (IxWriter qs z) = IxWriter (Cons p qs) z
iwappend :: Vec k1 w -> Vec k2 w -> a -> IxWriter w (Add k1 (Add k2 i)) i a
iwappend (Cons p ps) qs z = iwcons p $ iwappend ps qs z
iwappend Nil qs z = IxWriter qs z
Then we can define the "logging" action, and an interpreter for our effect:
itell :: Vec k w -> IxWriter w (Add k i) i ()
itell ps = IxWriter ps ()
runIxWriter :: IxWriter w i 'Z a -> (Vec i w, a)
runIxWriter (IxWriter Nil x) = (Nil, x)
runIxWriter (IxWriter (Cons p ps) x) = case runIxWriter (IxWriter ps x) of
(qs, r) -> (Cons p qs, r)
With this we can keep track of exactly how many entries we've logged:
case runIxWriter $
itell (Cons 1 Nil) `ibind` \_ -> itell (Cons 2 Nil) `ibind` \_ -> itell (Cons 3 Nil)
of (Cons a (Cons b (Cons c Nil)), x) -> (a, b, c, x)
{- pattern match is valid and complete because we
statically know it's a Vec ('S ('S ('S 'Z))) Integer -}
Here we used the graded monoid of finite sequences (and thus all our logs are of the same type). In theory we could have used any monoid graded by any other monoid, (for example the monoid of heterogeneous lists, graded by the monoid of lists of types -- if we wanted to be able to talk about heterogeneous tuples)