Working out the details of a type indexed free monad

Question

I've been using a free monad to build a DSL. As part of the language, there is an input command, the goal is to reflect what types are expected by the input primitive at the type level for additional safety.

For example, I want to be able to write the following program.

concat :: Action '[String, String] ()
concat = do
  (x :: String) <- input
  (y :: String) <- input 
  output $ x ++ " " ++ y

Along with an evaluation function

eval :: Action params res -> HList params -> [String]
eval = ...

Which works in the following way..

> eval concat ("a" `HCons` "b" `HCons` HNil)
["a b"]

Here's what I have so far.

data HList i where
  HNil :: HList '[]
  HCons :: h -> HList t -> HList (h ': t)

type family Append (a :: [k]) (b :: [k]) :: [k] where
  Append ('[]) l = l
  Append (e ': l) l' = e ': (Append l l')

data ActionF next where
   Input :: (a -> next) ->  ActionF next
   Output :: String -> next -> ActionF next

instance Functor ActionF where
  fmap f (Input c) = Input (fmap f c)
  fmap f (Output s n) = Output s (f n)

data FreeIx f i a where
  Return :: a -> FreeIx f '[] a
  Free :: f (FreeIx f i a) -> FreeIx f i a

type Action i a = FreeIx ActionF i a

liftF :: Functor f => f a -> FreeIx f i a
liftF = Free . fmap Return

input :: forall a . Action '[a] a
input = liftF (Input id)

output :: String -> Action '[] ()
output s = liftF (Output s ())

bind :: Functor f => FreeIx f t a -> (a -> FreeIx f v b) -> FreeIx f (Append t v) b
bind (Return a) f = f a
bind (Free x) f   = Free (fmap (flip bind f) x)

The problem is that liftF does not type check.

liftF :: Functor f => Proxy i -> f a -> FreeIx f i a
liftF p = Free . fmap Return

Is this the correct approach?

I thought some inspiration might come from the effect monad package. This is what led to the definition of Return and Free.

For some more backstory: I've seen in several places that users will define DSLs in this way and then define an evaluation function eval :: Action a -> [String] -> a or something similar. The clear problem with this approach is that all arguments must have the same type and there is no static guarantee that the correct number of arguments will be supplied. This is an attempt to solve this problem.

Answer 1

I have found a satisfactory solution to this problem. Here's a sneak peek at the ultimate result:

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

eval (1 ::: 2 ::: HNil) addTwo = ["3"]

Accomplishing this requires a large number of steps. First, we need to observe that the ActionF data type is itself indexed. We will adapt FreeIx to build an indexed monad using the free monoid, lists. The Free constructor for FreeIx will need to capture a witness to the finiteness of one of its two indexes for use in proofs. We will use a system due to András Kovács for writing proofs about appending type level lists to make proofs of both associativity and the right identity. We will describe indexed monads in the same manner as Oleg Grenrus. We will use the RebindbableSyntax extension to write expressions for an IxMonad using the ordinary do notation.

Prologue

In addition to all of the extensions your example already requires and RebindbableSyntax which was mentioned above we will also need UndecidableInstances for the trivial purpose of reusing a type family definition.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RebindableSyntax #-}

We will be using the :~: GADT from Data.Type.Equality to manipulate type equality.

import Data.Type.Equality
import Data.Proxy

Because we will be rebinding the Monad syntax, we'll hide all of Monad from the Prelude import. The RebindableSyntax extension uses for do notation whatever functions >>=, >>, and fail are in scope.

import Prelude hiding (Monad, (>>=), (>>), fail, return)

We also have a few bits of new general-purpose library code. I have given the HList an infix constructor, :::.

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)

infixr 5 :::

I have renamed the Append type family ++ to mirror the ++ operator on lists.

type family (++) (a :: [k]) (b :: [k]) :: [k] where
  '[]      ++ l  = l
  (e ': l) ++ l' = e ': l ++ l'

It's useful to talk about constraints of the form forall i. Functor (f i). These don't exist in Haskell outside GADTs that capture constraints like the Dict GADT in constraints. For our purposes, it will be sufficient to define a version of Functor with an extra ignored argument.

class Functor1 (f :: k -> * -> *) where
    fmap1 :: (a -> b) -> f i a -> f i b

Indexed ActionF

The ActionF Functor was missing something, it had no way to capture type level information about the requirements of the methods. We'll add an additional index type i to capture this. Input requires a single type, '[a], while Output requires no types, '[]. We are going to call this new type parameter the index of the functor.

data ActionF i next where
   Input :: (a -> next) ->  ActionF '[a] next
   Output :: String -> next -> ActionF '[] next 

We'll write Functor and Functor1 instances for ActionF.

instance Functor (ActionF i) where
  fmap f (Input c) = Input (fmap f c)
  fmap f (Output s n) = Output s (f n)

instance Functor1 ActionF where
  fmap1 f = fmap f

FreeIx Reconstructed

We are going to make two changes to FreeIx. We will change how the indexes are constructed. The Free constructor will refer to the index from the underlying functor, and produce a FreeIx with an index that's the free monoidal sum (++) of the index from the underlying functor and the index from the wrapped FreeIx. We will also require that Free captures a witness to a proof that the index of the underlying functor is finite.

data FreeIx f (i :: [k]) a where
  Return :: a -> FreeIx f '[] a
  Free :: (WitnessList i) => f i (FreeIx f j a) -> FreeIx f (i ++ j) a

We can define Functor and Functor1 instances for FreeIx.

instance (Functor1 f) => Functor (FreeIx f i) where
  fmap f (Return a) = Return (f a)
  fmap f (Free x) = Free (fmap1 (fmap f) x)

instance (Functor1 f) => Functor1 (FreeIx f) where
  fmap1 f = fmap f

If we want to use FreeIx with an ordinary, unindexed functor, we can lift those values to an unconstrained indexed functor, IxIdentityT. This isn't needed for this answer.

data IxIdentityT f i a = IxIdentityT {runIxIdentityT :: f a}

instance Functor f => Functor (IxIdentityT f i) where
    fmap f = IxIdentityT . fmap f . runIxIdentityT

instance Functor f => Functor1 (IxIdentityT f) where
    fmap1 f = fmap f

Proofs

We will need to prove two properties about appending type level lists. In order to write liftF we will need to prove the right identity xs ++ '[] ~ xs. We'll call this proof appRightId for append right identity. In order to write bind we will need to prove associativity xs ++ (yz ++ zs) ~ (xs ++ ys) ++ zs, which we will call appAssoc.

The proofs are written in terms of a successor list which is essentially a list of proxies, one for each type type SList xs ~ HFMap Proxy (HList xs).

data SList (i :: [k]) where
  SNil :: SList '[]
  SSucc :: SList t -> SList (h ': t)

The following proof of associativity along with the method of writing this proof are due to András Kovács. By only using SList for the type list of xs we deconstruct and using Proxys for the other type lists, we can delay (possibly indefinitely) needing WitnessList instances for ys and zs.

appAssoc ::
  SList xs -> Proxy ys -> Proxy zs ->
  (xs ++ (ys ++ zs)) :~: ((xs ++ ys) ++ zs)
appAssoc SNil ys zs = Refl
appAssoc (SSucc xs) ys zs =
  case appAssoc xs ys zs of Refl -> Refl

Refl, the constructor for :~:, can only be constructed when the compiler is in possession of a proof that the two types are equal. Pattern matching on Refl introduces the proof of type equality into the current scope.

We can prove the right identity in a similar fashion

appRightId :: SList xs -> xs :~: (xs ++ '[])
appRightId SNil = Refl
appRightId (SSucc xs) = case appRightId xs of Refl -> Refl

To use these proofs we construct witness lists for the the class of finite type lists.

class WitnessList (xs :: [k]) where
  witness :: SList xs

instance WitnessList '[] where
  witness = SNil

instance WitnessList xs => WitnessList (x ': xs) where
  witness = SSucc witness

Lifting

Equipped with appRightId we can define lifting values from the underlying functor into FreeIx.

liftF :: forall f i a . (WitnessList i, Functor1 f) => f i a -> FreeIx f i a
liftF = case appRightId (witness :: SList i) of Refl -> Free . fmap1 Return

The explicit forall is for ScopedTypeVariables. The witness to the finiteness of the index, WitnessList i, is required by both the Free constructor and appRightId. The proof of appRightId is used to convince the compiler that the FreeIx f (i ++ '[]) a constructed is of the same type as FreeIx f i a. That '[] came from the Return that was wrapped in the underlying functor.

Our two commands, input and output, are written in terms of liftF.

type Action i a = FreeIx ActionF i a

input :: Action '[a] a
input = liftF (Input id)

output :: String -> Action '[] ()
output s = liftF (Output s ())

IxMonad and Binding

To use RebindableSyntax we'll define an IxMonad class with the same function names (>>=), (>>), and fail as Monad but different types. This class is described in Oleg Grenrus's answer.

class Functor1 m => IxMonad (m :: k -> * -> *) where
    type Unit :: k
    type Plus (i :: k) (j :: k) :: k

    return :: a -> m Unit a
    (>>=) :: m i a -> (a -> m j b) -> m (Plus i j) b

    (>>) :: m i a -> m j b -> m (Plus i j) b
    a >> b = a >>= const b

    fail :: String -> m i a
    fail s = error s

Implementing bind for FreeIx requires the proof of associativity, appAssoc. The only WitnessList instance in scope, WitnessList i, is the one captured by the deconstructed Free constructor. Once again, the explicit forall is for ScopedTypeVariables.

bind :: forall f i j a b. (Functor1 f) => FreeIx f i a -> (a -> FreeIx f j b) -> FreeIx f (i ++ j) b
bind (Return a) f = f a
bind (Free (x :: f i1 (FreeIx f j1 a))) f =
    case appAssoc (witness :: SList i1) (Proxy :: Proxy j1) (Proxy :: Proxy j)
    of Refl -> Free (fmap1 (`bind` f) x)

bind is the only interesting part of the IxMonad instance for FreeIx.

instance (Functor1 f) => IxMonad (FreeIx f) where
    type Unit = '[]
    type Plus i j = i ++ j

    return = Return
    (>>=) = bind

We're done

All of the hard part is done. We can write a simple interpreter for Action xs () in the most straight forward fashion. The only trick required is to avoid pattern matching on the HList constructor ::: until after the type list i is known to be non-empty because we already matched on Input.

eval :: HList i -> Action i () -> [String]
eval inputs action = 
    case action of 
        Return () -> []
        Free (Input f) -> 
            case inputs of
                (x ::: xs) -> eval xs (f x)
        Free (Output s next) -> s : eval inputs next

If you are curious about the inferred type of addTwo

addTwo = do
  (x :: Int) <- input
  (y :: Int) <- input 
  output $ show (x + y)

it is

> :t addTwo
addTwo :: FreeIx ActionF '[Int, Int] ()

Answer 2

I have a new solution that is simple and quite generally applicable.

So far in the thread we've used monads indexed by a monoid, but here I rely on the other popular notion of an indexed monad, the one that has typestate transitions (Hoare logic-style):

    return :: a -> m i i a
    (>>=) :: m i j a -> (a -> m j k b) -> m i k b

I believe the two approaches are equivalent (at least in theory), since we get the Hoare monad by indexing with the endomorphism monoid, and we can also go in the opposite direction by CPS encoding the monoidal appends in the state transitions. In practice, Haskell's type-level and kind-level language is rather weak, so moving back-and-forth between the two representations is not an option.

There is a problem though with the above type for >>=: it implies that we must compute the typestate in a top-down order, i. e. it forces the following definition for IxFree:

data IxFree f i j a where
  Pure :: a -> IxFree f i i a
  Free :: f i j (IxFree f j k a) -> IxFree f i k a

So, if we have a Free exp expression, then we first transition from i to j following the constructor of exp, and then get from j to k by checking the subexperssions of exp. This means that if we try to accumulate the input types in a list, we end up with a reversed list:

-- compute transitions top-down
test = do
  (x :: Int) <- input       -- prepend Int to typestate
  (y :: String) <- input    -- prepend String to typestate
  return ()                 -- do nothing         

If we instead appended the types to the end of the list, the order would be right. But making that work in Haskell (especially making eval work) would require a gruelling amount of proof-writing, if it's even possible.

Let's compute the typestate bottom-up instead. It makes all kinds of computations where we build up some data structure depending on the syntax tree much more natural, and in particular it makes our job very easy here.

{-# LANGUAGE
    RebindableSyntax, DataKinds,
    GADTs, TypeFamilies, TypeOperators,
    PolyKinds, StandaloneDeriving, DeriveFunctor #-}

import Prelude hiding (Monad(..))

class IxFunctor (f :: ix -> ix -> * -> *) where
    imap :: (a -> b) -> f i j a -> f i j b

class IxFunctor m => IxMonad (m :: ix -> ix -> * -> *) where
    return :: a -> m i i a
    (>>=) :: m j k a -> (a -> m i j b) -> m i k b -- note the change of index orders

    (>>) :: m j k a -> m i j b -> m i k b -- here too
    a >> b = a >>= const b

    fail :: String -> m i j a
    fail = error

data IxFree f i j a where
  Pure :: a -> IxFree f i i a
  Free :: f j k (IxFree f i j a) -> IxFree f i k a -- compute bottom-up

instance IxFunctor f => Functor (IxFree f i j) where
  fmap f (Pure a)  = Pure (f a)
  fmap f (Free fa) = Free (imap (fmap f) fa)

instance IxFunctor f => IxFunctor (IxFree f) where
  imap = fmap

instance IxFunctor f => IxMonad (IxFree f) where
  return = Pure
  Pure a  >>= f = f a
  Free fa >>= f = Free (imap (>>= f) fa)

liftf :: IxFunctor f => f i j a -> IxFree f i j a
liftf = Free . imap Pure

Now implementing Action becomes simple.

data ActionF i j next where
  Input  :: (a -> next) -> ActionF i (a ': i) next
  Output :: String -> next -> ActionF i i next

deriving instance Functor (ActionF i j)                                      
instance IxFunctor ActionF where
  imap = fmap

type family (++) xs ys where -- I use (++) here only for the type synonyms
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type Action' xs rest = IxFree ActionF rest (xs ++ rest)
type Action xs a = forall rest. IxFree ActionF rest (xs ++ rest) a  

input :: Action '[a] a
input = liftf (Input id)

output :: String -> Action '[] ()
output s = liftf (Output s ())

data HList i where
  HNil :: HList '[]
  (:::) :: h -> HList t -> HList (h ': t)
infixr 5 :::

eval :: Action' xs r a -> HList xs -> [String]
eval (Pure a)              xs         = []
eval (Free (Input k))      (x ::: xs) = eval (k x) xs
eval (Free (Output s nxt)) xs         = s : eval nxt xs

addTwice :: Action [Int, Int] ()
addTwice = do
  x <- input
  y <- input
  output (show $ x + y)

To make things less confusing for users, I introduced type synonyms with friendlier index schemes: Action' xs rest a means that the action reads from xs and may be followed by actions containing rest reads. Action is a type synonym equivalent to the one appearing in the thread question.

We can implement a variety of DSL-s with this approach. The reversed typing order gives it a bit of a spin, but we can do the usual indexed monads all the same. Here's the indexed state monad, for example:

data IxStateF i j next where
  Put :: j -> next -> IxStateF j i next
  Get :: (i -> next) -> IxStateF i i next

deriving instance Functor (IxStateF i j)
instance IxFunctor IxStateF where imap = fmap

put s = liftf (Put s ())
get   = liftf (Get id)

type IxState i j = IxFree IxStateF j i

evalState :: IxState i o a -> i -> (a, o)
evalState (Pure a)         i = (a, i)
evalState (Free (Get k))   i = evalState (k i) i
evalState (Free (Put s k)) i = evalState k s

test :: IxState Int String ()
test = do
  n <- get
  put (show $ n * 100)

Now, I believe this approach is a fair bit more practical than indexing with monoids, because Haskell doesn't have kind classes or first-class type level functions that would make the monoid approach palatable. It would be nice to have a VerifiedMonoid class, like in Idris or Agda, which includes correctness proofs besides the usual methods. That way we could write a FreeIx that is generic in the choice of the index monoid, and not restricted to lifted lists or something else.

Answer 3

If you're willing to sacrifice the implicit ordering and use explicit accessors instead, your Action '[Int, Int] could be implemented using ReaderT (HList '[Int, Int]). If you use an existing library like vinyl that provides lenses, you could write something like this:

-- Implemented with pseudo-vinyl
-- X and Y are Int fields, with accessors xField and yField
addTwo :: ReaderT (PlainRec '[X, Y]) Output ()
addTwo = do
  x <- view (rGet xField)
  y <- view (rGet yField)
  lift . output $ show (x + y) -- output :: String -> Output ()

Type safety is enforced by constraint propagation: rGet xField introduces a requirement that X be a member of the record.

For a simpler illustration without the type-level machinery, compare:

addTwo :: ReaderT (Int, Int) IO ()
addTwo = do
  x <- view _1
  y <- view _2
  lift . putStrLn $ show (x + y)

We lose the ordering property, which is significant loss, particularly if the ordering is meaningful, e.g. represents the order of user interaction.

Furthermore, we now have to use runReaderT (~ eval). We can't, say, interleave user input with output.