7c8efd2228
- MCP server with stdio transport for local use - Search episodes, transcripts, hosts, and series - 4,511 episodes with metadata and transcripts - Data loader with in-memory JSON storage 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
149 lines
9.0 KiB
Plaintext
149 lines
9.0 KiB
Plaintext
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.
|