I’ve found bidirectional type checking is indeed a very handy technique for making expressive type systems quickly. I haven’t yet mastered how to marry it with constraint based inference (for implicit arguments) but it proved to be very useful when starting out on building Pikelet.
Let Arguments Go First is another interesting paper that adds an ‘application mode’ that allows you to pull more type information from argument applications. I’m hoping to try to implement that too at some stage!
https://www.youtube.com/watch?v=21bUrFEX4jI
Conor talks a fair amount about this in this video too.
I’ve found bidirectional type checking is indeed a very handy technique for making expressive type systems quickly. I haven’t yet mastered how to marry it with constraint based inference (for implicit arguments) but it proved to be very useful when starting out on building Pikelet.
David Christiansen has a somewhat more acessible intro here. It’s also used in the LambdaPi paper which Pikelet was originally based off.
Let Arguments Go First is another interesting paper that adds an ‘application mode’ that allows you to pull more type information from argument applications. I’m hoping to try to implement that too at some stage!