A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

Tag: evaluation

Representing pattern-matching with GADTs

Here is a little programming pearl. I’ve been wanting to work on pattern-matching for a while now, and it seems like I will finally have this opportunity here at my new (academic) home, McGill.

Encoding some simply-typed languages with GADTs is now routine for a lot of OCaml programmers. You can even take (kind of) advantage of (some form of) convenient binding representation, like (weak) HOAS; you then use OCaml variables to denote your language’s variables. But what about pattern-matching? Patterns are possibly “deep”, i.e. they bind several variables at a time, and they don’t respect the usual discipline that a variable is bound for exactly its subterm in the AST.

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.

The ideas probably extends seamlessly to De Bruijn indices, by threading an explicit environment throughout the term. It stemmed from a discussion on LF encodings of pattern-matching with Francisco over lunch yesterday: what I will show enables also to represent adequately pattern-matching in LF, which I do not think was ever done this way before.

Read the rest of this entry »

Update on Typeful Normalization by Evaluation

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.

Read the rest of this entry »

Strong reduction in big steps

It has been a long while since I updated this blog, let me finally revive it with an easy but (hopefully) fun post, well ehm… at least some usable reference material!

Strong reduction is the ability for the interpreter of a functional language to reduce under function declaration. Usually, in OCaml for example, evaluation stops at the λ boundary; we might like to reduce under them for various reasons:

  • partial evaluation (e.g. λx. 2+2+x ⇒ λx. 4+x)
  • conversion checking in dependent type systems (is λx. (λy. y) x the same as λx. x?)

I never remember the big-step semantics of strong reduction, so I’m going to write them down here in glorious Unicode-art. Over the years I accumulated many small variants of reduction machines, both weak and strong, call-by-name or call-by-value… Here is a first shot, starting with the canonical, CBV weak head reduction and incrementally building up strong reduction; I’ll be probably extending this list when I remember other variants.

Read the rest of this entry »