In my final year of college, I was working on a toy project named ShiTT (I rewrote it completely half a year ago), which is a dependent type checker in Agda style based on András Kovács’ elaboration-zoo, with dependent pattern matching (DPM) support. And I feel that I need to write a blog post to share some of the interesting ideas I came up.

One of the challenging problems I encountered was how to implement DPM in NbE settings. As we know, implementing DPM needs to unify the terms and when matching the pattern against the type . This process is to build a substitution and apply it to the body of the pattern matching. However, in NbE implementations, we usually have no simple way to substitute.

A Naive Solution

Take elaboration-zoo/02-typecheck-closures-debruijn for instance, there is an evaluation environment where contains the values of all variables. An intuitive way to do DPM is to modify the evaluation environment by changing the value of the unified variable. For example,

If the placeholder is a variable pattern , the type checking context of should be,

and the evaluation environment should be,

If is the constructor pattern , then the evaluation environment should be,

Then all the occurences of in RHS will directly evaluate to . But this approach comes with a problem: this kind of unification will break the wellformedness of the evaluation environment. The evaluation environment stores the values of all variables. And the type can be considered as a representation for the normal forms. We changed the value of from a variable to an other value, which might make some of other variables that depends on to be ill-formed. e.g. if there is a variable in the evaluation environment, after we change to , the value of will be , which is not a normal form, which will make other variables depend on also ill-formed, and so on.

A Better Solution

A workaround for this problem is to update the environment every time we need to unify two terms.

For example, we have a well-formed evaluation environment , such that . And we have a unification assignment where is a value. We have shown that directly substituting for in will fail. Instead, we introduce a new operation, I call it

Here implies that the environment need not to be well-formed. There might be a smarter way to implement without quoting it back, but let us just use this for now.

One can imagine as a substitution operation on . e.g. , here is the naive substitution of for in the environment (which, as we have seen, is not well-formed).

Then, we can map to every value in . We call this operation .

Thus we obtain . Is well-formed and is it the environment we want?

The answer is yes.

We can define the ill-formedness of an environment with a level parameter. For a value under an environment , if for any free variable in , , we say is well-formed or say it is -ill-formed. If there is a free variable in such that and is -ill-formed, then we say is -ill-formed. An environment is -ill-formed if it contains a value that is -ill-formed. For example,

We can prove that if is -ill-formed, then is -ill-formed.

If is well-formed, and and there are some other variables in depending on , then it is easy to see that is -ill-formed. And after applying on it we get a well-formed environment.

Let us rewrite the type of to make it more clear,

Where indicates the level of ill-formedness.

And also, don’t forget to using the updated environment to update all the types in type checking context as well.

A Limitation of Dependent Pattern Matching

This approach comes with an efficiency problem. Every time we need to unify two terms, we re-evaluate the whole environment, which is quite expensive. A workaround is to limit the length of the context. One can write the following Agda code,

module M (x : Nat) where 

  f : Id x 0 → ... 
  f refl = ...

A function has ability to unify the outer module variable . We can limit the ability of dependent pattern matching in ShiTT by only allowing it to unify the variables that are introduced in the current function (Well, I haven’t done it yet). So we rewrite the above code as,

module M (x : Nat) where 

  f' : (x : Nat) → Id x 0 → ...
  f' x refl = ...

  f = f' x

For a language with match expressions support, there is an extra reason to do this restriction. LightQuantum occurred this to me.

If we have the following data type,

data T : Set → Set where 
  C : T Bool 

And we have a function with a match expression,

f : (A : Set) → T A → A 
f A = λ t → match t with 
            | C => true -- here A = Bool

And we can define,

g1, g2 : T Nat → Nat 
g1 = f Nat

g2 = λ t → match t with 
           | C => true

g1 is well-typed, while g2 is not, but one can find that g2 = f A [Nat / A] = g1. Substitution does not preserve typing!

The solution is as same as before, we limit the ability of dependent pattern matching by requiring all the unifying variables must in match expressions. So the above code will be rewritten as,

f A = λ t → match A , t with
            | .Bool , C => true

After that, g2 ≠ f A [Nat / A] anymore, and it is not well-typed as expected.

All though Agda have no native support for match expressions, but it has lambda-case expressions which lead to the same problem. But seems they consider the lambda-case is a syntactic sugar for top-level pattern matching, which means the substitution is still type-preserving for Agda expressions (Since there is no pattern matching in Agda expressions).

Upon those two reasons, I think it might be a good idea to limit the ability of dependent pattern matching.

References

• me🫡. ShiTT
• András Kovács. elaboration-zoo
• Ulf Norell. Towards a practical programming language based on dependent type theory
• Jesper Cockx and Andreas Abel. Elaborating Dependent (Co)pattern Matching

There are some old blog posts that I wrote before I started using Kodama. You can find most of them in my Zhihu profile.