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!