Questions tagged [bidirectional-typing]

Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program.

Filter by
Sorted by
Tagged with
12 votes
0 answers
147 views

How do Coq's bidirectionality hints (`&`) affect type checking?

I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. ...
user avatar
  • 497
15 votes
2 answers
843 views

What is bidirectional type checking?

What is bidirectional type checking and why would I want to implement it? It feels like the name is a bit of a misnomer and the syntactic separation kind of resembles stuff like ANF, call by push ...
user avatar