(* The illustration of the Boehm-Berarducci encoding The encoding has been introduced in the paper Corrado Boehm and Alessandro Berarducci Automatic Synthesis of Typed {$\Lambda$}-Programs on Term Algebras Theor. Comp. Sci., 1985, v39, pp. 135--154. However, the explanations in the paper may be a bit difficult to understand. The present file aims to clarify the encoding. Boehm-Berarducci encoding represents an inductive data type as a non-recursive but higher-rank data type. The Boehm-Berarducci approach applies only to `strictly positive' data types: there are no functions in the domain of constructors. (See Remark 1.1 (d) in Boehm-Berarducci's paper). The running example is from the first part of the Tagless lecture. *) (* We start with the conventional definition of an inductive data type and write sample operations on it using pattern-matching. *) module InductiveDT = struct type exp = (* A sample inductive type *) | Lit of int | Neg of exp | Add of exp * exp (* Sample term *) let t1 = Add (Lit 8, Neg (Add (Lit 1, Lit 2))) (* The evaluator: case analysis on an expression *) let rec eval : exp -> int = function | Lit x -> x | Neg e -> - (eval e) | Add (e1,e2) -> eval e1 + eval e2 end;; let 5 = InductiveDT.eval InductiveDT.t1;; (* Boehm-Berarducci approach *) (* First we clarify the signature of the exp algebra: the types of the algebra constructors. We represent the signature as a record. It is NOT recursive. *) type 'a exp_dic = {lit : int -> 'a; neg : 'a -> 'a; add : 'a * 'a -> 'a};; (* The datatype-less encoding of expressions. First-class polymorphism is needed. We could have eliminated exp_dic as an argument by currying it. *) type exp = {expi : 'a . 'a exp_dic -> 'a};; (* Constructors *) let lit : int -> exp = fun x -> {expi = fun d -> d.lit x} ;; let neg : exp -> exp = fun {expi = e} -> {expi = fun d -> d.neg (e d)} ;; let add : (exp * exp) -> exp = fun ({expi = e1},{expi = e2}) -> {expi = fun d -> d.add (e1 d, e2 d)} ;; (* Sample term: like InductiveDT.t1, but in the lower case *) let t1 = add (lit 8, neg (add (lit 1, lit 2)));; (* First evaluator: as fold. The function eval1 is not recursive *) let eval1 : exp -> int = fun {expi = e} -> e {lit = (fun x -> x); neg = (fun e -> - e); add = (fun (e1,e2) -> e1 + e2)};; let 5 = eval1 t1;; (* Introspection and pattern-matching *) (* The following shows that we can replace type-level recursion (in InductiveDT.exp) with term-level recursion. Everything that we can do with InductiveDT.exp we can do with Boehm-Berarducci's exp. The following definitions of roll and unroll are actually present in Boehm-Berarducci's paper -- but in a very indirect way. The crucial part is Defn 7.1: sort of self-interpreter: v cons nil ~= v Informally, it shows that roll . unroll should be equivalent to the identity. The equivalence relation (~=) is strictly speaking not the equality; in modern terms, (~=) is contextual equivalence. *) (* First we re-write the signature of the Exp algebra, ExpDic, in the form of a strictly-positive functor *) type 'a expF = | Lit of int | Neg of 'a | Add of 'a * 'a ;; let rec roll : exp expF -> exp = function | Lit x -> lit x | Neg e -> neg e | Add (e1,e2) -> add (e1,e2) ;; (* The occurrence of roll: the source of major inefficiency when we do repeated pattern-matching. *) let unroll : exp -> exp expF = fun {expi = e} -> e {lit = (fun x -> Lit x); neg = (fun e -> Neg (roll e)); add = (fun (e1,e2) -> Add (roll e1, roll e2))};; (* We redo the evaluator, using pattern-matching this time. This evaluator is recursive *) let rec eval2 : exp -> int = fun e -> match unroll e with | Lit x -> x | Neg e -> - (eval2 e) | Add (e1,e2) -> eval2 e1 + eval2 e2 ;; let 5 = eval2 t1;;