4
$\begingroup$

So I'm working on type checking of an expression that pattern matches on terms, like case x of in Haskell. My question is, suppose we have case x of { X => ? } where:

  1. x is a variable
  2. X is a pattern
  3. There are other variables in the context whose type uses x

When we are at ?, should we replace x in the types from the context with X? In other words, should pattern matching expression update the context?

I have the impression that Agda does this, but this does not scale to arbitrary expressions (being matched), like a function call. Is it a good idea to keep the context as-is? If so, what is the recommended approach to update the context, given that the user really wants to do so?

$\endgroup$
2
  • $\begingroup$ Does agda even have case expressions? I thought they are emulated by clausal definitions plus function applications. $\endgroup$
    – Trebor
    Oct 27 at 14:08
  • $\begingroup$ Yes, Agda sugarize these things, but is it a good idea? $\endgroup$
    – ice1000
    Oct 27 at 22:51

1 Answer 1

4
$\begingroup$

I would say that having a pattern-matching construct that works differently depending on whether its scrutinee is a variable or a more complex expression sounds like a very ad-hoc thing to do. It might be reasonable as a feature of elaboration, so that the user can still have it if they wish, but I would steer away from it in the "core" language, as it would entail a lot of special-casing whenever you write code for pattern-matching.

Although this also depends on the kind of system you envision: if you aim for something Coq-like, with a quite simple core syntax but a complex elaboration layer and heavy manipulation of proof terms, then I would definitely keep the core syntax simple. If you wish to have a more Agda-like system, with a rather shallow elaboration and not many term manipulation, then maybe it is worth it.

There are multiple patterns you can use to emulate your feature, that mainly work by interleaving the case in the middle of a β- or ι-redex (what I have heard called a "commutative cut", I think the name comes from the linear logic literature). A simple one is to abstract over the context variables you want to make more precise: if the context is say x : nat, v : Vect bool x, you can build case x of { 0 => fun (v' : Vect bool 0) => … | S n => fun (v' : Vect bool (S n) => …} v. In each branch v' can be used instead of v, with its type properly refined. Note that this is not specific to v being a variable in the context, it can really be any term whose type you want to refine. In particular, you can do the following: case x of {p => fun (e : x = p) => …} eq_refl and in the branch use e to showcase the fact that x has been refined. This is usually called the convoy pattern, name coined in Chlipala's Certified Programming with Dependent Types. Note that both these approaches work even in the scrutinee is not a variable.

In the Coq ecosystem, the state of the art of compilation of complex, Agda-like clausal definitions to simple pattern-matching is the Equations plugin. If you want to learn more about the question of giving a high-level user interface compiled down to a simple pattern-matching primitive, the library and the Equations Reloaded paper might be worth a look.

$\endgroup$
1
  • $\begingroup$ The convoy pattern is sooo cool! $\endgroup$
    – ice1000
    Oct 28 at 21:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.