Futamura Projections in Coq

futamura.v

Require Import ssreflect ssrfun.

Module Futamura.
  (* Program from a -> b written in L *)
  Inductive Program {a b language : Type} :=
  | mkProgram : (a -> b) -> Program.

  Definition runProgram {A B L} (p : @Program A B L) := match p with mkProgram f => f end.
  Notation "[ S | a >> b ]" := (@Program a b S) (at level 2) : type_scope.

  (* An interpreter for S implemented in O *)
  Definition Interpreter S O :=
    forall a b, [O | [S | a >> b] * a >> b].

  (* A compiler from S to T implemented in T *)
  (* Read as: takes a function a -> b in S and returns function a ->
     b in T, implemented in T. *)
  Definition Compiler S T :=
    forall a b, [T | [S | a >> b] >> [T | a >> b]].

  (* Self-hosting specializer from S to T *)
  Definition Specializer S T :=
    forall i a b, [S | [S | i * a >> b] * i >> [T | a >> b]].

  (* Compiler-compiler from S to T *)
  Definition Partializer S T :=
    forall i a b, [T | [S | i * a >> b] >> [T | i >> [T | a >> b]]].

  Definition projection1 {O S T A B}
             (s : Specializer O T) (i : Interpreter S O) (p : [S | A >> B]) : [T | A >> B].
  Proof.
    eapply runProgram; eauto.
  Defined.

  Definition projection2 {O S T} (s : Specializer O T) (i : Interpreter S O) : Compiler S T.
  Proof.
    cbv in *; intros; refine (runProgram (s _ _ _) (s _ _ _, i _ _)).
  Defined.

  Definition projection3 {S T} (s : Specializer S T) : Partializer S T.
  Proof.
    cbv in *; intros; refine (runProgram (s _ _ _) (s _ _ _, s _ _ _)).
  Defined.

End Futamura.