hpr-knowledge-base/hpr_transcripts/hpr3796.txt

Episode: 3796
Title: HPR3796: Dependent Types
Source: https://hub.hackerpublicradio.org/ccdn.php?filename=/eps/hpr3796/hpr3796.mp3
Transcribed: 2025-10-25 05:26:03

---

This is Hacker Public Radio Episode 3,796 from Monday the 20th of February 2023.
Today's show is entitled, Dependent Types.
It is the first show by Newhost David Thryn Christensen, and is about 8 minutes long.
It carries a clean flag.
This summary is, A Quick Taste of Programming with Dependent Types.
Hi, my name is David Thryn Christensen.
I'm the Executive Director of the Haskell Foundation, but I'm not here to talk about Haskell
today.
I'm here to talk about dependent types.
Dependent types are a feature of a type system in a programming language, where the type
is allowed to contain ordinary programs and not just other types.
What does that mean?
Well, let's zoom out a little bit first.
So when you're writing a program in a language with a type system, you can work in a way
where first you write down the type and then you start writing down the program.
As you write the program, the compiler tells you which parts are matching the description
you gave in terms of the type and which parts aren't doing so yet.
And by refining the program toward the type, you're getting the computer to help you in
achieving your stated intentions.
This is a lot of fun, and also it has some nice practical benefits.
First off, you don't need to write quite as many tests, because certain bad situations
in the program just can't happen.
And also, refactoring becomes a lot easier because you make one change, and then the compiler
starts telling you, oh, hey, all these other parts of the program, they're not consistent
with that thing you just did.
So maybe you should go check them out and update them to fix the change they introduced
by refactoring.
Type systems, typically these days, have a feature that some people call generics, some people
call it polymorphic types, call whatever you want.
The basic idea is that a type is able to take another type as an argument.
So instead of being able to say, just this is a list, or this is a dictionary, you could
say, this is a list of strings, or this is a list of integers, or this is a dictionary
where the keys are strings, and the values are network sockets, or something like that,
or file handles.
And this is really nice.
You can also write programs that take a type as an argument.
So you might say, this program that sorts a list is going to take the type of elements
of the list as an argument to the program.
And then puts that into the list type.
So you can say, this is a program that'll sort a list that contains any type, I will
just call it A, and it's going to take a list of A's, and it's going to take a way to
check the ordering of two A's, and it's going to give essentially a less than or equal
to operator on A, and then looking back another list of A's.
Depended types simply remove the restriction that the argument passed to a type must be
another type.
So now we can not only say a list of strings, but we could say a list of five strings.
And the sorting function is not just going to be able to say, I'm going to take a list
of A's and give you back a list of A, instead it's going to say, I'm going to take a list
of N A's and give you back a list of N A's.
In other words, sorting a list keeps the length the same.
You get the same number of things out that you put in.
And this doesn't catch every mistake, you know, you might just take the first thing
in the list and make a bunch of copies of it and say, hey, I sorted it, but it can at
least prevent certain kinds of mistakes where you maybe forget an element during sorting.
This system wouldn't be very useful if you could only put variables in your types.
If you could only say N or five, ideally you want to be able to do things like running
programs in your types.
So the append operator on this can say, I'm going to take a list of N strings and a list
of K strings and then give you back a list of N plus K strings.
And in reality, you could make this work for any types.
You could say a list of N A's and a list of K A's and give you back a list of N plus
K A's.
And this is really fun.
You could tell you didn't forget items from one of your lists.
And when you're writing the program, oftentimes the compiler can even just write it for you.
So, you know, if you, a popular language with the pen type is Idris.
If you sit down and you write down that type signature and you say, Hey, Idris, write
my program, it'll just do it.
And you don't have to do anything else unless you have some special need that is guessing.
So the more specific your type, the more help you can get from your programming language
in writing your program.
Interestingly, this doesn't just allow you to write expressive specifications for programs.
It also allows you to encode arbitrary mathematics.
So one way that this can work is that the logical connectives, so things like AND or
and implies are all represented naturally by things that we have in programming language
it's already.
So most programming languages have a pair type.
So you might say, you know, like the pair of A, the type pair of A and B classifies a pair
like an actual tuple which has an A and a B in it.
Well, a proof of AND, in order to prove A and a B, well, we've got to prove A and we've
got to prove B. So the proof itself is just a pair of a proof of A and a proof of B.
Similarly, a lot of types have a lot of programming languages have a type called either.
So either AB has two constructors.
One of them takes an A and gives you an either AB, the other one takes a B and gives you
an either AB.
You know, if I want to say A or B, like the logical statement, well, there's two ways
to prove that either I can prove A or I can prove B.
So you can see data types as being proofs in this setting.
Implication is a function.
So I could say, you know, A implies B. Well, that's a function that transforms evidence
of A into evidence of B.
And finally, if I want to talk about quantification, which is to say, for all, well, that's also
a function where we name the argument and then get to refer to that name later in the
type.
So we could say, you know, the function for all N, N plus K equals K plus N. Or for all
N and K, N plus K equals K plus N. Well, that's just a function type, you know, you give
it any individual numbers N or K and it gives you back the evidence that, you know, swapping
the order of addition for those two things is, in fact, equal.
That's pretty cool.
And what this does is it means you can start using the tools of programming in order
to do mathematics.
And in particular, a proof by induction becomes a recursive function.
If this sounds like fun and you want to learn more, I'd recommend downloading and playing
around with one of the programming languages that has dependent types for a long, long
time.
Like the research has been going on for decades on this.
And it was really kind of a thing you could only do with academics and you kind of needed
to have a mentor to help you out.
But these days, there's a lot better resources and a lot better implementations.
A lot of progress has been made.
So I'd go download Idris, which is a programming language with dependent types.
It looks a lot like Haskell if you've ever had a chance to play with that.
Idris has, not only does Idris have dependent types, it also has a system for talking about
resources in the types.
So you can say that every file handle that's opened is closed exactly once.
You can also check out Agda, which has a really nice emax mode and it's got a, what do
you say?
It's more of a test bed for really new things in dependent types.
And there's a free online textbook called Programming Language Foundations in Agda that
you can read.
For Idris, I'd recommend Edwin Brady's really good book, Type Different Development in Idris.
You can also check out Lean, Lean 4, which is not quite released yet.
It's still a pre-release, but it's mostly intended to be a proof assistant.
However, it's a good enough programming language that they could implement it in itself.
Idris 2 is also self-hosting, so that's pretty fun.
And you could also check out Cock, which is really a system designed to do mathematics
rather than to write programs, although it has been used to write a C compiler, so it
is definitely usable as a programming language.
You might want to read my book that I wrote with Dan Friedman, The Little Typer, or Check
out an in-progress free book on programming in Lean called Functional Progaming in Lean,
if you want to learn Lean 4.
I hope this was interesting, and I hope it inspired you to explore a fun new corner of
programming languages.
All the best.
You have been listening to Hacker Public Radio at Hacker Public Radio, does work.
Today's show was contributed by a HBR listener like yourself, if you ever thought of recording
a podcast, and click on our contribute link to find out how easy it really is.
Hosting for HBR has been kindly provided by an honesthost.com, the Internet Archive
and our Sync.net.
On the Satellite status, today's show is released on our Creative Commons, Attribution 4.0
International License.