unison/unison-src/tests/console.u

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.++)

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."