correct by construction

imonad.scala

// Correct by construction.
// Adapted from https://gist.github.com/gelisam/9845116.

trait Opened
trait Closed

sealed trait Transition[S,T,A]
case object Open extends Transition[Closed,Opened,Unit]
case object Read extends Transition[Opened,Opened,String]
case object Close extends Transition[Opened,Closed,Unit]

sealed trait Program[S,T,A]
case class Return[S,A](a: A) extends Program[S,S,A]
case class FlatMap[S,T,U,A,B](
  p: Transition[S,T,A],
  f: A => Program[T,U,B]
) extends Program[S,U,B]

trait Ops[S,T,A] {
  def flatMap[U,B](f: A => Program[T,U,B]): Program[S,U,B]
  def map[B](f: A => B): Program[S,T,B]
}

implicit def transitionOps[S,T,A](p: Transition[S,T,A]) = new Ops[S,T,A] {
  def flatMap[U,B](f: A => Program[T,U,B]) = FlatMap(p, f)
  def map[B](f: A => B) = flatMap { a => Return(f(a)) }
}

// Calling run() on this won't type check, because run expects a program with
// Closed start and end states.
val p1 = for {
  x <- Read
} yield ()

// Same thing here, won't typecheck with run().
val p2 = for {
  _ <- Open
  x <- Read
} yield x

// Doesn't typecheck because Read is only valid while Opened.
// val p3 = for {
//   _ <- Close
//   x <- Read
// } yield x

// This is a correct program.
val p4 = for {
  _ <- Open
  x <- Read
  _ <- Close
} yield x

def run(p: Program[Closed,Closed,String]) = p