1. 12
  1. 6

    This book was recommended at r/haskell as a first book for type theory:

    For type theory I highly recommend Type Theory and Formal Proof: An Introduction. The title sounds scary, but I actually find it to be an excellent first book to get into the wonders of type theory.

    1. 7

      As an alternate recommendation, Type Theory and Functional Porgramming is also good. It is a bit old (and thus a bit unfashionable), but unlike many other texts, it is written from a programmer’s rather than a mathematician’s perspective.

    2. 4

      The video covers an introduction to the landscape of mathematics, category theory, set theory and discrete math, type systems, abstract data types and data structures, and semiotics, but does not actually introduce type theory. I think that type systems are here being substituted for type theories.

      I think that it would have been nice to flesh out the correspondence between some portion of type systems and category theory or logic. For example, the mantra that “well-typed programs never go wrong” corresponds to the totality of arrows in FinSet, the category whose arrows are functions between finite sets.

      I appreciate the mention of object-free category theory, although I wish that it would have been made more precise. Once we reduce objects down to mere labels which ensure that arrows are well-typed when they are composed, then identity arrows can fully represent their source/destination labels, and we can simplify the axioms accordingly.

      I wish that more attention would have been given to ideas like row polymorphism (“duck typing” in the video) for statically-typed languages, although a lot of the same ground is covered in the discussion on typeclasses. The presentation makes it seem as though languages like OCaml, where objects can have rows of methods and be somewhat incompletely typed, are not statically typed.

      The ontological argument at the end of the video is interesting, and while it has some edges of definite truth to it, I’m hesitant to embrace the central claim that computers simply do what we tell them to do. I dislike the anthropic bias and the idea that humans aren’t meatbag computers, and as a result, I’m not keen on modelling humans as having some special agentive nature which computers lack. Indeed, in object-capability theory, we say that every object is its own agent, capable of planning and pursuing its own goals, and we do this so that we are not surprised when a normally-useless object ends up being powerful due to its position in a plan. Humans are merely special objects which reside outside the heap, just like objects on other computers far away.

      1. 2

        Thank you for this. Your review is both in-depth and useful.

        I literally threw this together in a couple of hours the other morning. I was interested to see if I could scan and summarize the field in a quick and accessible manner.

        When we summarize, we by necessity abbreviate, skim. I was focusing on getting to the common terms we use in CS and how we get to them. I would have loved to have spent more time at the beginning. If I continue to develop this, I’ll give that some serious thought.

        I was especially fascinated by your reaction to my claims at the end regarding semiotics. I spent over 50 pages in my book reaching this conclusion from an entirely-different angle. I find with my nerd buddies that if I make this point too quickly, I get the same response as you gave me. I am not making a human-centric argument in any way, although I can see where it might seem that way. This conclusion would be true of intelligent machines, aliens, perhaps even dolphins and monkeys. It’s a problem/feature of intelligence. It’s not even related to biology.

        If I take the time to explain and prove it, people zone out. (At least most do). It does not seem to be related to technology and programming. However if I go at it too quickly, they misunderstand — and it seems they misunderstand in the same way. Let me know if you’d like to see the more in-depth version. I’d be fascinated to see if there are holes there as well.

        I always love a good critique.