Name: Type theory and functional programming
ISBN: 9780201416671

What Hacker News says

codeismathAug 2025

Books. Some books on my shelf covering these topics:

"Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)

First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers

For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof

"Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo

"Type-Driven Development with Idris" by Edwin Brady

"Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski

"Types and Programming Languages" by Pierce

"Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)

"The Little Typer" by Friedman and Christiansen

"Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)

For Category Theory:

"The Joy of Abstraction" (2023) by Euginia Cheng

"Basic Category Theory for Computer Scientists" by Benjamin C. Pierce

"Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel

"Categories for the Working Philosopher" by Landry

thread

solomatovApr 2014

All these tutorials won't teach you how to use coq or agda. The main problem is that in order to use coq or agda, you need to learn Martin-Lof type theory (or calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic:

* Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/)

* Programming in Martin-Lof type theory (http://www.cse.chalmers.se/research/group/logic/book/)

thread

codeismathMay 2021

I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.

But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.

If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.

thread

sirabenMay 2021

As others have said, I also recommend Types and Programming Languages.

> What's the relationship between programming language theory and type theory?

I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation).

There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.

thread

chriswarboMay 2014

Indeed, the wording of the article even made me think of type theory and functional programming.

> For instance, a kettle with a power supply can serve as a constructor that can perform the task of heating water.

kettle power_supply water : (water * heat)

> You simply say that the task of creating energy from nothing is impossible.

first_law : (Null -> energy) = _|_

> In principle, everything possible in our universe could be written down in a big book consisting of nothing but tasks

This sounds like an enumeration (eg. a Goedel numbering) of programs, or alternatively of a (program, runtime) quarter-plane.

> The collaborators then go on to define the concept of a “superinformation” medium that encodes messages that specify particular physical states—in this case, one in which copying is impossible

Sounds like substructural type systems and linear (or affine) types.

thread

silentvoiceMar 2014

This is a very interesting project and it has actually set me on an interesting path.

In scientific computation one blends mathematics and computation. The math is highly advanced, and it will tell you important things about your resulting code such as what kind of stability properties you should expect, and how "robust" the code is (deliberately ambiguous term, but in most cases it means: does your code work equally well no matter what parameters you throw at it?).

In the realm of physics simulations, these math questions turn out to be amazingly delicate and failing to answer them before running your code on a very large problem very often leads to unexpected (and wrong) results, if the code actually ever successfully finishes executing.

There is therefore a tremendous amount of literature where these questions are answered, all containing a meticulous amount of careful detail as well as deep insights coming from all the relevant branches: linear algebra, physics, functional analysis.

The problem however is that as we gain more understanding and knowledge the math hasn't gotten any easier. Sometimes the arguments are so sophisticated that it really leads me to doubt whether the result can be trusted at all.

This leads into something which I know very little:

A better understanding of foundations really is called for here, and a foundation which lends itself better to computation than what is currently available. Computers need to start being able to verify proofs better. Proof assistants exist today, but their use is currently limited to computer scientists because they rely on deep results in that field relating type theory to mathematics - it represents a tremendous barrier to practicing mathematicians.

I hope in the future that "reproducibility" in my field means not only submitting your code so that other people can reproduce your performance claims, but submitting proof documents to be independently verified on someone else's computer. Whenever I read the small bits about univalent foundations it sounds like they are adding magic sauce to make this possible, and so I follow it closely (but don't understand it all yet).

The interesting path I spoke of earlier: I'm now learning type theory and functional programming just so that I can make sense of this branch of computer science that I originally didn't know existed.

thread