Hirrolot

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by the program; let us call this machine M₁. In observing the operation of

Hirrolot

module Make_term (S : sig
  type 'a t [@@deriving show]
end) =
struct
  type t = def S.t

  and def = Lam of t | Var of int | Appl of t * t
  [@@deriving show { with_path = false }]

  let _ = S.show

Hirrolot

This is a minimalistic OCaml implementation of the type system from chapter 30 of TAPL, "Higher-Order Polymorphism".

The implementation uses bidirectional typing and does not feature existential types. Binders are represented as metalanguage functions (HOAS-style); free variables (TyFreeVar & FreeVar) are represented as De Bruijn levels.

See also:

• "Barebones lambda cube in OCaml"
• "How to implement dependent types in 80 lines of code"

Hirrolot

type cps_var =
  (* Taken from the lambda term during CPS conversion. *)
  | CLamVar of string
  (* Generated uniquely during CPS conversion. *)
  | CGenVar of int

type cps_term =
  | CFix of (cps_var * cps_var list * cps_term) list * cps_term
  | CAppl of cps_var * cps_var list
  | CRecord of cps_var list * binder

Hirrolot

(* A variable identifier of the lambda language [term]. *)
type var = string [@@deriving eq]

(* The lambda language; direct style. *)
type term =
  | Var of var
  | Fix of (var * var list * term) list * term
  | Appl of term * term list
  | Record of term list
  | Select of term * int

Hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

Hirrolot

type term = Lam of (term -> term) | Appl of term * term | FreeVar of int

let unfurl lvl f = f (FreeVar lvl)
let unfurl2 lvl (f, g) = (unfurl lvl f, unfurl lvl g)

let rec print lvl =
  let plunge f = print (lvl + 1) (unfurl lvl f) in
  function
  | Lam f -> "(λ" ^ plunge f ^ ")"
  | Appl (m, n) -> "(" ^ print lvl m ^ " " ^ print lvl n ^ ")"

Hirrolot

module type Form = sig
  type ('env, 'a) meaning

  val vz : ('a * 'env, 'a) meaning
  val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
  val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

  val appl :
    ('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
end

Hirrolot

module type Form = sig
  type 'a meaning

  val lam : ('a meaning -> 'b meaning) -> ('a -> 'b) meaning
  val appl : ('a -> 'b) meaning -> 'a meaning -> 'b meaning
end

(* Evaluate a given term. *)
module Eval = struct
  type 'a meaning = 'a

Hirrolot

let lam f = f
let appl f x = f x