effect State s where
  get : {State s} s
  set : s -> {State s} ()

effect Console where
  read : {Console} (Optional Text)
  write : Text -> {Console} ()

fst x = case x of Pair.Pair a _ -> a

--TODO type is wrongly being inferred (or at least displayed) as `Pair a (Pair a b) ->{} a`
snd x = case x of Pair.Pair _ (Pair.Pair b _) -> b

namespace Console where

  state : s -> Effect (State s) a -> a
  state s c = case c of
    {State.get -> k} -> handle state s in k s
    {State.set s' -> k} -> handle state s' in k ()
    {a} -> a

  simulate : Effect Console d -> {State ([Text], [Text])} d
  simulate c = case c of
    {Console.read -> k} ->
      io = State.get
      ins = fst io
      outs = snd io
      State.set (drop 1 ins, outs)
      -- this really should typecheck but doesn't for some reason
      -- error is that `simulate` doesn't check against `Effect Console c -> r`,
      -- but seems like that `r` should get instantiated as `{State (..)} c`.
      handle simulate in k (at 0 ins)
    {Console.write t -> k} ->
      io = State.get
      ins = fst io
      outs = snd io
      -- same deal here
      handle simulate in k (State.set (ins, cons t outs))
    {a} -> a

(++) = (Text.++)

x = handle Console.state ([],[]) in
      handle Console.simulate in
        use Console read write
        use Optional Some None
        write "What's your name?"
        case read of
          Some name -> write ("Hello" ++ name)
          None -> write "Fine, be that way."

> x