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

Tag: pattern-matching

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 »


1 ≠ 0

Learning Coq is usually an enlightening experience. I know it first-hand, it can also be a quite frustrating one, because it seems at first to involve remembering quite a lot of arbitrarily-named tactics, that one might not fully understand the effect of. discriminate is one of them: “if you’re faced with an obvious inequality, just apply discriminate” they say. If you look at the proof term, however, it is far from trivial and involves a “trick”, a kind of “lie” that Pierre has become a specialist of. There is an intermediate step in the comprehension, that we put together with Chantal: decomposing the proof generated by discriminate. Here is a very easy proof that 1 ≠ 0, which does not require to understand neither proof terms nor return clauses in pattern-matching. Pure beginner Coq.
Read the rest of this entry »