Explanation about bidirectionality hints #71
Conversation
|
I am going to ask @MevenBertrand to review as he is a specialist of bidirectional typechecking. |
There was a problem hiding this comment.
Thanks very much for writing it. It is a great addition on sth I know nothing of. Actually, I was not even aware of it.
I am reviewing it as an non-expert reviewers, so I tried to point out stuff that got me a bit confusing while reading.
Globally, I thought part 1 to 3 was a really good intro to the subject.
Concerning section 4, it depends on what you/we want to go with this.
As you mentioned, right now, it is more an explanation than a tutorial, because it just explains how it works and that it is.
I personally think it is a bit too bad, because at the end, you understand what are "bidirectional hints" but you have no idea when and how to use them.
That would be great if it were possible to modify the part 4 to help the user understand that.However, I have no idea how to do that, so I can't say much.
What do you think ? Note if no one has an example in mind, it can perfectly be merged like that, in which can we can create an issue to improve it latter.
| (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. |
There was a problem hiding this comment.
It would be good to add a comment explaining why because otherwise it sounds a bit like it is an arbitrary choice whereas from what I understand from my readings is that it is instrumental in making type checking decidable
There was a problem hiding this comment.
no
in fact the kernel is not bidirectional, only pretyping is bidirectional
I think pretyping has nontrivial "check" mode (ie not just "infer then coerce to expected type") for
- functions (eg if
f : (A -> B) -> Candfoo : A' -> B, pretypingf (fun x => foo x)will pretypefoo xwithx : Ainstead of an evar, then (if there is no coercionA >-> A') it can produce a type errorx has type A but A' was expectedinstead of instantiating the evar and later producing"fun x : A' => foo x" has type "A' -> B" instead of "A -> B") matchelaboration uses the type constraint in nontrivial ways- holes having a type constraint means you can avoid generating an extra evar for the hole's type which probably matters for efficiency
- tactics in terms (
ltac:(trivial) : Aonly runstrivialin goalAwith bidirectionality, without it the goal would be a fresh evar)
There was a problem hiding this comment.
in other words the benefits of bidirectionality in Coq are better type errors and better hole inference
|
|
||
| To start, we must understand the basics of how type checking works in Coq. | ||
|
|
||
| ** Bidirectional typing |
There was a problem hiding this comment.
| ** Bidirectional typing | |
| ** 1. Bidirectional typing |
| 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 ([↑]): |
There was a problem hiding this comment.
Maybe recall the usual type checking rule and explain how it is transformed ?
| - 2. check the arguments [a], [b] with their respective types [A], [B a]; | ||
| - 3. unify [C a] and [T]. | ||
|
|
||
| ** Existential variables |
There was a problem hiding this comment.
| ** Existential variables | |
| ** 2. Bidirectional Typechecking and Existential variables |
| *** Contents | ||
|
|
||
| - 1. Bidirectional typing | ||
| - 2. Existential variables |
There was a problem hiding this comment.
| - 2. Existential variables | |
| - 2. Bidirectional Typechecking and Existential variables |
| Bidirectionality hints are declared using the [Arguments] command, | ||
| as a [&] symbol. For example: | ||
| [[ | ||
| Arguments f _ & _. |
There was a problem hiding this comment.
This is linked to applications being n-ary in Coq.
It is not mentioned, maybe it is worth saying somewhere ?
| ]]] | ||
| *) | ||
|
|
||
| (** ** Examples *) |
There was a problem hiding this comment.
| (** ** Examples *) | |
| (** ** 4. Examples *) |
| - 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`; |
There was a problem hiding this comment.
Not sure what happens here but it sounds a bit weird to me, because it seems to say it uses injectivity of B ?
There was a problem hiding this comment.
unification uses the first-order unification heuristic ie avoids unfolding B when unifying its arguments is enough to succeed
|
|
||
| (** With no bidirectionality hint: | ||
| - 1. check the first argument [?x ↓ bool] (same as before, do nothing); | ||
| - 2. check the second argument [0 ↓ B ?x]: it is a constant so it has an inferred type `nat`, |
There was a problem hiding this comment.
| - 2. check the second argument [0 ↓ B ?x]: it is a constant so it has an inferred type `nat`, | |
| - 2. check the second argument [0 ↓ B ?x]: [0] is a constant so its type can be inferred, here to `nat`, |
| (** With the bidirectionality hint: | ||
| - 1. check the first argument [?x ↓ bool] (same as before, do nothing); | ||
| - 2. unify [C ?x ≡ C false], which unifies [?x ≡ false]; | ||
| - 3. check the second argument [0 ↓ B ?x]: it has an inferred type `nat`, |
There was a problem hiding this comment.
| - 3. check the second argument [0 ↓ B ?x]: it has an inferred type `nat`, | |
| - 3. check the second argument [0 ↓ B ?x]: its type is inferred to `nat`, |
I agree completely. As it is, this explanation works best for people who already have a little idea of what the feature does.
I remember one common situation that calls for bidirectional hints is with dependently typed records. I can add a paragraph about that, maybe even lead with it, but it might not be a deep example that turns it into a tutorial. |
|
You can also ask on zulip for examples, maybe someone has ideas. |
| {{https://coq.inria.fr/doc/V8.20.0/refman/language/extensions/evars.html} existential variables}. | ||
| To avoid fully spelling out all terms in Coq, you can write | ||
| holes ([_]) instead to let them be inferred. They are replaced with fresh | ||
| existential variables with names like [?u] right before type checking. |
There was a problem hiding this comment.
I would say during pretyping, not right before anything (I'm not sure if what you call type checking is meant to be pretyping or the kernel check, for this sentence the kernel doesn't see evars so I guess it can't be the kernel check)
|
|
||
| (** We replace the hole in the first argument with a fresh existential variable [?x]. | ||
| With no bidirectionality hint, type checking [f _ (0 : B false) ↓ nat] proceeds as follows: | ||
| - 1. check the first argument [?x ↓ bool]: it is a hole so checking succeeds without doing anything; |
There was a problem hiding this comment.
as I said holes are turned into evars during pretyping not before it, so we actually do check _ bool ==> ?x : bool generating a fresh evar
|
|
||
| [[[ | ||
| f ↑ forall (x : A), B x -> C x | ||
| a ↓ A C a ≡ T b ↓ B a |
There was a problem hiding this comment.
there is a subtlety here
after a ↓ A we know that f a : forall y : B a, C a
we could in principle check that y is not bound in C a before trying to unify C a and T
however in pretyping it is rare that we directly call "unify a and b", instead we usually want "coerce c : a to b"
this cannot be done without having a term c
(in fact it is not really right to write c ↓ T, it should really be something like "check input preterm c at input type T producing output term c'", similarly infer has an input preterm and output term and type)
so what we do is, regardless of if y is bound in the codomain:
- generate a fresh evar
?y : B a - coerce
f a ?y : C a(whereC ais the result of substitutingy := ?yinC a) toT(which first tries unifyingC atoTand if that fails tries to find a coercion to insert)
note that ifywas bound inC athis could instantiate?y - check
b ↓ B a - unify
?yandb(this time it really is unification not coercion) - produce term
f a b : C a(which is more faithful to what the user wrote thanf a ?yif coercing toTinstantiated?y, but theC ais still from substituting?ynotb) and replay any coercions toT
I think it's an explanation rather than a tutorial but I'll be happy to defer to you if you think otherwise.