Ask HN: Book to get started in Type Theory? | Hacker News Reader

Ask HN: Book to get started in Type Theory?

3 pointsf1shy4 comments

I saw this post today: http://strictlypositive.org/diff.pdf And I would like to understand it. Where should I start?

Thanks!

No need for "Type Theory", you are interested in "algebraic types".

A sum type is a type whose values consist of one of a menu of choices.

    Primo ::= Spaghetti + Gnocchi

A product type is a type whose values consist of "one from each column"

    Menu ::= Antipasto * Primo * Beverage

Sums and products interact the way you'd expect them to from elementary school, so:

    Antipasto ::= Proscuitto * (Melon + Fig)

tells us that an antipasto may (depending upon market conditions) either be Proscuitto with Melon, or Prosciuitto with Fig, which can be written equivalently as:

    Antipasto ::= (Prosciuitto * Melon) + (Proscuitto * Fig)

Now, we also have natural numbers at the type level, so 0 ("unobtanium") is the unit for sum and 1 ("a trifle") is the unit for product.

    Liberty + Death + 0 ~= Liberty + Death    (because 0 never happens)

    Death * Taxes * 1 ~= Death * Taxes        (because maybe hiccups (~= 1) are also unavoidable, but we *don't care* about hiccups)

And it turns out that sums of trivial things ("cases") allow us to make distinctions, so:

    True + False ~= 1 + 1 ~= 2

(optional exercise: exponentiation produces a function space, so for instance 2**Foo is equivalent to the type of predicates on Foo: Foo->2. confirm for yourself that all the usual math, with sum, product, 0, 1, etc., also goes through with exponentials)

Note that a product of similar things can be written as an exponential, eg:

    Shoe * Shoe ~= Shoe ** 2      (a 'left' shoe and a 'right' shoe ~= a pair of shoes)

Now read §1.1 of "The Derivative of..." and Huet97 ("The Zipper")

Once you've understood the specific case of the zipper, you should be able to make headway on the general cases that McBride is using some heavy notation to convey in the rest of "The Derivative of..."

(optional exercise: note that the choice between Melon and Fig is demonic —the restaurant makes it based on market price— and the choice between Spaghetti and Gnocchi is angelic —we make it based on preference—; learn about linear logic's additional connectives and explain why

    Menu ::= (P*(M+F)) * (S&G) * B

is a more precise notation for our menu.)

Thanks so much

Software foundations is a practical introduction to Coq's type theory (calculus of inductive constructions). You get a really strong feel for the concept of proofs as types. One of the sections builds the theory of typed lamda calculus within Coq. It's otherwise lighter on theory than other resources.

https://softwarefoundations.cis.upenn.edu/

Types and Prigramming Languages by Pierce

Reply on news.ycombinator.com