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
Replying to
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/
1
4
1