Restricting IO

Stream: new members

[Simon Daniel]

Im looking vor a more concise way to restrict IO effects, i feel like my solution is more verbose than it should be

inductive PrintIO (α:Type)   -- sequence of restricted Effects
| Print: String -> (PrintIO α) -> PrintIO α
| Return: α -> PrintIO α

def PrintIO.bind {α β : Type} : PrintIO α → (α → PrintIO β) → PrintIO β
| Return v, next => next v
| Print s cont, next =>
  PrintIO.Print s (bind (cont) next)

instance: Monad PrintIO where
  pure x := .Return x
  bind := PrintIO.bind

def PrintIO.run: PrintIO α -> IO α
| PrintIO.Print s next => do
  IO.println s
  next.run
| Return v => return v

instance : MonadLift  PrintIO IO where
  monadLift pio := pio.run

def print (s: String): PrintIO Unit := .Print s (.Return ())

def prog: PrintIO Unit :=do   -- here a "program" that may only print
  print "Hello"

def Main: IO Unit := do
  prog