To motivate this question, let's first recall a bog-standard Hoare-Dijkstra-style indexed monad, and the example instance of an indexed writer monad.
For an indexed monad, we just require type alignment on (i)binds:
class IMonadHoare m where
ireturn :: a -> m i i a
ibind :: m i j a -> (a -> m j k b) -> m i k b
and then just to show that this is usable, let's implement an indexed writer monad:
import Prelude hiding (id, (.))
import Control.Category
newtype IWriter cat i j a = IWriter{ runIWriter :: (a, cat i j) }
instance (Category cat) => IMonadHoare (IWriter cat) where
ireturn x = IWriter (x, id)
ibind (IWriter (x, f)) k = IWriter $
let (y, g) = runIWriter (k x)
in (y, g . f)
And it really is a writer-like monad, since we can implement the usual methods:
itell :: (Category cat) => cat i j -> IWriter cat i j ()
itell f = IWriter ((), f)
ilisten :: (Category cat) => IWriter cat i j a -> IWriter cat i j (a, cat i j)
ilisten w = IWriter $
let (x, f) = runIWriter w
in ((x, f), f)
ipass :: (Category cat) => IWriter cat i j (a, cat i j -> cat i j) -> IWriter cat i j a
ipass w = IWriter $
let ((x, censor), f) = runIWriter w
in (x, censor f)
OK, so far so good. But now I'd like to generalize this to other kinds (heh) of indices. I thought it would work to simply add associated type families for the type-level monoid operations, like so:
{-# LANGUAGE TypeFamilies, PolyKinds, MultiParamTypeClasses, FunctionalDependencies #-}
import Data.Kind
class IMonadTF idx (m :: idx -> Type -> Type) | m -> idx where
type Empty m :: idx
type Append m (i :: idx) (j :: idx) :: idx
ireturn :: a -> m (Empty m) a
ibind :: m i a -> (a -> m j b) -> m (Append m i j) b
So, does this work? Well, you can use it to define something where Empty/Append is non-indexed, like so:
{-# LANGUAGE DataKinds, TypeOperators #-}
import GHC.TypeLists
newtype Counter (n :: Nat) a = Counter{ runCounter :: a }
instance IMonadTF Nat Counter where
type Empty Counter = 0
type Append Counter n m = n + m
ireturn = Counter
ibind (Counter x) k = Counter . runCounter $ k x
tick :: Counter 1 ()
tick = Counter ()
But now can we recreate our IWriter example? Unfortunately, I haven't been able to.
First of all, we can't even declare Empty:
data IWriter cat (ij :: (Type, Type)) a where
IWriter :: { runIWriter :: (a, cat i j) } -> IWriter cat '(i, j) a
instance (Category cat) => IMonadTF (Type, Type) (IWriter cat) where
type Empty (IWriter cat) = '(i, i)
This, of course, fails because the type variable i is not in scope.
Let's change Empty into a Constraint instead, and recreate the Counter instance just to validate it:
class IMonadConstraint idx (m :: idx -> Type -> Type) | m -> idx where
type IsEmpty m (i :: idx) :: Constraint
type Append m (i :: idx) (j :: idx) :: idx
ireturn :: (IsEmpty m i) => a -> m i a
ibind :: m i a -> (a -> m j b) -> m (Append m i j) b
newtype Counter (n :: Nat) a = Counter{ runCounter :: a }
instance IMonadConstraint Nat Counter where
type IsEmpty Counter n = n ~ 0
type Append Counter n m = n + m
ireturn = Counter
ibind (Counter x) k = Counter . runCounter $ k x
tick :: Counter 1 ()
tick = Counter ()
Now we can at least write down the definition of IsEmpty (Writer cat), but in the code below, ireturn still doesn't typecheck. It is as if the defintion of IsEmpty isn't used to solve constraints:
instance (Category cat) => IMonadConstraint (Type, Type) (IWriter cat) where
type IsEmpty (IWriter cat) '(i, j) = i ~ j
ireturn x = IWriter (x, id)
Could not deduce
i ~ '(j0, j0)from the contextIsEmpty (IWriter cat) i
Similarly, we can try to enforce the alignment in the middle by adding a constraint for appending:
class IMonadConstraint2 idx (m :: idx -> Type -> Type) | m -> idx where
type IsAppend m (i :: idx) (j :: idx) :: Constraint
type Append m (i :: idx) (j :: idx) :: idx
ireturn :: (IsEmpty m i) => a -> m i a ibind :: (IsAppend m i j) => m i a -> (a -> m j b) -> m (Append m i j) b
But then that fails for IWriter in a similar way:
instance (Category cat) => IMonadConstraint2 (Type, Type) (IWriter cat) where
type IsAppend (IWriter cat) '(i, j) '(j', k) = j ~ j'
type Append (IWriter cat) '(i, j) '(j', k) = '(i, k)
ibind (IWriter (x, w)) k = IWriter $
let (y, w') = runIWriter (k x)
in (y, w' . w)
Could not deduce
j ~ '(j1, j0)from the contextIsAppend (IWriter cat) i j
Is it because IsEmpty and IsAppend defined "pointwise"?
IMonadclasses you propose different names, so we can properly discuss them. – Impartial