hirrolot

This is the predecessor of Mazeppa.

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 th

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.

	type term = Var of string \| Call of string * term array
	[@@deriving show { with_path = false }]

	type possibilities = term array [@@deriving show]

	let demux ~(x : string) ~(values : term array) : term -> possibilities =
	let rec go = function
	\| Var y when x = y -> values
	\| Var _ as t -> Array.map (fun _ -> t) values
	\| Call (op, args) ->

	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

	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

	(* 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

	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)

	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 ^ ")"

	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

	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