Accompanying code for https://ptival.github.io/deep-dive-meta-theory-carte-2

mtc-2.v

(** Preliminary definitions *)

Class SupportsFeature (E F : Set -> Set) :=
  {
    inject : forall (A : Set), F A -> E A;
  }.
Arguments inject {E F _ A}.
Notation "E 'supports' F" := (SupportsFeature E F) (at level 50).

Global Instance supports_Refl F
  : F supports F
  := {| inject := fun _ x => x; |}.

Inductive Boolean (E : Set) : Set :=
| MkBoolean (b : bool)
| IfThenElse (condition thenBranch elseBranch : E)
.
Arguments MkBoolean  {E}.
Arguments IfThenElse {E}.

Inductive Natural (E : Set) : Set :=
| MkNatural (n : nat)
| Plus (m n : E)
.
Arguments MkNatural {E}.
Arguments Plus      {E}.

Declare Scope Sum1. (* remove for older versions of Coq *)
Delimit Scope Sum1 with Sum1.
Open Scope Sum1.

Variant Sum1 (F G : Set -> Set) (A : Set) : Set :=
| inl1 : F A -> (F + G)%Sum1 A
| inr1 : G A -> (F + G)%Sum1 A
where
"F + G" := (Sum1 F G) : Sum1.
Arguments inl1 {F G A}.
Arguments inr1 {F G A}.

(**
We will use this "slow" bool-producing function to demonstrate a problem with
F-algebras.
 *)
Fixpoint slowBool (seed : nat) : bool :=
  match seed with
  | 0   => true
  | S n => if slowBool n then slowBool n else slowBool n
  end.

(** End of preliminary definitions *)



Module FAlgebra.

  Definition Fix (F : Set -> Set) : Set :=
    forall (A : Set), (F A -> A) -> A.

  Definition boolean
             {E : Set -> Set}
             `{E supports Boolean}
             (b : bool)
    : Fix E
    := fun _ wrap => wrap (inject (MkBoolean b)).

  Definition ifThenElse
             {E : Set -> Set}
             `{E supports Boolean}
             (c t e : Fix E)
    : Fix E
    := fun _ wrap => wrap (inject (IfThenElse (c _ wrap) (t _ wrap) (e _ wrap))).

  Definition countFalsesAndTrues (b : Boolean (nat * nat)) : (nat * nat) :=
    match b with
    | MkBoolean false                             => (1, 0)
    | MkBoolean true                              => (0, 1)
    | IfThenElse (f_c, t_c) (f_t, t_t) (f_e, t_e) => (f_c + f_t + f_e, t_c + t_t + t_e)%nat
    end.

  Definition someTerm : Fix Boolean :=
    ifThenElse (boolean true)
               (ifThenElse (boolean true) (boolean true) (boolean false))
               (boolean (slowBool 28)).

  Definition evalBool
             (b : Boolean bool)
    : bool :=
    match b with
    | MkBoolean bl => bl
    | IfThenElse c t e => if c then t else e
    end.

  (* This will be very slow *)
  Compute someTerm bool evalBool.

End FAlgebra.



Module MAlgebra.

  Definition MendlerAlgebra (F : Set -> Set) (A : Set) : Set :=
    forall (R : Set), (R -> A) -> F R -> A.

  Definition Fix (F : Set -> Set) : Set :=
    forall (A : Set), MendlerAlgebra F A -> A.

  Definition ifThenElse
             {E : Set -> Set}
             `{E supports Boolean}
             (c t e : Fix E)
    : Fix E
    := fun A malg => malg (Fix E) (fun e => e A malg) (inject (IfThenElse c t e)).

  Definition boolean
             {E : Set -> Set}
             `{E supports Boolean}
             (b : bool)
    : Fix E
    := fun A malg => malg A (fun x => x) (inject (MkBoolean b)).

  Definition someTerm : Fix Boolean :=
    ifThenElse (boolean true)
               (ifThenElse (boolean true) (boolean true) (boolean false))
               (boolean (slowBool 28)).

  Definition countFalsesAndTrues
             (R : Set) rec (b : Boolean R)
    : (nat * nat) :=
    match b with
    | MkBoolean false  => (1, 0)
    | MkBoolean true   => (0, 1)
    | IfThenElse c t e =>
      let '(f_c, t_c) := rec c in
      let '(f_t, t_t) := rec t in
      let '(f_e, t_e) := rec e in
      (f_c + f_t + f_e, t_c + t_t + t_e)%nat
    end.

  (* This will be slow as it needs to evaluate the else branch *)
  Compute (someTerm (nat * nat)%type countFalsesAndTrues).

  Definition evalBool
             (R : Set) (rec : R -> bool) (b : Boolean R)
    : bool :=
    match b with
    | MkBoolean bl => bl
    | IfThenElse c t e => if rec c then rec t else rec e
    end.

  (* This will be fast, as it never evaluates the else branch *)
  Compute (someTerm bool evalBool).

  Class ProgramAlgebra (Tag : Set) F A :=
    {
      programAlgebra : forall (R : Set), (R -> A) -> F R -> A;
    }.

  Inductive EvalResult :=
  | ValueBoolean (b : bool)
  | ValueNatural (n : nat)
  | Stuck
  .

  Variant ForEval := . (* tag *)

  Global Instance Eval__Boolean
    : ProgramAlgebra ForEval Boolean EvalResult
    :=
      {|
        programAlgebra :=
          fun _ rec b =>
            match b with
            | MkBoolean b      => ValueBoolean b
            | IfThenElse c t e =>
              match rec c with
              | ValueBoolean b =>
                if b then rec t else rec e
              | _ => Stuck
              end
            end
      |}.

  Definition natural
             {E : Set -> Set}
             `{E supports Natural}
             (n : nat)
    : Fix E
    := fun _ malg => malg _ (fun x => x) (inject (MkNatural n)).

  Definition plus
             {E : Set -> Set}
             `{E supports Natural}
             (a b : Fix E)
    : Fix E
    := fun A malg => malg (Fix E) (fun e => e A malg) (inject (Plus a b)).

  Global Instance Eval__Natural
    : ProgramAlgebra ForEval Natural EvalResult
    :=
      {|
        programAlgebra :=
          fun _ rec n =>
            match n with
            | MkNatural n => ValueNatural n
            | Plus a b    =>
              match (rec a, rec b) with
              | (ValueNatural a, ValueNatural b) => ValueNatural (a + b)
              | _ => Stuck
              end
            end
      |}.

  Global Instance ProgramAlgebra__Sum1
         (Tag : Set) (F G : Set -> Set)
         (A : Set)
         `{ProgramAlgebra Tag F A}
         `{ProgramAlgebra Tag G A}
    : ProgramAlgebra Tag (F + G) A
    :=
      {
        programAlgebra :=
          fun _ rec s =>
            match s with
            | inl1 l => programAlgebra _ rec l
            | inr1 r => programAlgebra _ rec r
            end
      }.

  Definition eval
             (e : Fix (Boolean + Natural))
    : EvalResult
    := e _ (programAlgebra (Tag := ForEval)).

  Global Instance Sum1_supports_Left F G
    : (F + G) supports F
    := {| inject := fun _ l => inl1 l; |}.

  Global Instance Sum1_supports_Right F G
    : (F + G) supports G
    := {| inject := fun _ r => inr1 r; |}.

  Compute (
      eval
        (plus
           (ifThenElse (boolean false) (natural 22) (natural 41))
           (natural 1)
        )
    ).

End MAlgebra.