4 ms·

Propositions as Types (2014) [pdf]

michaelsbradley 11y ago
This paper was recommended to me yesterday evening, when I expressed difficulty in fully understanding section 6.9 in the PureScript book: https://leanpub.com/purescript/read#leanpub-auto-nullary-type-classes 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.
- harveywi 11y ago
  The introduction and chapter 1 of the (free) homotopy type theory book (http://homotopytypetheory.org/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.
  - michaelsbradley 11y ago
    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?
    - harveywi 11y ago
      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. http://diginole.lib.fsu.edu/cgi/viewcontent.cgi?article=1357&context=uhm http://diginole.lib.fsu.edu/cgi/viewcontent.cgi?article=1357... If you find anything else, let us know!
chrislloyd 11y ago
If you're finding the paper too dense, Philip gave a extremely entertaining talk on the same subject at Strange Loop this year: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
- jcox92 11y ago
  +1 Probably my favorite talk at Strange Loop this year. It's worth watching just for the minute or so starting here: https://www.youtube.com/watch?v=IOiZatlZtGU&t=33m https://www.youtube.com/watch?v=IOiZatlZtGU&t=33m

This paper was recommended to me yesterday evening, when I expressed difficulty in fully understanding section 6.9 in the PureScript book: https://leanpub.com/purescript/read#leanpub-auto-nullary-type-classes 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.

harveywi 11y ago
The introduction and chapter 1 of the (free) homotopy type theory book (http://homotopytypetheory.org/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.
- michaelsbradley 11y ago
  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?
  - harveywi 11y ago
    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. http://diginole.lib.fsu.edu/cgi/viewcontent.cgi?article=1357&context=uhm http://diginole.lib.fsu.edu/cgi/viewcontent.cgi?article=1357... If you find anything else, let us know!

chrislloyd 11y ago

If you're finding the paper too dense, Philip gave a extremely entertaining talk on the same subject at Strange Loop this year: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

jcox92 11y ago
+1 Probably my favorite talk at Strange Loop this year. It's worth watching just for the minute or so starting here: https://www.youtube.com/watch?v=IOiZatlZtGU&t=33m https://www.youtube.com/watch?v=IOiZatlZtGU&t=33m