Blog [blog]

    1. A Way to Implement Dependent Pattern Matching with Normalization by Evaluation [blog/dpm-nbe]

    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 Limited Version 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.

    Update. Apr. 10. 2026

    I just realized that the match expression example is wrong, the above code is also not well-typed under substitution. The final solution is to use lambda-case only (or equivalently, only allow matching on variables), and forbid unification on outer variables. So the above code will be rewritten as,

    f = λ { A C -> true } : (A : Set) → T A → A

    And lambda case only reduces when it is fully applied.

    Update. Apr. 24. 2026

    Turns out Rocq’s match-in-return-with expressions work just fine, no such problem as I mentioned above.

    I so silly.

    References

    2. Syntax for pattern matching QIT (and maybe HIT) in OTT (and maybe HOTT) [blog/qit-syntax]

    • 2026/8/10

    By OTT, we mean Loïc Pujet and Nicolas Tabareau’s Impredicative Observational Equality.

    A type   a : A   b : A 
------------------------
    a ~_A b : Prop

cast A B : A ~_U B → A → B

    Open Data Types

    In OCaml (and a proposal of Haskell), there is a feature alowing you to extend a data type with new constructors. Which is called “Extensible Variant Types” in OCaml, and “Open Data Types” in Haskell. For some reasons, it is never supported by GHC.

    In OCaml, the eliminator (pattern matching) of an extensible type should always have a default case for the future extended constructors. While in Haskell, the eliminator of an open data type is an open function, a function defined with pattern matching that can adding new clauses. For example

    open data Expr = Add Expr Expr 

open pp : Expr → String 
pp (Add a b) = pp a ++ " + " ++ pp b 

data Expr += Lit Int 
pp (Lit x) = show x

    Those features can work perfectly with Agda style pattern matching syntax.

    A Syntax for QIT in Non Cubical TT

    In CuTT (and XTT), A HIT should be considered as an inductive type with “boundary conditions”, and functions should eliminate such types with respect to the conditions. But in OTT, we do not have such thing.

    Basically, this note works out a syntax for, 1. how to define a QIT 2. how to eliminate it.

    Define a QIT

    Suppose there are indexed inductive types Eq_A a b : Prop over all QIT A where a b : A. (Note. For cubical indexed inductive types, we need to add a new constructor transpX. In OTT, we need the similar thing, but Eq is a irrelevent proposition family, we can omit that on it, because we do not need to compute a proposition)

    The observational equality ~ computes to Eq when acting on QIT. i.e.

    a ~_A b = Eq_A a b    for QIT A.

    Thus we can translate a QIT, for example, the interval as follow,

    data I : Type where 
  i0 i1 : I 

data EqI : I → I → Prop where 
  seg : i0 ~ i1

    For indexed inductive types,

    data Ty : Cx → Type where 
  ... 
  _[_] : {G D : Cx} → Ty D → Sb G D → Ty G 

data EqTy {G : Cx} : Ty G → Ty G → Prop where 
  ...
  id[] : A [ id ] ~ A

-- A ~_{Ty G} B = EqTy {G} A B

    The sur-syntax is as usual,

    data I : Type where 
  i0 i1 : I 
  seg : i0 ~ i1 

data Ty : Type where 
  ... 
  _[_] : {G D : Cx} → Ty D → Sb G D → Ty Γ
  ... 
  id[] : A [ id ] ~ A

    Eliminate a QIT

    We define an open indexed inductive type,

    A : U i   x : A ⊢ B : U j 
----------------------------- Formation
 '(x : A) → B : U (imax i j)

    f : '(x : A) → B    a : A
--------------------------- Elimination
f $ a : B [ a / x ]

    Sometimes we omit $, just write f a.

    The introduction and computation rules are generated by pattern matching functions. For example, when we have the following definition,

    add : ℕ → ℕ → ℕ 
add zero    y = y
add (suc x) y = suc (x + y)

    We actually defined,

    add : 'ℕ → ℕ → ℕ -- an introduction rule, so add is a constructor
(add $ zero) = λ y → y -- a computation rule
(add $ (suc x)) = λ y → suc (add x y) -- a computation rule

    The elaborator should insert ' and $ automatically.

    Note. ($) is an open function.

    We have another open function for '(x : A) → B

    apd : (f : '(x : A) → B) (e : u ~_A v) → cast B[u] B[v] (ap B[_] e) (f u) ~ f v

    apd is a trivial function and can be automatically generated, if A is just a non-quotient inductive type. So we focus only on the case when A is a QIT.

    Every time we pattern match a QIT, e.g.

    f : 'I → Bool 
f $ i0 = true
f $ i1 = true

    Then apd is lacking a clause for f.

    apd f (e : a ~_I b) = ...

    we can split on e, because a ~_I b is a inductive type (Eq_I).

    apd f (seg : i0 ~_I i1) = ... : f i0 ~_Bool f i1

    f i0 = true = f i1, so the hole can be filled by refl

    apd f seg = refl

    I hope all of these can make sense in some way, and I will try to write a experimental implementation of it to see if it works. XD

    Examples

    ===============

      F : I -> Bool -> Bool
  F i0 true = true 
  F i0 false = false
  F i1 true = true 
  F i1 false = false

  find elimination F : 'I -> Bool -> Bool
  missing apd clause
    apd {a} {b} F (e : a ~_I b) : F a ~ F b

    ===============

      f : I -> I -> Bool
  f i0 i0 = True
  f i0 i1 = False
  f i1 i0 = True
  f i1 i1 = False

  find elimination f : 'I -> I -> Bool
  missing apd clause
    apd {a} {b} f (e : a ~_I b) : f a ~ f b 

  find elimination f (x : I) : 'I -> Bool
  missing apd clause 
    apd {a} {b} (f x) (e : a ~_I b) : f x a ~ f x b

  x can be further eliminated in apd
    apd {a} {b} (f i0) e = ...
    apd {a} {b} (f i1) e = ...

  no need to proof congruence for apd

    in apd POV, f and F are constructors in pattern matching sense we don’t need to prove congruence if the target of elimination is a prop

    Intuition:

    • '(x : A) -> B is an open indexed inductive type, indexed by A and x.B,each functor defined with pattern matching on A is a constructor to this type.
    • a ~_A b is an indexed inductive type over A,each quotient path is a new constructor to this type.
    • apd is an open function eliminating '(x : A) -> B and a ~_A b, for quotient inductive type A.when '(x : A) -> B is extended, the apd function should also be extended with new clauses,which corresponds to the congruence.

    3. Old Blog Posts [blog/old]

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