I am interested in learning “constructive type theory”, and I’d like to combine it with learning Haskell, or OCaml.
I am a beginner.
Do you have strong recommendations?
2 Likes
This kind of book does not exist yet for Haskell unfortunately, but there is a book that uses OCaml.
Program = Proof by Samuel Mimram is what you’re looking for. It starts off by introducing OCaml and functional programming and then goes into logic and lambda calculi. About halfway through it switches to Agda and uses it to talk about Martin-Lof type theory, i.e. constructive type theory, and even goes into HoTT at the end. It’s essentially the notes for a class, and the PDF of it is freely available but you can also buy a hard copy if you want one. Transposing the OCaml specifics into Haskell has been on my to do list forever, hopefully one day.
5 Likes
Warning: shameless self-promotion.
You might be interested in The Little Typer, a book I wrote with Dan Friedman. It’s a fairly non-traditional introduction to thinking in dependent types. The syntax of the language we use (Pie) looks like Scheme, but the resemblance is only skin deep - it’s basically like a simplified version of the core language of something like Agda. The book assumes only that you’ve seen lambda before, and it’s written as a dialog. The “Little” books work well for some people, and not at all for others - do you have experience with one of them in advance?
Simultaneously, you could work through a tutorial I wrote on implementing Pie in Haskell and then attempt to read and modify the Haskell implementation of Pie, which is written to be accessible and easy to read rather than performant.
I don’t really know enough about your background to say whether these are the right resource for you, but they seemed to work pretty well for a couple classes of undergrads at Indiana University and Portland State University.
6 Likes
Nice!
I am familiar with “Little” type books; I have heard of “The Little Schemer”, but never read it. I am most familiar with “The Little Mathematics Library” that Mir Publishing has (little mathematics library | Mir Books). Overall, it elicits a cozy feel in me, which I love.
Thank you; well placed self-promotion 
1 Like
There is in fact a book that goes into category theory in great detail using Haskell. This person authored a blog, book and produced a series of lectures hosted on youtube. The link to the blog: Category Theory for Programmers: The Preface | Bartosz Milewski's Programming Cafe
PS - I’m a fan of The Little Typer and anything that explores type-level programming!
3 Likes