title: Alternative way of interpreting computation build with indexed datatype
body: <p>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 <code>IO</code>).</p>
  
  <p>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 <code>step</code> given some input - if input matches the current program state, we'd feed its value and proceed, obtaining next program state.</p>
  
  <p>This is simple to type if the datatype is not indexed:</p>
  
  <pre><code>  data Prog : Type -&gt; Type where
      Req : Prog String
      Pure : a -&gt; Prog a
      (&gt;&gt;=) : Prog a -&gt; (a -&gt; Prog b) -&gt; Prog b
  
    data Event = Resp String
  
    run : Prog a -&gt; Event -&gt; Prog a
    run Req (Resp s) = Pure s
    run (Pure x) _ = Pure x
    run (x &gt;&gt;= f) ev = let x' = run x ev
                      in case x' of
                            Pure v =&gt; f v
                            v =&gt; v &gt;&gt;= f
  </code></pre>
  
  <p>And a sample:</p>
  
  <pre><code>  prog : Prog String
    prog = do
      x &lt;- Req
      y &lt;- 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 =&gt; putStrLn s
        _ =&gt; putStrLn "Something wrong"
  </code></pre>
  
  <p>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):</p>
  
  <pre><code>data State = StateA | StateB
  
  data Event = Resp String
  
  data Indexed : (ty : Type) -&gt; State -&gt; (ty -&gt; State) -&gt; Type where
    Req : Indexed String StateA (\res =&gt; case res of "frob" =&gt; StateB; _ =&gt; StateA)
    Pure : (res : a) -&gt; Indexed a (state_fn res) state_fn
    (&gt;&gt;=) : Indexed a state1 state2_fn
        -&gt; ((res : a) -&gt; Indexed b (state2_fn res) state3_fn)
        -&gt; Indexed b state1 state3_fn
  </code></pre>
  
  <p>Suddenly, it's not easy to type the <code>run</code> function:</p>
  
  <p><code>run : Indexed a s1 s2_fn -&gt; Event -&gt; Indexed a s3 s4_fn</code></p>
  
  <p>won't cut it, because caller doesn't dictate the resulting state. This brought me to attempt at 'hiding' those parameters with dependent pair:</p>
  
  <p><code>run : Indexed a s1 s2_fn -&gt; Event -&gt; (s3 ** s4_fn ** Indexed a s3 s4_fn)</code></p>
  
  <p>meaning "run this program in particular state for me, I don't care what resulting state (indexes) will be".</p>
  
  <p>But then, <code>Pure</code> is getting problematic:</p>
  
  <p><code>run (Pure x) _ = (?noIdea ** ?noIdeaAsWell ** (Pure x))</code></p>
  
  <p>so maybe we also need input indexes:</p>
  
  <p><code>run : (s1 ** s2_fn ** Indexed a s1 s2_fn) -&gt; Event -&gt; (s3 ** s4_fn ** Indexed a s3 s4_fn)</code></p>
  
  <p>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?</p>