3 ms·

Where can I get a good, intuitive explanation of what Type Theory really is?

by arjvik 5y ago

auggierose 5y ago
View it as a particular opinion of how collections should be formed. Now take this particular opinion and enforce it by mechanical rules, so that valid collections are exactly those that can be formed by these rules. Voila, you got your type theory. If you want to be really bold, start infusing a notion of construction and proof into your collections. Good luck with finding a good and intuitive explanation for that process.
stepchowfun 5y ago
I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use. I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it! If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

Where can I get a good, intuitive explanation of what Type Theory really is?

by arjvik 5y ago

Where can I get a good, intuitive explanation of what Type Theory really is?

View it as a particular opinion of how collections should be formed. Now take this particular opinion and enforce it by mechanical rules, so that valid collections are exactly those that can be formed by these rules. Voila, you got your type theory. If you want to be really bold, start infusing a notion of construction and proof into your collections. Good luck with finding a good and intuitive explanation for that process.

stepchowfun 5y ago

I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use. I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it! If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...