In a 'Type-Driven Development with Idris' book, there are couple of examples for encoding "programs" using a monadic datatype (leading to useful type-safe encodings with indexed datatypes). Usually, each such datatype can be run in a certain context (for learning purposes it's mostly IO).
I attempted to write another 'runner', that would not be executed in a monadic context, but rather there would be a function to perform one step given some input - if input matches the current program state, we'd feed its value and proceed, obtaining next program state.
This is simple to type if the datatype is not indexed:
data Prog : Type -> Type where
Req : Prog String
Pure : a -> Prog a
(>>=) : Prog a -> (a -> Prog b) -> Prog b
data Event = Resp String
run : Prog a -> Event -> Prog a
run Req (Resp s) = Pure s
run (Pure x) _ = Pure x
run (x >>= f) ev = let x' = run x ev
in case x' of
Pure v => f v
v => v >>= f
And a sample:
prog : Prog String
prog = do
x <- Req
y <- Req
Pure (x ++ y)
test : IO ()
test = do
-- this might doesn't look reasonable , but the point is that we could
-- keep/pass program state around and execute it in whatever manner we wish
-- in some environment
let s1 = run prog (Resp "Hello, ")
let s2 = run s1 (Resp "world")
case s2 of
Pure s => putStrLn s
_ => putStrLn "Something wrong"
This all seems to be working fine, but things get complicated when the main datatype is indexed, and tracks its state in dependently typed manner (depending on results):
data State = StateA | StateB
data Event = Resp String
data Indexed : (ty : Type) -> State -> (ty -> State) -> Type where
Req : Indexed String StateA (\res => case res of "frob" => StateB; _ => StateA)
Pure : (res : a) -> Indexed a (state_fn res) state_fn
(>>=) : Indexed a state1 state2_fn
-> ((res : a) -> Indexed b (state2_fn res) state3_fn)
-> Indexed b state1 state3_fn
Suddenly, it's not easy to type the run function:
run : Indexed a s1 s2_fn -> Event -> Indexed a s3 s4_fn
won't cut it, because caller doesn't dictate the resulting state. This brought me to attempt at 'hiding' those parameters with dependent pair:
run : Indexed a s1 s2_fn -> Event -> (s3 ** s4_fn ** Indexed a s3 s4_fn)
meaning "run this program in particular state for me, I don't care what resulting state (indexes) will be".
But then, Pure is getting problematic:
run (Pure x) _ = (?noIdea ** ?noIdeaAsWell ** (Pure x))
so maybe we also need input indexes:
run : (s1 ** s2_fn ** Indexed a s1 s2_fn) -> Event -> (s3 ** s4_fn ** Indexed a s3 s4_fn)
but the type errors soon became just too much, and lots of work would be just to 'recreate' the values for the dependent pair knowing the transition (which is already defined by transition anyway). This is leading me to thinking I'm on wrong track. How would one attempt at writing such interpreter?
I've pursued what I outlined in my second comment to the question. The type checker successfully convinced me there should be some different approach to that. If it's easy to write 'step' interpreter for a simpler datatype, and indexed datatypes make it harder, then why not define the run with some abstract datatype, that would allow us to build 'simply' typed structure easier for interpretation?
Let's recap:
data State = StateA | StateB
data Indexed : (ty : Type) -> State -> (ty -> State) -> Type where
Req : Indexed String StateA (const StateA)
Pure : (res : a) -> Indexed a (state_fn res) state_fn
(>>=) : Indexed a state1 state2_fn
-> ((res : a) -> Indexed b (state2_fn res) state3_fn)
-> Indexed b state1 state3_fn
Now, let's define an execution context, and a run function that will operate in that context. The run will give us its final value, but will do this via some abstract EventCtx, because all we need is to grab the values from external events, and we don't care how the computation will have them handled:
namespace EventType
data EventType = Req
data Event = Resp String
-- rename: eventType? what about EventType then :) ?
payloadType : EventType -> Type
payloadType EventType.Req = String
interface Monad m => EventCtx (m : Type -> Type) where
fromEvent : (et : EventType) -> m (payloadType et)
run : EventCtx m => Indexed a s1 s2_fn -> m a
run Req = fromEvent EventType.Req
run (Pure res) = pure res
run (x >>= f) = do
x' <- run x
run (f x')
run is now just a standard affair, yay:)
OK, but let's check how we can still be able to run it step by step, with simpler type so that we can store intermediate states somewhere (while waiting for events to occur):
namespace SteppedRunner
data Stepped : Type -> Type where
Await : (et : EventType) -> Stepped (payloadType et)
Pure : a -> Stepped a
(>>=) : Stepped a -> (a -> Stepped b) -> Stepped b
Functor Stepped where
map f x = x >>= (\v => Pure (f v))
Applicative Stepped where
pure = Pure
(<*>) f a = f >>= (\f' =>
a >>= (\a' =>
Pure (f' a')))
Monad Stepped where
(>>=) x f = x >>= f
This is again fairly standard, what we have gained is a simpler type to make our interpretation easier, and free us from some heavy-duty types.
We also need an implementation of our abstract EventCtx, so that we'll be able to use run to turn our Indexed values to a Stepped one:
EventCtx Stepped where
fromEvent = Await
Now, our function to perform a step, given current state and an event:
step : Stepped a -> Event -> Either (Stepped a) a
step s e = fst (step' s (Just e))
where
step' : Stepped a -> Maybe Event -> (Either (Stepped a) a, Maybe Event)
step' (Await Req) (Just (Resp s)) = (Right s, Nothing) -- event consumed
step' s@(Await _) _ = (Left s, Nothing) -- unmatched event (consumed)
step' (Pure x) e = (Right x, e)
step' (x >>= f) e = let (res, e') = step' x e
in case res of
Left x' => (Left (x' >>= f), e')
Right x => step' (f x) e'
The main gist of it is that we can proceed only when we bind (>>=) a value, and we can obtain a value when we have Await and matching event. Rest is just to collapse the structure so that we're ready for another event value.
Some testing program:
test : Indexed String StateA (const StateA)
test = do
x <- Req
y <- do a <- Req
b <- Req
Pure (a ++ b)
Pure (x++ y)
This is how we go from original, indexed datatype to stepped one:
s : Stepped String
s = run test
And now, just for a sake of obtaining a result in testing environment:
steps : Stepped a -> List Event -> Either (Stepped a) a
steps s evs = foldl go (Left s) evs
where go (Right x) _ = Right x
go (Left s) e = step s e
Some repling:
λΠ> steps s [Resp "hoho", Resp "hehe", Resp "hihihi"]
Right "hohohehehihihi" : Either (Stepped String) String