3 ms·
Agreed. This reminds me – and I wonder if it could be applied – to Computational Type Theory, which relies on a similar concept of "reducing" types to their pri
by simplify 2y ago
Agreed. This reminds me – and I wonder if it could be applied – to Computational Type Theory, which relies on a similar concept of "reducing" types to their primitive forms, actually taking computation into account (something type theories normally do not!)
This lecture series goes into how it works: https://www.youtube.com/watch?v=LE0SSLizYUI https://www.youtube.com/watch?v=LE0SSLizYUI
- deterministic 2y agoI watched all 5 videos a few years ago. And if I understand it correctly "Computational Type Theory" basically defines a type as describing the behaviour of a computation. Which is really interesting but kinda hard for me to wrap my arms around compared with Martin Loff type theory. It looks as if type checking will have to be done manual, using N axiomatic rules for how you can prove A from B. Is that your understanding as well? Also, there doesn't seem to be much material on Computational Type theory online. Any good references? (Except for the nuPrl book of course).