I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. Despite familiarity with bidirectional type checking, I can't connect the explanation given in the documentation with what I actually observe. So, precisely what change does & make to the checking of an application? To start, I understand the default bidirectional typing rule for applications to be, more or less (read clockwise, with denoting type synthesis and denoting subtyping (including unification)):

f ∈ ∀ (x1 : A1) ... (xn : An), B
M1 ∈ A1'    ...    Mn ∈ An'
A1' ≤ A1    ...    An′ ≤ An
f M1 ... Mn ∈ B[M1/x1, ..., Mn/xn]

Some questions I'd like to be answered as corollaries of the explanation:

  1. Is Arguments foo & x y. equivalent to Arguments foo x y.?
  2. Is Arguments foo x y &. equivalent to Arguments foo x y.?
  3. Is Arguments foo {x} & y. equivalent to Arguments foo & {x} y.?
  4. What happens for partial applications (of Curried functions)?
  5. Is the Arguments f ... & ... . mechanism reasonably complete for bidirectional typing strategies you may want/expect?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.