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

mtc-1.v

(** Our two extensible language feature definitions *)

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}.

(** Our type-level fixed point type *)

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

(** Sum of language features **)

Delimit Scope Sum1_scope with Sum1.
Open Scope Sum1_scope.

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_scope.
Arguments inl1 {F G A}.
Arguments inr1 {F G A}.

Definition BooleanAndNatural
           : Set -> Set
  := Boolean + Natural.

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 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; |}.

(** Smart constructors **)

Section Boolean.

  Context {E : Set -> Set}.
  Context `{E supports Boolean}.

  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))).

End Boolean.

Section Natural.

  Context {E : Set -> Set}.
  Context `{E supports Natural}.

  Definition natural
             (n : nat)
    : Fix E
    := fun _ wrap => wrap (inject (MkNatural n)).

  Definition plus
             {E : Set -> Set}
             `{E supports Natural}
             (m n : Fix E)
    : Fix E
    := fun _ wrap => wrap (inject (Plus (m _ wrap) (n _ wrap))).

End Natural.

Definition extensibleTerm
           {E : Set -> Set}
           `{E supports Boolean}
           `{E supports Natural}
  : Fix E
  := (ifThenElse (boolean true) (natural 0) (plus (natural 1) (natural 2))).

Definition concreteTerm : Fix BooleanAndNatural
  := extensibleTerm.