3 ms·

What is a good way to get started with this literature? And is it better to read theory first, or read theory in conjunction with using languages like Haskell

What is a good way to get started with this literature? And is it better to read theory first, or read theory in conjunction with using languages like Haskell and Coq? I studied a lot of mathematics, and I find this fascinating, but I've found it hard to read the literature on type theory, and mathematical logic also.

ek 13y ago
It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want. You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference. The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read. It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.
- tel 13y ago
  I have only managed to get through the first chapter myself and I really want to reiterate that—the first chapter does a fantastic job presenting MLTT.
- yetanotherphd 13y ago
  thanks for the pointers. I gave up with Martin-Löf type theory reading other texts, so I'm looking forward to trying again with this book.
RoboTeddy 13y ago
I asked this question in ##hott on freenode last week, and someone recommended http://www.cs.cmu.edu/~rwh/courses/hott/ http://www.cs.cmu.edu/~rwh/courses/hott/

ek 13y ago

It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want. You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference. The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read. It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.

tel 13y ago
I have only managed to get through the first chapter myself and I really want to reiterate that—the first chapter does a fantastic job presenting MLTT.
yetanotherphd 13y ago
thanks for the pointers. I gave up with Martin-Löf type theory reading other texts, so I'm looking forward to trying again with this book.

RoboTeddy 13y ago

I asked this question in ##hott on freenode last week, and someone recommended http://www.cs.cmu.edu/~rwh/courses/hott/ http://www.cs.cmu.edu/~rwh/courses/hott/