1. 32

  2. 7

    I think programmers are commonly averse to this, but I do wonder what a more pared down and directed/ordered pedagogy would look like for learning type theory.

    Any recommendations @jozefg?

    1. 8

      I’d say there’s some variance but the general pattern would be

      • One good introductory book
      • Several introductions to more advanced topics
      • Classic papers in area of interest

      By 3 you have a solid grasp on TT and can learn things more piece-by-piece. I’d probably suggest

      • PFPL
      • Frank Pfenning’s notes/Pierce’s CT book + Ed Morehouse’s notes/Advanced Topics in Types and Programming Languages
      • Papers I listed (particular Martin-Lof, Reynolds', and Girard’s papers which I will add ASAP)

      The issue for me finding more of the second bullet point. Once I do that I’ll probably add some procedure like this to the “Reading Recommendations” sections.

      Was that more what you’re looking for?

      1. 4

        That helps, but isn’t quite what I meant.

        I mean figuring out what introduction to type theory works for the unschooled vs. mathematically mature people and providing recommendations for each. That sort of thing.

        Thank you for replying.

        1. 7

          I know that I have vaguely been interested in and occasionally have learned about type theory, and recently bought a copy of TAPL and got about two pages in before I set it down and haven’t picked it up since. That was a while back, so I don’t even quite remember what my issue is, I think it was too much math.

          This doesn’t mean the book is in any way bad, I’m probably just not ready for it, or maybe need to be in the right mindset.

          1. 5

            I think it would be hugely valuable to have a reading group or something where when someone is confused by a bit of the book it could be added to a wiki and folks with a deeper grounding in TT could answer. Build up annotations as we go?

            1. 3

              I’d love to participate in such a group!

              1. 3

                I’d be interested in this as well :)

                1. 1

                  So what’s the best tool for a scholarly online study group? I’ve seen Mendelay, but the group stuff is pretty weak.

                  1. 1

                    I’m not sure.. I’ll ask around and get back to you :)

                    1. 2

                      Thanks! “Worst” case is using lobste.rs itself, I guess, but it would be nice to have something designed for the job. Like a cross between Rap Genius, a wiki, and Coursera. Free startup idea, if anybody wants it!

              2. 4

                have learned about type theory, and recently bought a copy of TAPL and got about two pages in before I set it down and haven’t picked it up since

                I think that’s the typical TAPL experience but nobody wants to admit it. This is why I get frustrated with context-free book recommendations.

                Haskell’s been the easiest, “I don’t know any math, teach me TT”, I’ve found so far. This leaks into the book a little bit, in fact, one of the chapters we’re releasing this weekend in the Haskell book are called Algebraic Datatypes and teaches the basics of how to reason about datatypes.

                TAPL and PFPL don’t work for this purpose. Wayyy too much math. I’ve gotten bad answers for how to bootstrap to TAPL like, “How to write proofs”. Basic proof-writing really isn’t the issue.

                I’d love to know what the real bootstrap to being able to read TT books and papers is. I’ve been too busy to track this down properly but I’ve been trying to find something.

                1. [Comment removed by author]

                  1. 3

                    I have no idea how well it works as a stepping stone to other things but I strongly second the of recommendation of Conceptual Mathematics. It’s just about the most accessible mathematics book I’ve touched, tied with K A Stroud’s “Engineering Mathematics”.

                    1. 2

                      Conceptual Mathematics is good for CT, but I’m not sure it really captures what I’m looking for as an intro to type theory.

                      Anything can help, but I’m really trying to be more precise and focused than that.

                    2. 3

                      I’ll try to keep you posted, this is one of my personal goals over the next year or so, especially as I have to teach Rust’s type system to more and more people…

                      1. 2

                        I’d be very interested in this as well. I’d love to add suggestions for learning necessary math to this repository.

                        1. 1

                          I’d make a good guinea pig for this — highly interested in the math, not enough math background. If you want one, let me know.

                    3. 3

                      Yeah, you kinda just have to nod at the math and keep going. Once it hits lambda calculus it feels like it lets up a little on the math. I haven’t gotten past this part yet, but I need to revisit it.