monads.v

Set Implicit Arguments.

Require Import List String.

(** definition of a monad *)


Class Monad (M : Type -> Type) : Type
  :={
      ret : forall {A : Type}, A -> M A
    ; bind : forall {A B : Type}, M A -> (A -> M B) -> M B
    }.

Notation "x <- c1 ;; c2" := (bind c1 (fun x => c2)) 
                           (right associativity, at level 84, c1 at next level).

Notation "c1 ;; c2" := (bind c1 (fun _ => c2)) (at level 100, right associativity).


(** example instance *)

Instance option_monad : Monad option
  :={
      ret := fun {A : Type}(x : A) => Some x 
    ; bind := fun {A B : Type}(x : option A)(f : A -> option B) =>
                match x with
                | None => None
                | Some y => f y
                end
    }.


(** fixing subtraction *)

Fixpoint subtract (n m : nat) : option nat :=
  match n, m with
  | n' , 0 => ret n'
  | 0  , _ => None
  | S n', S m' => subtract n' m'
  end.

(** monads for evaluating expressions *)

Inductive exp : Set :=
| Num : nat -> exp
| Plus : exp -> exp -> exp
| Minus : exp -> exp -> exp.

Fixpoint eval (e : exp) : option nat :=
  match e with
  | Num n => ret n
  | Plus e1 e2 =>
      n1 <- eval e1 ;;
      n2 <- eval e2 ;;
      ret (n1 + n2)
  | Minus e1 e2 =>
      n1 <- eval e1 ;;
      n2 <- eval e2 ;;
      subtract n1 n2
  end.

(** improved error support *)

Inductive err (A : Type) : Type :=
| Ok : A -> err A | Fail : string -> err A.

Arguments Fail [A] _.

Instance err_monad : Monad err
  :={
      ret := fun {A : Type}(x : A) => Ok x
      ; bind := fun {A B : Type}(x : err A)(f : A -> err B) =>
                  match x with
                  | Ok y => f y
                  | Fail s => Fail s
                  end
    }.

Definition tryCatch {A : Type} (e : err A) (s:string) (handler : err A) : err A := 
  match e with 
    | Fail s' => if string_dec s s' then handler else e
    | _ => e
  end.

Fixpoint eval' (e : exp) : err nat :=
  match e with
  | Num n => ret n
  | Plus e1 e2 =>
      n1 <- eval' e1 ;;
      n2 <- eval' e2 ;;
      ret (n1 + n2)
  | Minus e1 e2 =>
      n1 <- eval' e1 ;;
      n2 <- eval' e2 ;;
      match subtract n1 n2 with
      | None => Fail "underflow"
      | Some m => ret m
      end
  end.

(** modeling state *)

Definition var := string.

Inductive exp_s : Type := 
| Var_s : var -> exp_s
| Plus_s : exp_s -> exp_s -> exp_s
| Times_s : exp_s -> exp_s -> exp_s
| Set_s : var -> exp_s -> exp_s
| Seq_s : exp_s -> exp_s -> exp_s
| If0_s : exp_s -> exp_s -> exp_s -> exp_s.

Definition state := var -> nat.

Definition upd(x:var)(n:nat)(s:state) : state :=
  fun v => if string_dec x v then n else s x.

Definition state_comp (A:Type) := state -> (state * A).

Instance state_monad : Monad state_comp := {
  ret := fun {A:Type} (x:A) => (fun (s:state) => (s,x)) ; 
  bind := fun {A B:Type} (c : state_comp A) (f: A -> state_comp B) => 
            fun (s:state) => 
              let (s',v) := c s in 
              f v s'
}.

Definition read (x:var) : state_comp nat := 
  fun s => (s, s x).

Definition write (x:var) (n:nat) : state_comp nat := 
  fun s => (upd x n s, n).

Fixpoint eval_sm (e:exp_s) : state_comp nat := 
  match e with 
    | Var_s x => read x
    | Plus_s e1 e2 => 
      n1 <- eval_sm e1 ;; 
      n2 <- eval_sm e2 ;; 
      ret (n1 + n2)
    | Times_s e1 e2 =>
      n1 <- eval_sm e1 ;; 
      n2 <- eval_sm e2 ;; 
      ret (n1 * n2)
    | Set_s x e => 
      n <- eval_sm e ;; 
      write x n 
    | Seq_s e1 e2 => 
      _ <- eval_sm e1 ;; 
      eval_sm e2
    | If0_s e1 e2 e3 => 
      n <- eval_sm e1 ;;
      match n with 
        | 0 => eval_sm e2
        | _ => eval_sm e3 
      end
  end.

(** properties *)

Class Monad_with_Laws (M: Type -> Type){MonadM : Monad M} :=
{
  m_left_id : forall {A B:Type} (x:A) (f:A -> M B), bind (ret x) f = f x ;
  m_right_id : forall {A B:Type} (c:M A), bind c ret = c ;
  m_assoc : forall {A B C} (c:M A) (f:A->M B) (g:B -> M C), 
    bind (bind c f) g = bind c (fun x => bind (f x) g)
}.


Instance OptionMonadLaws : @Monad_with_Laws option _ := {}.
  auto.
  intros ; destruct c ; auto.
  intros ; destruct c ; auto.
Defined.