New draft on Normalization by Evaluation using GADTs
by Matthias Puech
There is a new draft on my web page! It is called Tagless and Typeful Normalization by Evaluation using Generalized Algebraic Data Types, which is a mouthful, but only describes accurately the cool new OCaml development we elaborated together with Olivier and Chantal. The world of Normalization by Evaluation (NbE) is still relatively new to me, but its wonders keep amazing me. It’s a program specialization algorithm… no, it’s a completeness proof for first-order logic… wait, it’s a technique to turn an interpreter into a compiler! Definitely, Aarhus University, my new home, is not the worst place to learn about it.
Since the introduction of GADTs in OCaml, a whole new realm of applications emerged, the most well-known being to faithfully represent typed languages: it allows to define compact and correct interpreters, and type-preserving program transformations. Ok, if you never saw this, here is a small snippet that should be self-explanatory:
type _ exp = | Val : 'a -> 'a exp | Eq : 'a exp * 'a exp -> bool exp | Add : int exp * int exp -> int exp let rec eval : type a. a exp -> a = function | Val x -> x | Eq (e1, e2) -> eval e1 = eval e2 | Add (e1, e2) -> eval e1 + eval e2 ;; assert (eval (Eq (Add (Val 2, Val 2), Val 4)))
Nice, isn’t it? Our question was: if we can so beautifully go from typed syntax (expressions) to typed semantics (OCaml values), can we do the converse, i.e., go from an OCaml value back to a (normal) expression of the same type? In other words, can we implement NbE in a typeful manner, using GADTs?
The answer is a proud “yes”, but more interestingly, we all learned some interesting GADT techniques and puzzling logical interpretations on the way. Read on to know more!
Tagless and Typeful Normalization by Evaluation using Generalized Algebraic Data Types
We present the first tagless and typeful implementation of normalization by evaluation for the simply typed λ-calculus in OCaml, using Generalized Algebraic Data Types (GADTs). In contrast to normalization by reduction, which is operationally carried out by repeated instances of one-step reduction, normalization by evaluation uses a non-standard model to internalize intermediate results: it is defined by composing a non-standard evaluation function with a reification function that maps the denotation of a term into the normal form of this term. So far, normalization by evaluation has been implemented either in dependently-typed languages such as Coq or Agda, or in general-purpose languages such as Scheme, ML or Haskell. In the latter case, denotations are either tagged or Church-encoded. Tagging means injecting denotations, either implicitly or explicitly, into a universal domain of values; Church encoding is based on the impredicativity of the metalanguage. Here, we show how to obtain not only tagless values, making evaluation efficient, but also typeful reification, guaranteeing type preservation and η-long, β-normal forms. To this end, we put OCaml’s GADTs to work. Furthermore, our implementation does not depend on any particular representation of binders (HOAS, de Bruijn levels or indices) nor on the style (direct style, continuation-passing style, etc.) of the non-standard evaluation function.
PS: My previous draft, Proofs, upside down was accepted for presentation at APLAS 2013. See you in Melbourne!
I don’t understand: GADTs are tagged, just like all other algebraic datatypes. Take a look at what they compile to. So I don’t understand why you call your method ‘tagless’. If you are tag-free, you won’t be able to do any pattern-matching at all, which does introduce some rather non-trivial complications!
Surprisingly, you don’t seem to be aware of the “finally tagless” approach, which does get rid of the tags entirely — and where it is shown, for example, how to do CPS conversion. And, of course, the very first interpreter in the “finally tagless” paper does some form of NbE (all without GADTs).
Dear Jacques,
It is very nice to hear from you, thank you very much for your comment. You are right: of course, GADT values are tagged. In the draft, we chose to present the initial syntax of terms as a GADT [‘a tm], but what we refer to tagless are actually the *values* (i.e. the result of [eval]): they have type [‘a] (and not [‘a value], an ADT). As Boespflug, Dénès and Grégoire measured in the implementation of Coq, value tagging seems to be the real performance bottleneck.
As far as I understand, the “finally tagless” approach is orthogonal to our point, and we could have implemented tagless evaluation of terms in this style as well (this remark should have appeared in the draft, it is fixed now). The important GADT here is not really the one for terms, but the one for types, [‘a tp]: it is this one we need to pattern-match on to reconstruct the normal form [‘a nf] in our off-line NbE (which is different from your on-line partial evaluation). Are you suggesting that there would be a way to turn this GADT into finally tagless style?
Note that normal forms (type [‘a nf]) are already represented as an abstract module, à la “finally tagless”. We present it as a “modular” representation, since it can be instantiated with actual, tagged term representation as well as tagless “evaluation” of your choice.
About CPS translation, both are similar of course, but I think that the difference between a tagless translation and a representation of terms with GADTs is that in the latter case, one can witness the type-level translation directly, as we did (look at type [‘a tm] on page 12 for instance).
Does it answer your concerns?
Yes, this does.
Let me make a further suggestion: at the bottom of p.4, you (correctly) say “Then,eval can be given type α tm → α .” This is where you should repeat the remark that there are no tags in the value type. So although your source language is tagged, your target language is not — which is indeed quite different than the “finally tagless” approach, where it is possible for both to be untagged [or both to be tagged too!]
You also say “The important GADT here is not really the one for terms, but the one for types, [‘a tp]”. On my first read of your paper, this did not sink in for me. You might want to be explicit about this, earlier in your paper (maybe even in the introduction?).
An interesting issue to think about are ‘exotic types': while HOAS does rule out exotic terms, Atkey, Lindley and Yallop in http://homepages.inf.ed.ac.uk/slindley/papers/unembedding.pdf make a big deal out of also ensuring that you can’t give ‘exotic types’ to some (proper) terms. That might be worth examining as well — certainly I am not convinced that one can’t do this in the context of the system presented in your section 2.2.1. Of course, sneaking in such things in the system of section 3.2.1 would be significantly harder, but may still be possible.
The fact that there are no inhabitants of ‘base’ is good, as these will be used to represent variables in the middle of your computation, and you can’t have these be “raw”.
Note that part of the point of “finally tagless” is that if you are parametric over a type constructor (which you are in NormalForm of section 3.2), then what you do in Section 4 has the same NormalForm signature — which appears true in your case, but is not stated explicitly.
Lastly, take a good look at the PE in finally tagless. You’ll see our troubles with the lack of type families (in Haskell as well as in Ocaml), which we had to solve in ad hoc ways at the time. But now, in both languages, this can be done.
Anyways, this is a nice piece of work (else I would not have bothered to read+comment to this depth!).
Jacques, these are extremely valuable comments! We will take them into account for sure. Yes, it’s probably worth redoing Finally Tagless’s PE with my new understanding of NbE. I actually discovered Atkey et al.’s paper not long ago, I’m still wrapping my head around it. Thank you again!
Pretty interesting read (and I’ve discovered really nice papers in the references! e.g. Hatcliff and Danvy’s A Generic Account of CPSs). Is the accompanying code available somewhere for us to play with the beast?
Hello Guillaume,
Thank you for your feedback. I just updated my web page with the code of the draft. Here is the quick link to it: http://www.pps.univ-paris-diderot.fr/~puech/typeful.ml
Happy hacking!
[…] October, I publicized here a new draft on normalization by evaluation, which provoked some very helpful comments and constructive criticisms. Together with Chantal and […]
Reblogged this on My Thoughts.