Does anybody know of any calculus or other more formal exploration of conditional types a la TypeScript’s? or or maybe?
Conversation
A few things.
1. Recently, has been looking at related things.
2. This is easy to encode with full spectrum dependent types, or even limited versions as in Haskell.
3. I don't know of anything that has that exact feature.
1
3
Thanks for the overview. I’ve been meaning to implement a toy dependently types language to get a feel for it, maybe it’s time...
1
1
It's worth it! Makes the interplay between checking, inference, and evaluation much more clear. Would recommend having a look at some of these:
- davidchristiansen.dk/tutorials/nbe/
- andres-loeh.de/LambdaPi/
- math.andrej.com/2012/11/08/how