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] ()
liftFdoesn't check either on GHC 7.8.3 – Knottyevalis non-trivial. – CheckerbloomHList. You are trying to build something that reads from theHList, with a proof that it reads the types one-for-one in order. – ThremmatologyaddTwoto something non-associative likeconcatTwo, withshow x ++ " " ++ show y, and adding a note thateval concatTwo (HCons 1 $ HCons 2 $ HNil)would output"1 2". – SentimentalAppendis associative. Specifically, I need to prove thatAppend i1 j1 ~ iimpliesAppend i1 (Append j1 j) ~ Append i j. The only reference I can find for this is gist.github.com/jasonreich/756130 which requires the Stathclyde Haskell Enhancement. – Thremmatology