This is Hacker Public Radio Episode 3,796 from Monday, the 20th of February, 2023.
Today's show is entitled, Depended Types.
It is the first show by new host David Thrin Christianson 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 Thrin Christianson.
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.
Depended 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 the 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 your refactoring.
Type systems typically these days have a feature that some people call generic, some people
call a play, more fictips, 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 element
to the list as an argument to the program, it then puts that into the list type.
So you can say, you know, this is a program that'll sort, you know, a list that could
take 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 of two a's and it's going to give, you
know, like, a, it's actually a list that are equal to operator on a and then look me
back in other list of a's dependent 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 sort of it, but it can at least
prevent certain kinds of 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 funny.
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 have a popular language with dependent types of interests, if you
sit down and you write down that type signature and you say, hey, address, write my program,
it'll just do it and you don't have to do anything else unless you have some special
need that isn't 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
and 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 languages already.
So most programming languages have a pair type.
So you might say, you know, the pair of the type pair of ANDB classifies a pair, like
actual tuple, which has an A and a B in it.
Well, a proof of AND in order to prove A and 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 A B has two constructors, one of them takes an A and gives you an either A B,
the other one takes a B and gives you an either A B.
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.
Application is a function. So I could say, you know, an 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 and plus k equals k plus n. Or for all n and k and plus k equals k plus n. Well, that's
just an a function type. You, 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, not only is Idris have dependent
types, it also has 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
e-max mode and it's got a, what do you say? It's more of a testbed for really new things in
dependent types. And there's a free online textbook called Programming Language Foundations and Agda
that you can read. For Idris, I'd recommend Edwin Brady's really good book, a type
different development in Idris. You can also check out Lean, Lean 4, which is not quite
released yet. It's still a prior lease, 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 can 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 sea
compiler, so it is definitely useable as a programming language. You might want to read my book
that I wrote with the environment the little type or check out an in-progress free book on
programming in Lean, called Functional Programming in Lean, if you want to learn Lean 4.
I hope this was interesting and I hope it inspired you to go explore a fun new corner of
programming languages. All the best.
You have been listening to Hecker Public Radio at Hecker Public Radio.org.
Today's show was contributed by a H-burner this night like yourself. If you ever thought
of a coin podcast, click on our contributally to find out how easy it means.
Hosting4HVR has been kindly provided by an onsthost.com, the internet archive and our synced.net.
On this otherwise stages, today's show is released on our creative comments,
attribution 4.0 international license.