### Update on Typeful Normalization by Evaluation

#### by Matthias Puech

In October, I publicized here a new draft on normalization by evaluation, which provoked some very helpful comments and constructive criticisms. Together with Chantal and Olivier, we thus revised the draft profoundly and a revamped version is available on my web site.

Besides the enhanced form and better explanations, we included a completely new section on what it means for NbE to be written in Continuation-Passing Style, that I am particularly excited about. This allowed us to extend our typeful NbE formalization beyond the minimal λ-calculus to sums and **call/cc** (which is known to be difficult). Taking our code, you can write a program with **call/cc** and **if** statements, and partially evaluate it: all redexes will be removed and your code will be specialized. All this, as before, is done *typefully*, thanks to OCaml’s GADTs: this means that the transformation is guaranteed to map well-typed terms to well-typed normal forms.

What I really liked about working on program transformations with GADTs, is that they enable an efficient methodology to devise your tranformations, and read off of them the (typed) target language. Let me give you an example. Say we write the canonical, direct-style evaluator for the λ-calculus:

let rec eval = function | Lam f -> Fun (fun x -> eval (f (Var x))) | App (m, n) -> let Fun f = eval m in f (eval n) | Var x -> x

If the input language is simply typed:

type 'a tm = | Lam : ('a tm -> 'b tm) -> ('a -> 'b) tm | App : ('a -> 'b) tm * 'a tm -> 'b tm | Var : 'a vl -> 'a tm

then so can be the output language:

type 'a vl = Fun : ('a vl -> 'b vl) -> ('a -> 'b) vl

and the type of `eval`

then guarantees to preserve types: `type a. a tm -> a vl`

. Up to here, no big news. Now what if I CPS-transform the code above? Following the usual, call-by value CPS transformation, I get:

type o let rec eval : type a. a tm -> (a vl -> o) -> o = function | Lam f -> fun k -> k (Fun (fun x k -> eval (f (Var x)) k)) | App (m, n) -> fun k -> eval m (fun (Fun v1) -> eval n (fun v2 -> v1 v2 k)) | Var x -> fun k -> k x

My input language is unchanged, but what about the output values? As you can hint from the `Lam`

and `App`

cases, the type of constructor `Fun`

has been changed. Using type inference, type errors and `C-c C-t`

in my `tuareg-mode`

, I can read off the new type it should have:

type 'a vl = Fun : ('a vl -> ('b vl -> o) -> o) -> ('a -> 'b) vl

Yes, this is the type of CPS values! For instance, I can write the CPS-transformed applicator:

let app : type a b. ((a -> b) -> a -> b) vl = Fun (fun (Fun f) k -> k (Fun (fun x k -> f x k)))

The same way, if I write the usual Normalization by Evaluation algorithm from typed values to typed normal forms and CPS-transform it, I can deduce the specialized syntax of normal forms in CPS:

S ::= let v = R M in S | return k M

M ::= λxk. S | R

R ::= x | v

If this excites you or puzzles you, come read our draft, and do not hesitate to leave any comment below!

The link to the paper is (currently) broken.

Oops! It is fixed now, thank you.

[…] It turns out that there is an adequate encoding, that relies on two simple ideas. The first is to treat variables in patterns as nameless placeholders bound by λ-abstractions on the right side of the arrow (this is how e.g. Coq encodes matches: match E₁ with (y, z) -> E₂ actually is sugar for match E₁ with (_, _) -> fun x y -> E₂); the second is to thread and accumulate type arguments in a GADT, much like we demonstrated in our printf example recently. […]