Hosted by
David Thrane Christiansen
on 2023-02-20 00:00:00
I discuss dependent types, which are types that can contain non-type
programs. An example of a dependent type is a list whose type contains
its length. Instead of just writing List<String>
for
a list that contains strings, dependent types include types like
List<String, 5>
that describe lists of exactly five
strings. Dependent types can also be used to represent mathematics, in
which case the programs that they describe count as proofs, and tools
from programming can be used to write math.
Dependent types used to be something that really required a research
background, but there has been a lot of progress on making them more
user-friendly and on writing accessible introductions lately.
Languages mentioned:
- Idris is a self-hosted
dependently typed language with type-level resource tracking
- Agda
is a testbed for new ideas in dependently typed programming
- Lean 4 is a self-hosted
dependently typed language that has a more conservative logical core
than Idris or Agda, and attempts to appeal more to practicing
mathematicians.
- Coq is a proof assistant based
on dependent types that has been used to fully mathematically verify a C
compiler
Books mentioned:
- The Little Typer, by
Daniel P. Friedman and David Thrane Christiansen is an intro to the core
ideas of dependent types, in dialog form
- Type
Driven Development with Idris by Edwin Brady, the creator of Idris,
describes an approach to programming that uses expressive types as a way
to make programmers' lives easier
- Programming Language Foundations
in Agda by Phil Wadler, Wen Kokke, and Jeremy Siek describes the use
of Agda for both programming and proving
- Software
Foundations is a series of books that use Coq as an introduction to
mathematically rigorous software development in a proof assistant. It's
how I initially learned these topics!