I want to learn bidirectional type checking
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
See this amazing survey paper by and Neel K! This is what made it click for me.
cl.cam.ac.uk/~nk480/bidir-s
2
4
also highly recommend ’s /An Algebraic Approach to Typechecking and Elaboration/ which combines extremely well with bidi typechecking: bentnib.org/posts/2015-04-
1
3
you can also check 's reference implementations of dependently-typed languages:
github.com/AndrasKovacs/e
also seconding the offer of rambling about my implementation(s) of bidirectional type checking ^^
2
4
These are really good and I have been learning tons from them!




