Inductive result (S F : Type) :=
  | Success : S -> result S F
  | Failure : F -> result S F.

Inductive unit := Unit.

Inductive procedure (S F : Type) :=
  | Procedure : (unit -> result S F) -> procedure S F.

Definition execute
  {S F : Type}
  (p   : procedure S F)
: result S F :=
  match p with
  | Procedure f => f Unit
  end.

Definition combine
  {S T F : Type}
  (p     : procedure S F)
  (f     : S -> procedure T F)
: procedure T F :=
  Procedure T F (fun _ =>
    match execute p with
    | Success x => execute (f x)
    | Failure y => Failure T F y
    end).

Notation "p >>= f" :=
  (combine p f) (at level 50, left associativity).

Definition order
  {S T F : Type}
  (p     : procedure S F)
  (q     : procedure T F)  
: procedure T F :=
  combine p (fun _ => q).

Notation "p >> q" :=
  (order p q) (at level 50, left associativity).

Definition succeed
  {S F : Type}
  (x   : S)
: procedure S F :=
  Procedure S F (fun _ => Success S F x).

Definition fail
  {S F : Type}
  (x   : F)
: procedure S F :=
  Procedure S F (fun _ => Failure S F x).

(*
Definition type_error :=
  fail false >> fail 0.

Error: The term "fail 0" has type "procedure ?310 nat"
 while it is expected to have type "procedure ?306 bool".
*)  

Definition catch
  {S F G   : Type}
  (p       : procedure S F)
  (handler : F -> procedure S G)
: procedure S G :=
  match execute p with
  | Success x => succeed x
  | Failure f => handler f
  end.

Require Import Coq.Strings.String.

Module IO.
  Inductive error :=
    | File_Not_Found
    | Permission_Denied
    | Device_Busy.

  Definition file := nat.
  Axiom file_open : string -> procedure file error.
  Axiom file_close : file -> procedure unit error.
  Axiom file_write : file -> string -> procedure unit error.
  Axiom file_write_nat : file -> nat -> procedure unit error.
End IO.

Definition io_example0 : procedure unit IO.error :=
  IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd.

(*
Definition type_error : procedure unit unit :=
  IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd.

Error: The term
 "IO.file_open "file.txt" >>=
  (fun fd : IO.file =>
   IO.file_write fd "Line 0" >> IO.file_write fd "Line 1" >>
   IO.file_write fd "Line 2" >> IO.file_close fd)" has type
 "procedure unit IO.error" while it is expected to have type
 "procedure unit unit".
*)

Definition io_example1 : procedure unit unit :=
  catch (IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd)
    (fun _ => succeed Unit).

Inductive other_error :=
  | IO_Failed_Soft : IO.error -> other_error
  | IO_Failed_Hard : IO.error -> other_error
  | Other_Failure.

Definition io_example2 : procedure unit other_error :=
  catch (IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd)
    (fun e => match e with
     | IO.File_Not_Found    => fail (IO_Failed_Hard IO.File_Not_Found)
     | IO.Permission_Denied => fail (IO_Failed_Hard IO.Permission_Denied)
     | IO.Device_Busy       => fail (IO_Failed_Soft IO.Device_Busy)
     end).

Definition handle_all
  {A : Set}
  (e : IO.error)
: procedure A other_error :=
  match e with
  | IO.File_Not_Found    => fail (IO_Failed_Hard IO.File_Not_Found)
  | IO.Permission_Denied => fail (IO_Failed_Hard IO.Permission_Denied)
  | IO.Device_Busy       => fail (IO_Failed_Soft IO.Device_Busy)
  end.

Definition io_example3 : procedure unit other_error :=
  catch (IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd)
    handle_all.

Module Motor_Control.
  Inductive error :=
    | Velocity_Too_Fast
    | Velocity_Too_Slow
    | On_Fire.

  Axiom set_velocity : nat -> procedure unit error.
  Axiom get_velocity : unit -> procedure nat error.
End Motor_Control.

Inductive combined_error :=
  | IO_Error    : IO.error -> combined_error
  | Motor_Error : Motor_Control.error -> combined_error.

Definition r_io
  {S : Type}
  (p : procedure S IO.error)
: procedure S combined_error :=
  catch p (fun e => fail (IO_Error e)).

Definition r_motor
  {S : Type}
  (p : procedure S Motor_Control.error)
: procedure S combined_error :=
  catch p (fun e => fail (Motor_Error e)).

Definition converge_example0 : procedure unit combined_error :=
  r_io    (IO.file_open "motor-log.txt")    >>= fun file =>
  r_motor (Motor_Control.get_velocity Unit) >>= fun v =>
  r_io    (IO.file_write_nat file v)        >>
  r_motor (Motor_Control.get_velocity Unit) >>= fun v =>
  r_io    (IO.file_write_nat file v >> IO.file_close file).