Bidirectionality Hints

Summary

An explanation of bidirectionlity hints. After presenting the requisite background on bidirectional typing and existential variables in Coq, we will see how bidirectionality hints affect type checking of function applications, and we will illustrate with simple examples.

Contents

• 1. Bidirectional typing
• 2. Bidirectional typing and existential variables
• 3. Bidirectionality hints
• 4. Examples

Before we explain what bidirectionality hints are, we must first understand some basics of how type checking works in Coq.

1. Bidirectional typing

Coq uses bidirectional typing, an approach to type systems that interleaves type checking with type inference. A bidirectional type system replaces the usual typing judgement e : T with two judgements: type checking e ◃ T where T is an input and type inference e ▹ T (also called type synthesis in the literature) where T is an output. Making inputs and outputs explicit enables an algorithmic interpretation of the typing rules: a bidirectional type system is a way to present a type checking and a type inference algorithm. Function application is usually associated with a rule for type inference (▹):

f ▹ forall (x : A), B x      a ◃ A	app-infer
f a ▹ B a

To infer the type of an application f a:

• 1. infer the type of the function f (f ▹ ∀ (x : A), B x), usually f is a constant whose type is known from its definition.
• 2. check the arguments a against the argument type A.
• 3. output the result type B a as the inferred type for f a.

What if we want to check with a type, rather than infer it? The following subsumption rule turns inference (▹) into checking (◃): to check that e has type T (e ◃ T), infer a type T’ (e ▹ T’), then unify T’ with T (T’ ≡ T).

e ▹ T’     T’ ≡ T	infer-check
e ◃ T

(Here we gave the subsumption rule using a type equality, or rather unification (T’ ≡ T). A more general variant of the subsumption rule uses subtyping instead, and in fact such a generalization lets us deal with coercions in Coq. For the rest of this explanation, we will ignore coercions and only talk about unification (T’ ≡ T) to keep it simple.) The two rules above combine into the following rule for checking an application:

f ▹ forall (x : A), B x
a ◃ A        B a ≡ T	(1)
f a ◃ T

To check whether the application f a has a given type T:

• 1. infer the type of f;
• 2. check the argument a against its type A;
• 3. unify the inferred result type B a and the checked one T.

2. Bidirectional typing and existential variables

To a first approximation, the unification judgement (T’ ≡ T) merely denotes an equivalence relation between types. This story is further complicated in Coq by the presence of existential variables. To avoid fully spelling out all terms, in Coq, you can write wildcards (_) instead and Coq will try to infer them. Wildcards are replaced with fresh existential variables with names like ?u during pretyping. Existential variables will then be instantiated by unification: when a unification problem such as ?u ≡ T is encountered, Coq will use this information to instantiate the variable ?u. Thus, the typing rules above are interpreted statefully: there is a global set of bindings for existential variables ?u := M which is read and updated during unification. In particular, the order in which unification judgements T’ ≡ T are evaluated matters. For example, consider the following two unification requests:
?u ≡ true
0 ≡ if ?u then 0 else 1

Unifying ?u ≡ true first allows the second unification to succeed since if true 0 else 1 reduces to 0. In contrast, unifying 0 ≡ if ?u then 0 else 1 will fail if we haven't instantiated ?u yet, because if ?u then 0 else 1 is stuck.

3. Bidirectionality hints

Bidirectionality hints indicate when unification with the result type should happen during type-checking of a function application. By default, that happens at the end, after having type-checked all of the arguments. This corresponds to the type checking rule above. A bidirectionality hint moves that unification step earlier. Intuitively, that allows information about a function expected result type to be propagated to type check its arguments. For instance, to type check the application f _ b of a polymorphic function f : ∀ (x : A), B x → C x, knowing that the result type is C T for some T, we may want to infer that the first argument _ should be T and check that the second argument b has type B T. However, by default, without a bidirectionality hint, the result type C T will be ignored at first, and b will be checked against a type B ?x containing less known information. Earlier, we showed the type checking rule for a function application with one argument. While function applications with multiple arguments f a b are technically multiple nested applications (f a) b, for the purposes of type checking in Coq, they are treated as a single n-ary application. For example, the rule for type checking an application with two arguments f a b looks like this:

f ▹ forall (x : A), B x -> C x
a ◃ A     b ◃ B a     C a ≡ T	(2)
f a b ◃ T

(For more generality, you could reformulate that typing rule with the more dependent function type ∀ (x : A) (y : B x), C x y, and also with more arguments. We will stick to this simpler form as our running example.) In other words, we check whether the application f a has a given type T following these steps:

• 1. infer the type of f;
• 2. check the first argument a against its type A contained in the type of f;
• 3. check the second argument b against its type B a (that is B x from the type of f with x replaced by a);
• 4. unify the result type C a and T.

The unification of the result types is the last step by default. That behavior can be modified using bidirectionality hints. Bidirectionality hints are declared using the Arguments command, as a & symbol. For example:
Arguments f _ & _.

This hint f _ & _ makes unification happen after type checking the first argument, instead of at the end, resulting in the following type checking rule:

f ▹ forall (x : A), B x -> C x
a ◃ A     C a ≡ T     b ◃ B a	(2)
f a b ◃ T

4. Examples

Let us demonstrate the difference with two examples: one does not require the hint, the other does. Both use the same concrete definitions for the types A, B, and C below, where B and C pattern match on the first argument x : A:

The expression f _ (0 : B false) : nat type checks without bidirectionality hints, but fails with the hint f _ & _. With no bidirectionality hint, type checking f _ (0 : B false) ◃ nat proceeds as follows:

• 0. generate a fresh existential variable ?x in place of the wildcard _;
• 1. check the first argument ?x ◃ bool: do nothing (actually, bool gets unified with the type of ?x, which is another fresh existential variable, but that is not an important detail for this explanation);
• 2. check the second argument (0 : B false) ◃ B ?x: the type annotation gives us the inferred type B false, which is unified with the checked type B ?x, and we unify false with ?x (note that this unification step happens even if B is not injective: in general, B false ≡ B ?x does not imply false ≡ ?x; unification in Coq is lossy, it does not aim to find most general unifiers);
• 3. unify the result types C ?x ≡ nat: it succeeds because we previously unified ?x with false.

With a bidirectionality hint, type checking proceeds as follows:

• 1. check the first argument ?x ◃ bool: same as before;
• 2. unify the result types C ?x ≡ nat, that is (if ?x then bool else nat) ≡ nat, which fails because ?x is still unknown.

The expression f _ 0 : C false type checks with the hint f _ & _ but fails without. With no bidirectionality hint:

• 1. check the first argument ?x ◃ bool: same as before;
• 2. check the second argument 0 ◃ B ?x: 0 is a constant so its type can be inferred as nat, which is unified with the checked type B ?x, and that fails because ?x is still unknown.

With the bidirectionality hint:

• 1. check the first argument ?x ◃ bool: same as before;
• 2. unify the result types C ?x ≡ C false, which unifies ?x ≡ false;
• 3. check the second argument 0 ◃ B ?x: its type is inferred as nat, which is unified with the checked type B ?x, and that succeeds we previously unified ?x with false.