Typing dependent pattern matching

I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing

match e with
| C_1 a_1_1 a_1_2 ... a_1_n1 -> e_1
| C_2 a_2_1 a_2_2 ... a_2_n1 -> e_2
| ...
| C_m a_m_1 a_m_2 ... a_m_nm -> e_m
end

be, where e is of type T, which has constructors C_i for each i.

I think that to prove that the pattern match has a type T', we need to prove that each e_i has type T' under specific assumptions, but I can't quite pinpoint those assumption to add into the context.

• You'll need to know the types of each C_i and in particular what it's arguments are, but that's not the hard part. The hard part is that a type may be indexed over certain type arguments so that when you pattern match you restrict what they could be. – jozefg Jan 15 '16 at 16:12
• OK, do you happen to know of a book/article that covers this in detail? – Guido Jan 15 '16 at 16:50
• Peter Dybjer has a number of papers on the subject, I think you might find his work on indexed inductive types helpful and relevant. cse.chalmers.se/~peterd/papers/Indexed_IR.pdf I think covers everything you would find with dependent pattern matching in Agda for example. – jozefg Jan 15 '16 at 17:19

In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is

match t as x in T1 return T2 with
| C1 a1 ... an
...

In particular, ommiting any of the as, in or return clauses can prevent type inference of the statement.

Intuitively, if the type of (say) constructor $C_1$ is $$\Pi(x_1:A_1)\ldots(x_k:A_k).I\ \vec{p}$$ and the type of the matched term $t$ is $$I\ \vec{v}$$ then you get the constraint $$\vec{p}[\vec{a}/\vec{x}]\simeq \vec{v}$$ which may lead to an undecidable problem, as explained in Goguen et al.

Then all you need is for each right hand side to correspond to the appropriate instance of the return type. This return type may depend on $t$, so the return clause specifies the pattern of the return type as a function of $x$ (which represents $t$ through the as clause).

More formally, each $e_i$ must have type:

$$T_2[C_i\ \vec{a}/x]$$

and the type of the whole match expression is $$T_2[t/x]$$

More details can be found here.