Introduction to dependent match

Consider a match expression
   match e with
   | C1 => e1
   | C2 => e2
   | C3 => e3
   ...
   end

The usual typing rule for the above is quite simple. First, the match must be exhaustive, i.e., the patterns C1,C2,C3,... must cover all the cases. In other words, all the constructors for the type of e must be handled. Then, all the branches e1,e2,e3,... must be of the same type T. When this holds, the whole match expression is typed with type T. For instance:

Above, we handle both constructors for nat, namely zero and successor. Also, both branches true,false have type bool, hence the whole match has type bool, and isZero typechecks. This typing mechanism for match is indeed the one used in most functional programming languages. When proving theorems via the Curry-Howard isomorphism, e.g. in Coq, the above match typing rule is sometimes overly restrictive. Consider for instance:
Definition foo (P : nat -> Prop) (H0 : P 0) (HS : forall n, P (S n)) (x : nat) : P x :=
   ...

Intuitively, here P is a predicate on nat, and we need to prove P x for any x. We have as hypotheses, that P holds on 0 and S n for any n, so the proof should be a simple case analysis on x. We get:
Definition foo (P : nat -> Prop) (H0 : P 0) (HS : forall n, P (S n)) (x : nat) : P x :=
   match x with
   | 0 => H0
   | S n => HS n
   end

The above definition is very reasonable but it can not be typed using the match typing rule seen before! In fact, the first branch H0 has type P 0 while the second branch has type P (S n). Of course, one might object that in the first branch x is 0, while il the second x is S n, so both branches intuitively should be assigned the common type P x instead. This however requires a more sophisticated typing mechanism known as the "dependent match" typing.

Dependence on the value of the term being matched

We shall use a simple color type, containing only two colors.

Simple example for match .. as ..

Consider the definition below:

Coq accepts the above match. Why? The two branches have different types, namely P white and P black, violating the rule for match typing! The return type of match_as_0 is P (f white) which is even different from both! On further inspection, the definition is at least morally correct. For instance the first branch returns Hw which is of type P white instead of the claimed P (f white). This may look wrong, but we reach this branch only when f white is white, so there is no real difference between the expected and actual types. Similarly, the second branch is reached only when f white is black, so Hb of type P black can be thought to have type P (f white) as well. Intuitive reasons aside, how did Coq manage to type check the above match? Curiously, if we inspect the definition, we notice that Coq has added something to our code.

Notice the extra as x return (P x) part. This special match is used to state that the type of the whole match expression depends on the value of the term being matched f white. That is, the type of the match is P x, where x is f white. In other words, it is P (f white) which is what we need. What about type checking the branches? The idea is that when checking
      | white => Hw

we require that Hw has type P x where x is the value we are matching against, that is, white. So, Hw is checked against P white. Similarly,
      | black => Hb

makes Hb to be checked against P x where x is black, hence against P black. This form of match is called a "dependent match", indicating that the type for the whole match expression is dependent on the term being matched. Rough summary:

• The type for a match expression can be expressed as a function of the term being matched;
• The branches C => e are then checked by applying said function to C, hence obtaining a type, and then checking e against that.

Note that if the type-valued function is constant, as in
       match e as x return nat with ...

we get all the branches checked against nat. That is, we recover the typing of the non-dependent match. This shows that the regular match is indeed a special case of the dependent match. As a final remark, note that in the above case Coq was able to guess the function which related the value of the term being matched and the target type. Coq has some heuristics to help the user in this task. In the general case, however, the user has to define explicitly the function, annotating the dependent matches with as x return ... .

Dependent match: dependence on the type of the term being matched

Simple example for match ... in ...

This is a simple predicate on colors, which holds only on black

Consider this Coq definition, which does not pass type checking.
Definition match_in_0 (P : color -> Prop) (H : P black)
   (x : color) (H2 : isBlack x) : P x :=
  H
.

The above definition fails with

The term "H" has type "P black" while it is expected to have type "P x".

However, the above Definition is morally right. The match_in_0 function above takes as an argument H2 : isBlack x, so we know that x is actually black. Hence, the type error above complaining about the difference between P black and P x is just due to the type checker being overly restrictive here. How can we convince the type checker to accept the definition above? Let's try by matching over H2 which claims x is black.

Note the strange typing here:
       H : P black
       match H2 with B => H end : P x

The match intuitively returns the same value as H, yet inside a different type. We know this is OK since x must be black for H2 to exist, but why this match is allowed by Coq? Inspecting the match_in_0 term, we discover that Coq added something to our definition!

Note the extra in (isBlack c) return (P c) part. This is stating that the whole match expression has type P c where c is the color for which we have H2 : isBlack c. This means that c is x, hence the whole match has type P x. However, when in .. return .. is specified for a match, the typing of the match branches is done differently. Typing the branch
         | B => H

no longer requires H to have type P x as the whole match expression. Instead, H has to have type P c where c is the color for which we have B : isBlack c. Of course, we have B : isBlack black, so c is black, hence P c is P black. Rough summary:

• The type of "match A" can be expressed as a function of the type of A;
• Checking a branch "C => e" is done by applying said function to the type of the constructor C, and then checking e against this type.

Note that in out example above Coq was able to guess how to express the match type P x as a function of type of the matched term isBlack x. In the general case, however, Coq will not be able to define the function and the user has to provide it. This more sophisticated form of match is called a "dependent match". Here, the adjective "dependent" means that the returned type depends of the type of the object being matched. As a final remark, consider the case in which the function is constant, e.g,
         match H2 in isBlack c return nat with ...

In this case, every branch is checked to have type nat, and the whole match will have type nat. This shows that once again a regular match is just a special case of the dependent match of the in..return.. variant.

Advanced example for match .. in ..

Let's define a relation holding between opposite colors.

The following definition is morally correct but is not accepted by Coq.
Definition match_in_1 (P : color -> Prop) (H : P black)
                      (x : color) (H2: opposite white x) : P x :=
  H .

Coq complains with

The term "H" has type "P black" while it is expected to have type "P x".

While types P black and P x are syntactically different, the function above takes as an argument H2 : opposite white x, and this implies that x is actually black, so that the distinction between P black and P x is not a real one. Adapting the code above to pass the type checker is non trivial.

The above example intuitively transformed a P black value into a P x value, when we had a proof implying that x was black. The next example shows instead how to convert a P x into a P black, when holding the same proof. Surprisingly, this requires a bit more finesse.