Type Theory for the Working Rustacean -
This is a modal window.
Das Video konnte nicht geladen werden, da entweder ein Server- oder Netzwerkfehler auftrat oder das Format nicht unterstützt wird.
Formale Metadaten
| Titel |
| |
| Serientitel | ||
| Anzahl der Teile | 15 | |
| Autor | ||
| Lizenz | CC-Namensnennung 3.0 Unported: Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen. | |
| Identifikatoren | 10.5446/52178 (DOI) | |
| Herausgeber | ||
| Erscheinungsjahr | ||
| Sprache |
Inhaltliche Metadaten
| Fachgebiet | ||
| Genre | ||
| Abstract |
|
2
15
00:00
TypentheorieParadoxonSelbstbezüglichkeitKreisflächeSystemprogrammierungMathematikerWort <Informatik>TermSchlussregelRegulator <Mathematik>Physikalische TheorieQuick-SortMultiplikationsoperatorBitRussell, BertrandRechter WinkelOrientierung <Mathematik>ZahlensystemMinkowski-MetrikMathematikTypentheorieDifferenteSoftwareentwicklungKomplex <Algebra>DivisionDämpfungPunktKonstruktor <Informatik>Mathematisches ObjektFormale SemantikReelle ZahlOrdnung <Mathematik>ProgrammierungProgrammiergerätMengenlehreGrundraumPi <Zahl>Programmiersprache
04:04
TypentheoriePunktSelbstbezüglichkeitHierarchische Struktur
04:24
ZeichenketteCodeProgrammProgrammierspracheNatürliche ZahlFormale SemantikZahlenbereichKonstruktor <Informatik>Meta-TagSelbstbezüglichkeitPhysikalische TheorieHierarchische StrukturTermGeradeOrtsoperatorGebäude <Mathematik>UnendlichkeitQuadratzahlQuick-SortMereologieAutomatische IndexierungVektorraumKontrollstrukturFunktionale ProgrammierungSchaltnetzFormale GrammatikSchlussregelRechter WinkelFormale SpracheBeweistheorieObjektorientierte ProgrammierungMAPReelle ZahlParametersystemZweiSoftwareentwicklungZeichenketteSystemprogrammierungComputerspielMusterspracheProgrammierungÜbertragDeklarative ProgrammierungBitEin-AusgabeFehlermeldungZusammenhängender GraphGruppenoperationDatentypComputeranimation
11:52
ThreadRechter WinkelDickeQuellcodeDebuggingVektorraumHalbleiterspeicherZahlenbereichProgram SlicingProgrammfehlerOrtsoperatorProgrammbibliothekElement <Gruppentheorie>ResultanteMultiplikationsoperatorSoftwareentwicklungQuick-SortFunktionale ProgrammierungKonstruktor <Informatik>Funktion <Mathematik>MereologieRechenwerkArithmetischer AusdruckParametersystemCodeAutomatische IndexierungAutorisierungBeweistheorieQuellcodeGleitendes MittelSystemprogrammierungMathematikImplementierungCompilerFormale SemantikAggregatzustandNatürliche ZahlMusterspracheProzess <Informatik>Güte der AnpassungStandardabweichungDifferenteSoundverarbeitungSpeicherabzugZustandsmaschineCASE <Informatik>KanalkapazitätTouchscreenRechter WinkelMaximum-Entropie-MethodeAssoziativgesetzGewicht <Ausgleichsrechnung>PaarvergleichComputeranimation
19:19
Vorlesung/Konferenz
Transkript: Englisch(automatisch erzeugt)
00:05
Hi, I'm Dan from Portland. I'm going to talk with you all today, or I guess I should say I have the privilege to talk with you all today about one of my favorite subjects to just kind of ramble on about endlessly, and that is type theory. So we're going to look a little bit at the history of or sort of the origin story
00:23
of type theory, and then we'll spend some time looking at how this history led to a want for the ability to kind of enumerate some rules of what it means to use a type theory or a type system. And then finally, we will use a Rust type system to give some concrete examples
00:41
of some of these rules, and we can look at some ways that we can kind of abuse Rust type system to start to bend some of these rules. So there we go. OK, click. Not a space bar. What am I talking about when I talk about type theory?
01:01
Well, type theory in general just kind of orients itself around this notation. We have an A on the left and a big A on the right, separated by the colon. The little a on the left is called a term. The big A on the right is called a type. And it's really just a formal system that we can use to reason about mathematical objects or really almost any subject.
01:21
It is, of course, a familiar notation to us programmers. We write things down like this in our Rust programs every day, albeit in a slightly different outfit here. We've got some x that is of some type u8. It's a byte. But while we're using this every day, what we probably don't think about is why. Like, where did types come from? How did we get to be using types in our programs and in our programming languages?
01:44
To answer that question, I'll have to take a little historical digression. Now, type theory was created by the British mathematician and philosopher and just kind of all around badass Bertrand Russell. And Russell was on a mission. He wanted to give a foundational theory for all of mathematics.
02:03
And he wanted to do that constructively. And so what I mean when I say constructively can kind of be illustrated with a Carl Sagan quote that says, if I want to be able to bake a pie from scratch, then I will first have to invent the universe. Well, Russell wanted to bake mathematics and he wanted to do it from scratch. He wanted to start with absolutely nothing and
02:22
then build these mathematical objects up on top of one another, up until the point where he could start to reason about complex things like the real numbers or long division. And while he was on this quest, he found that for a theory to be foundational for all of mathematics, that that theory will also have to be foundational for itself.
02:42
And what I mean by that means that to use a theory, when we use a theory to talk about things formally, what we're doing is talking about the rules and kind of the regulations that guide that object that we're giving formal semantics to. And that's what we're using type theory for when we do this in programs. But at this point in time in history, the sort of lingua franca for
03:02
mathematics was set theory. And in order to talk about set theory in set theory, he's going to have to use sets to talk about sets. It becomes this kind of self-referential circle. It's kind of like the barber's paradox, which I'm going to say very slowly so I don't screw it up, is this idea of the barber who shaves all that do not
03:22
shave themselves. So if this barber does shave themselves, then that implies that they did not. However, if they don't shave themselves, that implies that they should. And this is paradoxical. It's the same idea to try and talk about sets using set theory. You can't self reference that way, it's a paradox. And we call that paradox Russell's paradox.
03:42
And so as an answer to Russell's paradox, he came up with this notion of types where he could separate the theory that kind of gives the rules and regulations from the mathematical objects that we're trying to specify. The technical word for this is actually called stratification. The types are stratified from the terms. But unfortunately for Russell, just a few decades later,
04:04
the French mathematician Gerard found that type theory was actually susceptible to the same self-referential problem. And that's because at some point, if we want to start talking about doing type theory in type theory, we're going to have to be able to talk about the type of all types. And if we stop there at types, we can't self reference in that way.
04:23
So in the literature, we started building up a hierarchy where we can talk about the type of all types as being the star is what is usually used to represent the type of all types in the literature. We say that the type of all types is this star. But if we stop here, we end up in the same position, where we are self referencing at the type of all types.
04:45
So we just keep building. In the literature, what comes after star is square. Square represents the type of all types, of all types. And we just keep going, because we continue to just be self referenced. And we can't, so we start building these squares where we index the squares.
05:02
And we're kind of just going on from i to j to k and l. And we end up with this sort of infinite hierarchy, this kind of stairway to heaven of formal theories, where one is specifying the theory below it. And all of this is just to try and keep from being able to self reference. So we can talk about the theory that lives outside
05:21
the objects that we're trying to formalize. So another way to think about this is that these things on the right hand side of each colon kind of represent a meta theory. It's the theory about the theory for the thing below it. And I know this is kind of starting to get abstract and tenuous. So I'm gonna ground it by looking at rust type system. And we'll look at some of the rules that use these things to govern what's allowed
05:44
and what we can do in rust type system. So here is a very simple rust function. It takes a byte and it returns a string. It's two concrete types. But of course, if we needed to write a rule that could prescribe us to be able
06:01
to use this kind of function, it would need to talk about all of the possible combinations that we can use to write a function like this. So it actually has to step up one level in the meta theory, so to speak. And that rule ends up looking like this. We have this star to star. That is the idea of being able to write a function that goes from any type to any type.
06:20
But in Rust, we can also write functions like this one. Now, this is not a useful function in real life, but it does give us a good example of this idea of being able to enumerate the type of all types inside the language, inside the theory of Rust itself. And that's what T represents here. It's a polymorphic type that can be any type that could ever exist in any Rust program. And it returns a string.
06:42
So to be able to write a function like this, we have to step up once again in that hierarchy. So the rule that governs a function like this, it looks like this. We have the square to star, cuz we've stepped up one in the meta theory. So this is an example of a type that we can't actually write in Rust.
07:01
You see, it looks fairly familiar at first. We have the type parameter t, and then we have this peculiar second parameter, where we've got this n colon u8. And then when we actually declare a value of this type, we're putting a one inside the type. Now, this is a thing that we can't actually do in Rust. This is not legal in Rust type system. The rule that would allow us to do something like this,
07:22
actually is this star to square. Going from something that lives in the meta theory at the type of all types, and actually gives us something that is polymorphic. So if we look back, what are the things that we can do inside Rust type system? So we can go from star to star. We can go from square to star, but the thing that we can't do is this idea of going from star to square.
07:45
So you may have deduced or noticed while looking at this, that there is kind of a subtle pattern here. We can either move down in the hierarchy in the meta theory, or we can stay where we're at in star. What we can't do is move up in the hierarchy.
08:01
The rule that allows us to get this moving up in the hierarchy actually gives us something that is called the dependent types. Put simply, a dependent type is just a type that depends on a value. It's kind of like that vector that we saw before where we put the number one in the type. Well, that's what a dependent type is. But if we think about this a little bit more abstractly,
08:21
this idea of being able to climb the ladder, to climb the hierarchy while we're inside the language, that's what allows us to start giving formal semantics to the objects that we're defining in the level below. And then when we need to give formal semantics to those formal semantics, we can step up the hierarchy and kind of do this infinitely. And maybe actually achieve those goals that Russell was kind of shooting for.
08:42
But if we ground this in actual executable runnable programs, kind of like for the reason that we're all here today. Well, what that means is that we end up in a situation where we can actually write our proofs in our programs. This is a quote from a paper called Why Dependent Types Matter.
09:00
And these researchers have this very succinct way of putting, saying that if we have dependent types in a programming language, then those programs are by their nature proof carrying. And proof carrying is a term that's used in the programming languages research that means if you have two components in a program, and
09:21
before they interact, they first trade proofs of one another. And then they check those proofs before they take any action on the inputs that they've been given. And if the proofs don't check, then they just throw it away, or they return an error, or it crashes the program altogether. And this is very interesting. So what I'd like to do next is to look at a few examples of a language that
09:43
actually does have dependent types. And we'll see an example of being able to carry a proof through a program. And then we can go back to Rust and kind of look at ways that we can bend the rules to let Rust allow us to do something like this in Rust. So we have a definition here, this definition called NAT.
10:01
NAT is short for the natural numbers, is what NAT stands for here. The other part of this top line that I want to point out here is that we have this colon type. So when we have the ability to climb the hierarchy inside of the language itself, the thing that we're using to give formal semantics, we also kind of have to help the compiler and tell it where in the hierarchy we're entering.
10:23
So when we do this here, we're telling it that NAT lives in the hierarchy just below type, which is that star that we saw before when we were looking at this in terms of the meta theory. We then have two constructors. We have the zero constructor here, and it actually represents the number zero. The natural numbers are just all of the positive integers plus the number
10:41
zero. And we can actually use this constructor in combination with this constructor, the successor constructor, to construct from basically nothing the natural numbers. So we're starting at zero, and then we can just repeatedly apply this suck function over and over again to produce or to induce the natural numbers. So for example, the number one would be suck zero, the number two, suck suck
11:04
zero, and so on. Now that we have this definition of the natural numbers, we can then embed that definition into a data type that actually carries a proof using it. So here we have a vector, and we'll kind of break it down part by part.
11:21
So again, we have the data declaration for this. And then we show that it has a parameter and that that parameter lives in the hierarchy at the level of just below type. And then on the right-hand side, we have what looks like a function. And what's happening here is that we are taking something that lives in the hierarchy at nat, and then we return a type.
11:41
So this is an actual example of that star to square rule that we were looking at before. It also has two constructors. It has the empty constructor, which gives us a vec where it has the natural number zero. And then it has a second constructor, this cons constructor. And this is what's used to add an element into the vector. So we can break this down as well.
12:01
It starts with a vec where the natural number is at n. And then it takes a new x. And what it produces is a vector with the successor function applied to n, increasing the size by one. So what's happening here is we are carrying a proof of the size of this vector as the program advances.
12:22
Any use of this carries the proof forward. So if we go back to the Rust type that we were looking at before, we could actually make a sort of minor modification to this, to actually make it a legal Rust expression. What if we could do something like this? So now we have an n type parameter.
12:42
And it has a trait bound with this nat here. So what's happening here? Well, what we're actually doing is giving a definition of the natural numbers inside Rust type system. So we have to give types to show the two constructors that we saw before. We had zero, which is just a unit struct.
13:01
It's got nothing in it. And then we have the successor constructor, which appears to take a parameter. And it takes that nat type. And then we glue them together to make them act as though they are a single type with this nat trait. And now we just implement it for both. And now we can start to use something like the natural numbers inside Rust type system.
13:22
So what's an example of using something like this? Well, let's actually put our own or roll our own little size proof vec that carries a proof of its size inside Rust type system. You can see that it actually just wraps around an ordinary Rust vec. But to use it is actually gated by this proof here.
13:41
So anything that we actually do to use that vec inside will have to abide what this size says if it's making changes to those sizes. So to implement the idea of actually adding things, we have a push function here. If you look closely, you see it's implemented over a vector of any size, anything that has an index in it for
14:01
n. But what it's doing upon return is giving us that n wrapped with the suck. It's increasing the size by one. So all together, our push function here ends up giving us that same sort of semantic of carrying a proof of the size of the vector as we use it through the program.
14:23
Now, to give a really good concrete example of why we would ever want to do something like this, I have to tell a little story. And that story's antagonist is this function. It's in the standard library in Rust, or in core, which is how I was using it.
14:41
And its job is to just copy some data from one slice into another. So mute self here is the destination slice, and you call it on that, and you pass it some source data. And it just goes to the data and copies it one by one. But what happens when you use this function when the two slices are not exactly the same size?
15:00
It crashes the program. It expects the two slices to have the same size. It has an assert in there to verify that they're same size. Now, for me personally, when I ran into this, I was actually cross-compiling for ARM, and then running it in QEMU, and then plugging a debugger into QEMU to try and figure out how in the world this had happened, and I was
15:20
in a situation where the two vectors were not the same size. And to make matters worse, what I ultimately found that how this was happening was actually in a library that I was using. It wasn't in my code. It was just an assumption that either the writer had about that function, or just something that has not been hit yet. But that library had been shipped, and I was using it. And I ended up in this situation.
15:41
And I lost a day or a day and a half chasing this thing while I should have been writing this talk. So what can we do to better this situation so you don't end up in such a conundrum where you lose a day and a half when you should be doing something else? Well, what if we could write a copy from over our
16:03
proven vector? What would that look like? Well, the body of the function, it effectively looks the same as copy from slice. Now, copy from slice actually uses memcpy underneath. But in effect, this is what it's doing. It's just copying data from one position in memory to another position in memory. But what copy from slice doesn't have is this.
16:24
Here we have an extra m coming in. And if you look over there on the other side of the screen, that m is what represents the size of the size proof vec. And then we have this extra trait bound is less or equal to, and we say that m must be bound by that. And it's over n. And then we ask that an associated type called result is
16:42
equal to true. So we were talking about dependent types earlier. And one of the things that you get when you use dependent types is a proof-carrying code. And how you get that proof-carrying code is because part of the program has to actually be evaluated by the type checker for it to be able to verify that what you're doing is sound.
17:01
And to mimic that kind of thing, we're actually going to write part of the program inside a Rust type system. So is less or equal to is actually a comparator function. It takes two things of type nat and returns, or sticks in the associated type this result.
17:20
So how it works is it just recursively peels off those suck constructors. And if it occurs that there is a zero on the left first, then the output it sets to true inside result. But if it finds a zero on the right, it sets the result to false. So what happens if I was to try and use this function
17:43
with a vector that was actually larger than its destination, the source vector was larger than the destination? Well, the compiler is going to bark at me. I'm not going to be able to actually produce a program that I can run and deploy and then have to debug for an hour or days or whatever. It's going to tell me I expected to see true here, but
18:02
I didn't. These are inverted because it's comparing it to what the result equals true there was, as opposed to what that implementation was for that M. But in effect, what's happening here is that I am no longer capable of actually deploying this program. So if the library author had this, then they would have
18:21
not been able to build that library and then ship it to cargo. And I wouldn't have been in the situation where I was stuck trying to find that bug. And I would have had all that time back. And I think that's pretty cool. So this pattern that we're showing here, this idea of implementing part of the program inside Rust type
18:41
system, can actually be applied to lots of different patterns kind of similar to this one. We can use state machines, and then you bound the output state with some trait. You can actually track capacity as well. It's kind of flipping this problem on its ear where you start with some number and kind of decrement it. And if you hit zero, you fail to compile.
19:01
And all of this is in an effort to find bugs before we ship code. So we don't find ourselves chasing bugs forever, and then maybe we, I don't know, have more time on our hands to do fun things. And I think that's pretty cool. And that's it. That's all I've got for today. Thank you very much.