Stats for nerds
1recommend
6mentions
5people
2016–2025years
33% recommend67% neutral
Mentions per year
What Hacker News says
- 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
- 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.
- Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history of dependent types is intertwined with the history of formalizing mathematics; dependent types were designed to encode essentially arbitrary mathematical statements.)
The interesting feature of Ada here seems to be what it calls "subtype predicates". As you've explained, these come in a "dynamic" flavor, which are a nice syntax for runtime assertions, and a static flavor, which are compile-time checked but restricted to certain static expressions (per https://ada-lang.io/docs/arm/AA-3/AA-3.2#p15_3_3.2.4).
An example of something you can do in a dependently typed language is write a sorting function in such a way that the type checker proves that the output will always be in sorted order. I am pretty sure this cannot be done in Ada; checking at runtime does not count!
I do believe (having heard from multiple sources) that Ada's type system was ahead of its time and its success in creating practical programs that are likely to be correct is probably underrated. But I'm not here just to legislate semantics; one should be aware that there is something vastly more powerful out there called "dependent types" (even if that power is not likely to come into most people's day-to-day).
(Unfortunately Wikipedia is quite poor on this topic; you will see, for example, that on the Talk page someone asked "Is Ada really dependently typed?" two years ago; no reply. And it makes no sense to say that Ada has "tactics" but not "proof terms"; tactics are a way of generating proof terms. There are many better resources out there (especially ones associated with the languages Agda, Coq (currently being renamed Rocq), and Lean, e.g. https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...). But be warned, there is no "short version": dependent types cannot be explained in a sentence, and they are not something you will arrive at with enough "hacking away".)
- Maybe Not is an excellent video in some ways, but I just watched it a few years later and it reminded me that as much as I love almost every Rich video, I do wish he'd spend some time reading a little deeper on type systems and theory.
For example his note about "Categorical descriptions" and then the explanation about maps/and spec at 25:00[1] seems to indicate he's unfamiliar with the difference between extensional and intensional type theory.
The core difference between the two is extensional type systems decide equality on the observable behavior of the output. For example if two functions take the same input, and produce the same output extensional type systems/theories say they are the same. The problem with this is type equality is then undecidable.
Extensional type systems also struggle because there are more than one way things might be equal! For example two string might be equal if you ignore case, but unequal if you don't. So if we want our type system to check if two functions are equal under case insensitivity an extensional type system will struggle with this.[2][3]
Now in fairness to Rich, these concepts come more from the math community, especially the notion of types being equal under different paths, and in the case of Homotopy type theory are burred in unapproachable language and concepts... even by mathematicians standards.
He also talks about select from spec, and it not preventing you from passing types broader types, and the necessity of specifying deeper type.[4] But, that's just an eliminator defined on the type[5].
Now most strongly typed programming languages suffer from the issue he identifies when talking about not making brittle systems [6] and the issues you get with coupling around taking a map/struct/product type C = A X B (e.g a map C = {A: something, B: something}), and you require A so you're function should be good but you fail to compile because the function says A, and now you're passing C.
It's frankly pretty annoying in places like Java that if you have a Point = Int x Int y you can't use it in functions which take a Tuple = Int x Int y. I'd actually say that's the common observation that both Rich, the Go Inventors, and the TypeScript folks have all made. You need to care about the extensional type of your input (and output) fairly often. And carring around the intensional type causes both dependency issues and just some general PITA's.
[1] https://www.youtube.com/watch?v=YR5WdGrpoug&t=1504s [2] https://math.stackexchange.com/questions/4486995/what-is-an-... [3] https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Ext... [4] https://youtu.be/YR5WdGrpoug?t=2668 [5] https://www.quora.com/In-type-theory-what-is-an-eliminator-a... [6] https://youtu.be/YR5WdGrpoug?t=2823
- I am a high-schooler and I understand dependent types. (I am not the person you are replying to, but I am the person who first mentioned typed holes.)
In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`.
According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem.
With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms.
Here are some types in Martin-Lof type theory:
The unit type is a type with one inhabitant, (). It can be interpreted as the type of the empty tuple. In the Curry-Howard correspondence, the unit type corresponds with truth.--------- () : Unit
A * B, the product type of A and B, is the type of pairs. It is based on the Cartesian product operation: https://en.wikipedia.org/wiki/Cartesian_product In the Curry-Howard correspondence, the product type corresponds with logical conjunction (and). By proving A and proving B, you can prove A * B (AKA A /\ B).x : A y : B -------------- (x, y) : A * B
The empty type is the type with no inhabitants. If you have an inhabitant of the empty type, you can eliminate it to derive anything. The empty type corresponds with falsity, and its elimination means that false implies anything.x : Empty ---------------- elim-empty x : a
The sum type is the tagged union, meaning "this or that." The type A + B means that the Inl tag holds an A and the Inr tag holds a B. The sum type corresponds with logical disjunction (or).x : A -------------- Inl x : A + B x : B -------------- Inr x : A + B
The exponential type, the type of functions, means logical implication. If you have f, a proof that A implies B, and x, a proof of A, you can prove B by doing f(x).f : A -> B x : A ------------------- f(x) : BWith dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively.
With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A).
With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x.
Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't:
Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), and if B(x) is some constant C, Σ for x = 1 to n, C = n * C. The same rule applies to types, as multiplication (product) is just repeated addition (dependent sum of a constant).
Π is like Σ, but for repeated multiplication instead of repeated addition. After all, exponentiation is just repeated multiplication.
Another type that you should be aware of is the equality type, `x = y`. In vanilla Martin-Lof type theory, `x = y` is inhabited by `Refl` if `x` and `y` have the same normal form (reduce to the same simplest form). However, there is ongoing research in a field called Homotopy Type Theory, which redefines the equality type in various ways.
Finally, types themselves form a hierarchy. With dependent types, the types themselves are first-class values, and they have their own types. However, `Type : Type` leads to Girard's paradox (similar to Russell's paradox). The solution is for each type to be in a "universe" so that `Type l : Type (l + 1)`, where `l` is the universe level.
Read about Martin-Lof type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory
- > After 1970 with the introduction of Martin-Löf's Intuitionistic Type Theory, an inbreed of abstract math and computer science, a period of intense research on new type languages as Agda and Epigram started. This ended up forming the basic support layer for functional programming paradigms. All these theories are taught at college level and hailed as "the next new thing", with vast resources dedicated to them.
This seems pretty dubious. Dependently typed languages and other projects embracing advanced type theory are still the realm of niche enthusiasts. While some of the more academic colleges might teach them in one or two courses, the vast majority of education a CS college student receives will be taught in traditional imperative languages. If "vast resources" have been devoted to Agda and Epigram, then I'm not sure what kind of language should be used to describe the resources devoted to C, C++, Java, etc. Also as the author mentions, Intuitionistic Type Theory has been around since the 70's, in fact the same year that C was introduced. Certainly it hasn't been taking over the CS world by storm since its inception, as he seems to claim.
Beyond that, the author's argument seems to be a bit incoherent. He critiques the readability of Modern C++, but C++ is notoriously hard to understand, including or especially prior to the development of C++11. It's never going to be an easy language to read except to seasoned developers. If anything, modern C++11 seems to provide abstractions that increase readability and safety. He critiques the performance of modern C++, but then he ends up recommending that people ditch C++ entirely and learn VHDL/verilog instead. Not even vanilla C++ is fast enough for him, then why criticize modern C++ on the grounds of performance?
Related
Type theory and functional programming
2 recommend · 6
Type Theory and Formal Proof
11 recommend · 15
2018–2025
Gentle Introduction to Dependent Types with Idris
1 recommend · 2
The Little Typer
16 recommend · 37
Type-driven Development with Idris
30 recommend · 47
The Little Schemer
288 recommend · 652
