Re:Propositions as Types (2014) [pdf]
by harveywi on Saturday November 14, 2015 @07:39AM
(#10565450)
The introduction and chapter 1 of the (free) homotopy type theory book (http://homotopytypetheory.org/book/) provide a great overview of type theory and the Curry-Howard correspondence which, for me, was the moment when I developed a deep appreciation for (non-broken) type systems.
Many of us are probably only exposed to type systems through, say, Java. This is unfortunate because Java's type system is rather primitive, and limits one's ability to take full advantage of Curry-Howard. Scala provides a good environment for developing some introductory experience with type-level programming, since it is sort of halfway* between Java and a dependently-typed programming language like Idris.
*=Scala has higher-kinded types, path-dependent types (weaker than dependent types, but allows you to see what all the fuss is about), existential types, and implicit arguments - many of the ingredients that you will find in many theorem provers and proof assistants which, interestingly, rely on type theory (via Curry-Howard). Java has none of those.
Re:Propositions as Types (2014) [pdf]
by michaelsbradley on Saturday November 14, 2015 @10:56AM
(#10566035)
Thank you, I'll definitely consider the HoTT book. Are there any "background material" or "first course" books you'd recommend reading before starting the HoTT book?
Re:Propositions as Types (2014) [pdf]
by harveywi on Saturday November 14, 2015 @11:48AM
(#10566247)
Lawrence H. Dunn III from FSU put together a really nice honors thesis that provides a gentle overview of HoTT. The author was an undergrad math student, so there might be a couple mistakes here and there, but the text was quite accessible.
https://leanpub.com/purescript/read#leanpub-auto-nullary-typ...
It's certainly opening my eyes to a deeper understanding of the nature and role of the type system.
Many of us are probably only exposed to type systems through, say, Java. This is unfortunate because Java's type system is rather primitive, and limits one's ability to take full advantage of Curry-Howard. Scala provides a good environment for developing some introductory experience with type-level programming, since it is sort of halfway* between Java and a dependently-typed programming language like Idris.
*=Scala has higher-kinded types, path-dependent types (weaker than dependent types, but allows you to see what all the fuss is about), existential types, and implicit arguments - many of the ingredients that you will find in many theorem provers and proof assistants which, interestingly, rely on type theory (via Curry-Howard). Java has none of those.
http://diginole.lib.fsu.edu/cgi/viewcontent.cgi?article=1357...
If you find anything else, let us know!