Alternative way of interpreting computation build with indexed datatype

Question

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?

Answer 1

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