4 ms·
Somewhat related, "A Little Taste of Dependent Types," implemented in Racket: https://youtu.be/VxINoKFm-S4 https://youtu.be/VxINoKFm-S4
by cercatrova 4y ago
Somewhat related, "A Little Taste of Dependent Types," implemented in Racket:
https://youtu.be/VxINoKFm-S4 https://youtu.be/VxINoKFm-S4
- tluyben2 4y agoThat's basically this[0] book, is it not? Great book (the entire series) by the way. [0] https://thelittletyper.com https://thelittletyper.com
- fithisux 4y agoA bit pricey for people not in US.
- Hirrolot 4y ago"Checking Dependent Types with Normalization by Evaluation: A Tutorial" [1] This one is cool too, I believe from the same author. I've read it recently and it makes pretty clear the intuition behind dependent types implementation. [1] https://davidchristiansen.dk/tutorials/nbe/ https://davidchristiansen.dk/tutorials/nbe/