I've been using bidirectional type checking in my work quite heavily over the past year and a half. It's a really handy technique, and not too hard to get your head around! did a really nice presentation of it at :
Conversation
It's really nice that he explains the type theory notation up front, so if you were wanting to learn that, this is the place to go! Also check out:
- davidchristiansen.dk/tutorials/bidi
- andres-loeh.de/LambdaPi/
- davidchristiansen.dk/tutorials/nbe/
Replying to
Also, to understand why bidirectional type checking works, take a look at Frank Pfenning’s lecture notes. cs.cmu.edu/~fp/courses/15
3