What type of thing is a type? by Ron Garcia

so good afternoon, everybody, as Zeeshan said
I’m Ron and I work on types. So I’m — I’ll tell you a little bit more
about myself in a bit but I just wanted to kind of set up the stage, which is you know,
a lot of programmers here, I write lots of code, like ten lines a year or so now, so
I have lots of insights into how this works. But in my older days when I was actually writing
more code, I came to both have a love and hate relationship with types, which is why
I think I work on types and not types at the same time now. Call it schizophrenia. But you can look at types and typed programming
languages in multiple different ways and I just wanted to kind of highlight these two
kind of views of the idea of having a type discipline and one of them is like, you know,
the discipline strengthens your mind and helps guide you so that you can break things and
like shoot people across the wall. But on the other hand you can think of a discipline
as like that thing that keeps you from doing wrong and makes you sad, so you know, then
you find yourself getting your hiney smacked in modern art. So for instance and a lot of people who are
really into programming and especially typed function programming languages like this idea
that the types will guide your program and thinking in types will help you program well
and so this is just an example of the Idris language and this type-driven development
but I’d also note that the first where I first came to appreciate type driven development
is in the Racket language. It’s like, high wire walking for like people
who don’t feel like using training wheels. So on the other side, you have this idea of
type discipline and how type checkers that you work with kind of sometimes they drive
you crazy, sometimes they help you out a lot. And one case here is just like, yeah, you
know, your type checker tells you that you gave it something that has type string, it
has type string and lists lists oh, I know how to fix this, let’s just put brackets around
it twice and carry on. It reminds me of my old C programming days
where you’re like you ever this three-star programmer and you’re just like, I’ll add
more stars. So the real answer is you’ll swap your arguments. Maybe you want to switch them the other way. So that’s kind of life of a person programming
with types and as a researcher I spend a lot of time kind of thinking more in the abstract
about them so this talk is kind of to give you a flavor of the theoretician’s point of
view on how types work and how that kind of style of thinking can help you think about
even types in programming. And give you some insight into what kind of
type systems researchers do or so — so as Zeeshan said I’m a professor at University
of British Columbia and I’ve spent a lot of time on mixing dynamic and static typing. And in order to do that I’m trying to think
about what’s going on with types. There are so many different views and as theoretician,
you want some grounding and you end up spending a lot of time reading and reading lots of
papers, not necessarily visiting the town of Reading, but whatever. So I put together this list of papers that have definitely influenced me when reading about types. I should note this is not the definitive list of papers on types. There are papers from earlier, there are definitely papers that have been written in the last 13 years that are really significant. This was just a really interesting window
into types. So having spent a lot of time kind of digesting
these papers and reading them, I guess I am that kind of person who sits around with a
beer and a paper and is like — [laughter] Yeah, you know, like papers, it’s the weekend,
what am I gonna do? Read another paper!
[laughter] So it’s kind of addictive. But today I’m going to talk about one of the
mostly I’m going to focus on one of the — what I think is one of the great papers on types
and programming languages that just happened to come out in the 1970s, and there’s a number
of other papers here that I think are also really significant but you can only cover
so much in a period of time an I decided that I’d focus on mostly one and then talk about
how it relates to some of the work in the others. So throughout the talk, I kind of hope that
I’ll bring a few themes that arise when you’re thinking about types and type systems from
a theoretical point of view and one is this idea of syntax as a, you know, we’re all — we
all know about syntax because we spend all our time arguing with one another about what’s
the right syntax for a programming language but really here what I mean is this idea of
symbols and symbol-pushing really, that basically symbol-pushing is what is really what computers are really good at to a certain extent. And when McCarthy came out with Lisp he wanted a language for writing functions that operate on symbolic expressions. much of what we do in computing and programming
is really building symbolic representations of ideas and then computing over them and
much of what you do with type systems is that and how it gets implemented and how you reason
about them. But you know, just because you can throw symbols
up doesn’t mean you have any idea what they mean and at some time you have to think about
semantics and semantics is just a highfalutin’ word for what do I meaning you know, huh? So I’ll spend some time talking about whats the relationship between syntax and semantics since its a really big deal in basically any kind of programming. Programming languages
just happens to be writing programs where data is programs. Which is kind of cool if you like eating your own dog food. Any program you write is it going
to have some sort of notation and some sort of interpretation. And then the last is pragmatics. So in the world of linguistics they talk about
these three things and what I mean here is at the end of the day you will have some goal
that you want to achieve and you’ll do what you need to bridge that last gap to getting
that job done and focus on that. From a theoretician’s point of view, which
may not be the same thing from a practitioner’s point of view come up. So on to the meat of the talk. So this paper by Robin Milner, it’s great. It’s from the ’70s, I was actually alive when
this paper was written. That didn’t help me understand it. But Robin Milner, just a sidenote on him,
he’s a really brilliant British computer scientist. He’s no longer with us, unfortunately but
he did a lot of work on theorem proving and he wrote this LCF theorem prover and the
ML programming language came out of trying to solve the problem of how do I write a theorem prover and how write techniques for writing theorem proving. So it’s one you do like one amazing thing
and you do another amazing thing so you can get the first amazing thing done and then
he went on to work with concurrency and came up with these calculations especially for
the pi-calculus, for his body of work, he was awarded the Turing Award, and you always
thought it was cool this guy who blows your socks off, he didn’t have a Ph.D. but he was
really passionate about his work and thought — you read his papers and you get this sense
of intellect of really trying to think hard about problems and conceptualize them. So I really enjoy reading his papers and seeing
how he thinks about things, you know. Better with a beer. Not too many or you won’t understand. So the paper, you know, in the community on
types, this is kind of like, oh, beings this is the hindly/mill letter type inference paper. How many of you have programmed in Haskell
or ML or standard ML before so there’s quite a few of you and you’ve enjoyed your
experience of not having to spend all of your time writing down type annotations and some how the type checker does things, and this paper kind of codified a lot of those ideas and has been viewed that way I mostly want to talk about it from a different
point of view, that like its place in the world of type systems, which is that in many
ways, this paper really brought together what I call a conceptual blueprint for analyzing
types and type systems for how theorists think about types, and I’m hoping that I can kind
of convey some of those ideas through like a walk through some of the details of this
paper. So let’s just dive in. [laughter] Now, so … unlike the last talk there’s probably
going to be a lot more math than code in this one. There’s a lot of symbols, you but know, bear
with me we’ll kind of walk through it and you’ll see that like your intuitions as a
programmer really help you understand a lot of this stuff and the — the math starts to
get you at the conners, so as long as you don’t need to prove any theorems, you can
be like, yeah, I can kind of figure out if what’s going on if I put my programmer hat
on. Yeah, it’s just Haskell code, it just happens to be undecide-able, whatever. So, as I’d alluded to we start with the syntax which is in the top box. [laughter] It’s just data type, its just data. You have trees, programming
language theorists don’t worry about parsing or how many spaces, we just skip the whole
Pretty-Printing be like. We just skip the whole pretty printing part. Like, let somebody else do it like the previous
speaker and give me an abstract syntax tree and I’ll operate on that. So this is just a data representation in Racket of that symbology up there. So as you can see that one is a lot smaller
than that one which is why I think PLP people like to write this. Because you can translate that into Haskell
or into Ocaml. Or write a class hierarchy in Java and that’s your syntax. And its meaningless just as syntax. So this concludes the coding part of the talk. So going back, down below we have this is
the semantics, so this is really the definition of what these programs that you can write
in that language up above mean. Like if you give me one of these abstract
data types, what can I do with it? Like what’s the result that this program is
going to produce. And it’s basically an interpreter, like
you could almost take this notation and say, yeah, it looks a lot like the Haskell programming
language and if you look in the bottom left corner, the cursive e is just like, yeah,
that’s the name of my eval function and I just happen to have unicode, so I’m not going
to bother writing eval. So its like Math-Cal E And the fancy brackets, which are called Scott brackets, after Turing award winner Dana Scott Its basically just a notation for heres how we do pattern matching on our data structures. And each of the equations up there is like
pattern matching your data structure apart into all of the pieces that make up your data
and the last thing is called an environment and that’s essentially just a look-up table
and it’s a mapping from variables to values. So the idea is you have a type signature at
the bottom, but it’s like a math-type signature and it says if you give me an expression in
my language what what I will do is return you a function and what the function says
is, tell me what environment I’m in. Like, what’s the world around me like? What’s the value of X, what’s the value of
y, and I will give you an answer and the answer happens to be like, some stuff in math world
so you can think about this as basically an interpreter from the EXP language to math. And this ends up being a theme throughout
and it is kind of interesting that given any arbitrary piece of code you get back like
a meaning and it will be like tell me what the world is like and this will give you an
answer and this theme will arise again later. So interestingly enough, at the core of this ML language, it’s a dynamic language. It has all of these checks in its definition
and like if you look at the second line, what it’s basically saying that the first thing
it says is, well, v1 is basically what happens when I evaluate the argument position of a
function application. That’s a function application, and then if
it’s a function, then keep going, if not, then go down to the next line. Wrong! Like you have a type error. Like a Python-style error. But if it’s OK, then double-check running
the second thing and then if that threw a type exception, then throw a type exception,
otherwise take the first argument as a function and then pass it the result of the second
argument. So if you’ve ever written an interpreter,
by chance. Actually I’m curious, can you raise your hand
if you’ve written an interpreter before. So there’s a few of you who have. The rest of you probably actually but you don’t
know it. Most programs are really interpreters. But the basic thing is walk the tree and interpret it and we happen to implement EXP functions using math functions here. And if you are ever to implement an interpreter you’ll find that’s a really cool trick that
you can do, too. Oh I’m going to implement my Python functions using Haskell functions or vice versa if you’re sick. [laughter] Just kidding you can perfectly well do that Especially like interestingly enough, there’s
an interesting implementation of jit compilers using Python called Py-Py. So you can implement lots of languages like that. Another thing I’ll note is basically Every program runs, like as long as you don’t
have free variables floating around, you better have some meaning for your variables and that’s
what the environment is for here. So its basically all closed programs run and You don’t get wrong if you try to look up
a variable. Like you better have the — you always have
some meaning for it. So that’s kind of the kind of core of this
dynamic language and now, kind of the goal is how do we make those red circles go away? In Milner’s paper he talks about, yeah, you
know, you run into they silly problems where you decide to call — try and apply a number
as if it was a function and give it an argument and bad things happen And wouldn’t it be nice if that kind of error
just went away? Yeah, that’s what type systems are for. People had been doing this for long before
this paper came along, but he said, how do we take an analytic approach to thinking about and proving once and for all that our type checker does good things and keeps us from having certain kinds
of errors happen, specifically the ones that are listed as wrong here. There’s nothing on this slide that says divide by zero produces wrong. You just say ‘it produces divide by zero’ and that’s just not wrong. So when I say that well typed programs don’t
go wrong, you’re like, yeah, but they divide by 0. [laughter] Or like, you know, don’t worry about that. So let me start talking about types and I’ve
got this language, and interestingly enough, there’s like a bunch of prose up here and there’s and it’s basically like the syntax of type is as follows, it its basically just another definition of a syntax for types. And I list it as two things here, and it really
is again a data type, and but he separates his world of types into two different kinds
of types. And this is really for reasons of the kind
of language that he’s trying to define here, the way that ML’s type system works. So he has monotypes, which are basically types
that you’d see in any language, you’ve got integers, functions from integers to booleans,
functions from integers to integers to integers, etc. And he also adds this idea of polytypes. He adds type variables. You’re like, OK, so just stir in some type variables and keep adding arrows and now I’ve got these new things and give them a name called polytypes. And those are the types and so in this case he uses Greek letters, because PWL people can’t help but using Greek letters as a result of studying too much type theory. We know all of them we know the difference between cassi and chi, which is kind of disturbing. And now you types like have alpha to alpha and alpha to beta to alpha. Which is not the same thing as int to int and alpha to int to alpha. It’s like, OK, we can go home? No, we can’t. Because all I have done is written down more syntax. This is just a datatype. So what do these things mean to us? If somebody came from Mars and says what is this alpha, arrow alpha arrow beta. Well if someone came from Mars we discuss other things than interpreted types but Assuming that they were into programming, you’re wondering, what do these things mean, what does INT mean what do these types tell us. So what Milner does is give semantics to his types. He says there are meaningful things in the
world and it’s up to us to decide what they mean and be able to say something about that. So he starts by in a place that to me seemed weird. He’s like, OK, so our programming language, you know, you throw in expressions and values pop out and let’s give — first let’s give
meaning to the values that pop out of running your program and sort of like, yeah, but when I grew up, I always typed my programs, not the results of them, so what’s that about? And it’s like, well, this is a starting point,
because if you think about it, the values that come out of your program are in a certain
sense the meaning of the programs, so you want to kind of understand what the types
have to do with the meaning of your programs and then worry about the syntax of your programs later and we’ll get there. So he starts by giving a definition of the
semantics of his mono types, the ints and the int arrow int, and once you start looking at it you’re like, yeah, this
is sort of intuitive, but there’s some stuff that’s a little weird. So one thing that happens is that I had mentioned that math works a little funny and there’s a value in your language which is basically
infinite computation. It’s like, yeah, you can have infinite computation in your hands, pass it your friends, you know, share it and it’s like, OK, that’s a little
funny, but this is math. Math doesn’t care about nondecidability. So any non terminating computation has basically every type So like yeah, if I have a value and it’s not
terminating, I can say it’s an integer, I can say it has type bool, like why is that
OK? In a certain sense it’s OK, because that ship
has sailed, it’s not coming back. It’s like you can give me my infinite computation and add 5 to it and it’s not going to go wrong. [laughter] It’s just gonna go. So it’s essentially a design decision in that
I’ve decided that the meaning of my types is yeah, some programs don’t terminate but I’m going to be OK with that. I’m going to say that its ok that something doesn’t terminate and has type int. Same with functions. Now, your basic — your basic constants in
your language, he uses the symbol BI and he’s really referring to things like 42 or false
and he’s like, saying yeah, so a value has a Type INT if it’s an integer and a value
has type bool if it’s either true or false: So this is kind of mathematizing thing that feel pretty obvious. Now when he gets to functions I think it’s interesting. Aside from the non-terminating functions He says something like basically a value
is a function if it’s a mathematical function. That’s what the VEF thing is like. Yeah, make sure its a function. If its not then it doesn’t have a function type. And if it’s a function, then make sure that if you give me any value that has the domain type, where the domain is if it is int it’s a number, if it’s bool, it’s boolean,
but it could also be a function type, right? It could be a function from INT, to INT. Which is also defined in this definition. Its all like this recursive never ending weave Except that it ends because types shrink. And the definition of the type on the left in this definition is bigger than the types on the right So you work your way down. So it’s basically saying as long as this function takes something, and then produces a value, if it produces a value, then that value behaves like the second thing, this ADA, then the function has that type. So this is kind of mathematizing a behavioral property of a program. So to me this is very much like what people call duck typing. “Yeah if it walks like an int ->int and it talks like an int ->int, then it has typing of ->int. So now I’ve given meaning what it means in my language in terms of the semantics of values. What it means to have a type. And then yeah, every nonboolean computation has a type. Interestingly wrong doesn’t have a type and
that ends up being important. Wrong has a value in the language. So then all that was talking about was the
monotypes, right? Ok, int ->int, we’re cool. Int, we’re good. But what about this like alpha arrow alpha
or alpha arrow beta arrow alpha? No problem. OK, what’s going on here? This is like a bunch of notation. So in English what this is basically saying
is so sigma is one of these polytypes. It could be like all monotypes are also polytypes But it might have variables in it and then
this sort of less than symbol is saying, is mu which is like a monotype is like an instance of sigma, and so it’s basically saying V has this like polytype if every concrete type
that looks like this type with type variables in this is also a type of V. So to give you like a concrete example that
might make it easier, which helps with me, you could say, OK, what does it mean to have v have type alpha arrow alpha. If I have a value, it has type alpha ->alpha only if it has type int ->int and bool ->bool And int ->int ->int … etc. So any give
me any type, and as long as this thing can behave according to this behavioral specification of blah arrow blah, then v has that type, but it has to satisfy all of them. Make sense? So this is basically going to be a function
that takes something and returns the same kind of thing. Something that behaves like it, as far as
we know. So in a sense what we’ve done is built up
this tower of meaning for our types, and this is part of why this monotypes, polytypes is
separated. The monotypes are just like I know what int is, I know what int ->int is The polytypes are now that I know what monotypes mean this allows me to talk about lots of types at the same time. And say this one this has lots of types And in fact there’s an infinite number of
them. OK, so all this time I’ve been talking about
how do we type value. These things that pop out of our program. And so it’s like, yes, my values for running
a program are meaningful, and I can describe their behavior, how they can be operated on. Both in terms of monotypes and polytypes,
so now it’s like yeah, well, but I want to talk about my programs. By the time I get my value the ship has sailed. Like, please tell me about my programs before I even run them and get values. So you know, how do we give types to expressions? Well, yeah, Milner does this, but in a sense
his main goal in this paper is to try and focus on his main theorem which is like, whenever my type checker says that things are checked, things don’t go wrong and he sort of glosses over this, yeah, expressions have types, we can kind of give types to expressions so in
this talk I’m forced to do a little bit of violence to his paper and butcher it and put
it back together the kind of hidden story of what the types of expressions are. It’s there, but he didn’t tell the story there. But he didn’t tell the story that way. And it’s quite reasonable because really this is the first paper as far as I know that does anything close to this, that does this tight
connection between programs, gives meaning between what types and programs have to behave. And then talks about what you type checker has to do with any of that We haven’t even talked about type checking
yet, right? Hey, we haven’t talked about how do you type an expression. So here I start stealing bits of Milner’s
paper and kind of putting them together to describe. So he first starts with this idea of like
we need to be able to — we want to be able to talk about what the type of an expression is, not necessarily an entire program, but like a piece of code, a chunk of code, and
that chunk of code may have variables in it that aren’t bound, they’re like free variables,
so you need to kind of account for that. How do I even talk about a piece of code that free variables in it? So we start by saying we can build a list of what variables show up in that piece of code. He calls this a prefix. So then what he says is, if I have
a piece of code and it has free variables in it, then I probably want to say something
about what’s — what do I know about my piece of code, assuming some things about what those variables are going to be bound to? And so all you do is say, well, I’ll just
assign a specification to each of those variables. I’ll give it a type so he creates these things
called type environments. Now, as a side note I’ll note that if you
look in kind of modern papers or books like Benjamin Pierce’s: Types in Programming Languages. They don’t use this P overbar.
Milner was treading somewhat new ground, but he also hadn’t interacted too much logicians yet. He found logician religion later. In most modern notation, they’ll use this capital gamma for this thing that instead of mapping variables to values, it maps variables to types, so descriptions of behavior of values. So then he describes this idea that you can
say, what does it mean for a value environment? Remember that our semantics for our language has these environments, these ada’s and so what does it mean for one of these ada’s, a value environments, to satisfy or respect a type environment? And so a type environment says a variable
has a type. A value environment says that a variable maps to a value and all you want to do is make sure that the two mesh together. That whenever all the variables over here
say that they have these types, that the values the environment points to have values that
satisfy those specifications. so from those pieces, this idea that I can
say that a value environment satisfies a type environment and I can already talk about the idea that a value satisfies a type, then I can now say, what does it mean for an expression, and so I put a D here, D is the same thing as E, but Milner just happened to say, yeah,
we use D and E interchangeably and when I cut and paste out of his paper and I was like, why is there a D there and not an E and you dig back in his paper he’s like, Ds are Es
and he’s making me sad in the future. So I get to pass on the sadness. But not that Ds are Es. So he’s basically saying that given a type
environment and a specification for variables an expression D, so code, a piece of possibly open code, has a type, if and only if, for every possible value environment, that maps variables to types that — to values that satisfy the types that P bar says, then if
I evaluate, that’s the e, that expression using such an environment, I better get back a value that satisfies the tao, So that’s the semantics of expressions and
I’ll kind of wax poetic about that again, because this is really kind of the heart of
his semantics for types for expressions and this is really what does it mean for an expression
to have a type and it’s basically if every possible value environment that meets the
input spec P bar, yields an output value v, that meets the output spec tao, then and
only then can you say that under value the type environment P the expression D satisfies the type Tau. This input specification that this expression has an output specification. So it’s all written in terms of the meaning
of your programs, like using this e thing. Make sense? So this is kind of a sort of semantic model
of your types. You’re talking about types as meaning behavior and not like, you know, my type checker gave me an error about string list list, and it’s
more like, these are behaviors. So OK, great, now we have a definition of
what it means to be well typed, so all I have to do is if you give me an expression and
you give me a type environment, I just have to look up all infinite value environments,
Find how many of them satisfy my type environment and then run my program and see if the value that pops out satisfies an infinite number of behaviors that matches my spec. Piece of cake! And I show that you know this is in a sense
like it’s really a static analog to this idea of running your program, that usually you
take one environment, you run your program, you get a value, but now what we’re saying
is like for a class of environments that all satisfy a particular spec, running my program produces a set of values that satisfy this spec. So it’s kind of a global statement about lots
of inputs and outputs and it’s so so undecidable. [laughter] Like, no, no, you can’t just grab all environments and check in the general case. So it’s like, well, OK, so what do we do? Like I’ve got this great definition of what
it means to have something that’s got a type but I actually want to do some type checking or be able to say somehow that things are going to be OK. So that’s what we’ve got going now but it’s
going to be in a couple of steps. So just to recap what we did is we gave a
syntax and semantics of a language and then we gave a syntax and semantics of types first on values and Then on the code that you write. The resulting values and now we have types
for code and so the question is how do I even check that a program has types? And of course I can’t do it in general. I need to approximate somehow. So we go to this thing that’s called a syntactic type system. And now, you know, when we talk about type systems, you’re often like the type system is the thing that my type checker didn’t complain about whenever I give it a program. That’s kind of like a loose thing, but we
can be a bit more rigorous about what’s called a syntactic type system and I’m emphasizing this idea of syntactic because we’re now going to engage in symbol-pushing, that thing that computers are really good at. On the left is Milner’s definition of this
idea, what does it mean for a type environment P bar to syntactically say that an expression E has a type Sigma — and it’s like mumble, mumble,
mumble, that’s why it’s small. So that was an early definition of it, but
later on, as he as Milner found out more about how logicians think about proofs and building proof systems, he adopted that notation and others had, as well, and so this is still
kind of small, but it’s a bit more structured. There’s like a bunch of things with horizontal bars and names to the left of them, stuff on top, and stuff on the bottom. So I’ll note right now that basically for
all practical purposes, the thing that you’re looking at on the right is a description of
a data type. It’s like a recursive abstract syntax tree
kind of thing, but it happens to be somewhat context-sensitive so you can’t just hook any
two things together with premises. There’s going to be some conditions. So typically if I implement this in Racket,
I need to add a bunch of like contracts so every time I try and add something together and then I do a run-time check or I die and don’t build a tree because then the tree would be bad. If you have language with a really sophisticated type system like Idris or calk, then you can actually code in the type checker those rules, so you can basically build proofs as objects, these context sensitive things. This is sort of the secret sauce behind Curry-Howard based theorem provers. So let me give you a brief comparison between these two types systems: The
semantic type system and the syntactic one. Right now I’m going to kind of focus on functions. The two rules at the bottom are describing
kind of how the syntactic type system interacts with functions whereas this one statement at the top talks about the behavior of functions in terms of running programs and observing behavior. So the one on the bottom what it says and
it’s a little small, but it basically says, if I had a piece of code, and I was assuming an environment where some particular variable had a type, and then that meant that the body, the piece of code, produced this output behavior, then I could just wrap a lambda around it
and that function would have that function type. Now, that’s — I’m speaking intuitively in
terms of how we think about typing and if you thought about it you’d say like, yeah,
of course if the body of my function, given this particular type for a variable, was going to behave a certain way, then putting a lambda x said it should have a behavior about that
function. Now, that is our intuition about the step
of reason and we’ve encoded it in a bunch of syntax, so that’s like a syntactic proof. But while I sure hope I’m right. I really hope my language is sane and acts this way. I’m on the hook to prove it’s true. Similarly, on the other wise, what it says is if I have a function of type like tao prime ->tao, and I have an expression who’s type is tao prime ->tao, so it should intuitively produce a function and another expression of type tao prime if I apply the first one to the second one,
I should get the output result. So you’re like, yeah, intuitively that should
be true. So again, I’m on the hook to prove that. Now, interestingly, in both cases you can
think about these rules with respect to the syntax of your code. Like the things on the top are smaller code
than the things on the bottom, right? On the left you have some expression. On the bottom you have a function with that as the body. On the right you have two expressions and
on the bottom you have a function application of the two hooked together. So what this is describing is a way to reason about the behavior of my code by thinking about the behavior of small pieces and what happens when I hook them together. So I can think about what it — how my code
behaves syntactically and in pieces and so modularly, one piece at a time, and then compositionally by hooking them together. And that’s really one of the secret sauces
of type systems in general is the syntactic idea of reasoning about how my program runs by thinking abstractly by the behavior of each piece. This is kind of the heart of type driven development. And it ends up being attached to the meaning in terms of behavior. so now we have to like, we have some due diligence to fill out, which is how do we relate this thing down here, description for building
these proof trees, kind of like in geometry where you have lists of proof steps and you
say by whatever rule and we have to relate that to the semantics. So we do that with a proof that’s called a
semantic soundness and basically here is Milner’s proof of the syntactic soundness that connects type assignments, our trees of proof rules, to actual behavior, and I’m rewriting it in
slightly — almost more modern notation and it’s basically saying, if I have a data structure who’s like, that is a proof of blah, blah, blah, that’s what the single, that’s the thing
with the single turnstile after the p on the left is, then something meaningful is true
in the world and you can see that both of these look exactly the same. I defined the one on the left because Milner didn’t bother doing it, but this is essentially what that theorem is saying just slightly factored differently If I write down a proof, it’s actually true
about the behavior of my code. And it really does say, like every proof of
type assignment says something meaningful about my code and it relates syntax to semantics: Now conveniently as a corollary we achieve Milner’s big goal Which is like “By the way, wrong has no type so every well typed program go wrong”. This was his goal. Well typed programs don’t go wrong. And he could prove that by having coming up with this behavior specification. Now it’s useful to note that this was already true about the semantic systems, just that he didn’t bother bringing it out until he had already connected the syntax to the semantic. And he’s like now I know that if I can build
one of these proofs, then I know that my code won’t go wrong. So all I’ve done is describe a sort of data
structure, right? It’s like, oh, I described the data structure
and like if you build me a data structure that when I look about it says something about my code, then something is true about my code And the questions is “How do I build a data structure that says something about my code?” That’s what type checking is. So Milner’s language has this type inference thing, which really every language has to some extent. You have a program, you have — I didn’t give
you a — like when I program I don’t program by writing proofs of typing trees, what I
do is give you a bit of code and then what your type checker does is try to find a tree
that corresponds to your code and it just happens to be particularly sophisticated in Milner’s case and so he develops this algorithm called algorithm W. There’s algorithm W. You can see it in much detail as you need, which is it takes a bunch of lines, it’s describing a bunch of computational steps and what you need to know is like, is it any good? OK, you gave me an algorithm, takes a program, and then it makes a claim, yeah, this program has a type, there’s a type or no it has an
error, I can’t type it. So this is where another proof comes into
play and this is what he calls syntactic soundness and this connects the result of type checking to this definition of type assignment, these trees. Now, in turn type assignment is connected
through semantic soundness to behavior. So it’s a two-step thing. I have a program who’s job is to take programs and generate typing trees and then I have a theorem that says they mean something. So what this says is that if Algorithm W returns a type assignment, says that this program has a type, then I, the person who writes the theorem, could build a corresponding proof in this
case. And what you do is you basically discover
that, yeah, what the algorithm is doing is it’s stack trace is building the tree and
then it’s throwing it away because you don’t actually care about the tree, you just care
that the program has a type. You care that it has a type, which then means it doesn’t go wrong. So let me kind of bring everything together
about what’s kind of going on in this mathematical model. At the top level as a programmer you’re thinking about, I have a type checker for my language and it performs computation. I give it a program and it gives me a thumbs up or a thumbs down. Thumbs up is a type and a thumbs down is you need to add more list brackets around your S That in turn is connected to this idea
of what is a syntactic proof of a types element and it’s really a proof that a program has a type following the syntax of your program and the nice thing about that is it really
allows you to think locally about the behavior of your program. You don’t have to take the whole program and say, given a whole program, what can I find out about it? It’s like by looking at pieces, modules, libraries and then look hooking them together, I can understand something about them as a program. And I split it up across and organization and provide interfaces. And then the last bit is — well, Milner came
up with a meaning for his types. What does it mean for an expression to have a type? Like, yeah, if it has Type INT, it better
diverge or produce a number, or throw an exception or leak my passwords or —
[laughter] Given any programming language it’s up to
you to decide what the guarantees are that your types give you. To some extent they seem to pop up very similarly again and again, but at the end of the day you ultimately have to decide what the definition is and whether or not you can build a full thing that can stand on top of that definition. So in many pieces of work on type systems, the part at the top where you have this type checker and this type assignment is viewed as kind of obvious. It’s like, if you’re not doing crazy type
inference, then you look at your proof rules and you say, do recursion the other way. Like, I can see what my program looks like,
I know which rule I’m going to use, I need to search for something that’s smaller for the other pieces. Milner’s is more complicated because you didn’t tell him what types were so he has to do something much more sophisticated. Which is why he needs to talk about the algorithm and talk about the proof In many cases you’re like turn your head upside-down, type checker. The other thing is that as I mentioned at
the end of the day, what Milner really wanted was he wasn’t trying to give a semantics of
types. That wasn’t the main goal of the paper and
it’s not really what he talks about in the abstract of the paper. What he talks about is I prove a theorem that says that well typed programs don’t go wrong. He doesn’t say that I prove a theorem that says that well typed programs behave according to what my types say, because that really wasn’t his main focus But it’s a useful thing to know and to think
about and just happens to not be what he was doing and much work on type systems really doesn’t worry about the semantics of types, it just worries about I need some way of proving that if my type checker says something, then well-typed programs won’t go wrong, and so later work that I’ll talk about just very briefly kind of comes up with a way of doing that, like skipping that step of oh, don’t bother giving me your types, your informal
understanding will do, and we will go from there, and you can prove that your type system guarantees this sort of non-wrongness soundness. So, yeah this is a particular mental model
for thinking about types as somebody who’s being very analytic and precise while analyzing semantics of a programming language. And much of the work on type systems that theorists do builds on top of this work and some pieces collapses depending on the needs of the researcher. So at the end of the day, you know, I ask
like, you know, what are types? What are these things? Well, as I mentioned earlier, it’s like programming languages, they have this syntax, you know, you have to write something down, they have semantics, they give meaning to them in terms of the evaluator and there are some pragmatics, at the end of the day I want to run closed programs with maybe like library functions. Interestingly enough, types have syntax, you get these arrows, there are these things called INT and bool, there are semantics which say what do these types have to do with the behavior of my programs And there are some pragmatics which is like better be true that they go wrong, no, it better be true that they don’t go wrong. So really a type system is a language, so
in particular it’s a language specifically geared for talking about properties of programs and program fragments. So when we talk about static checking or dynamic checking or static typing or dynamic typing At the end of the day, we’re talking about
a language that is ultimately separate from the language that it’s talking about. It’s a different language. And but the mechanisms by which we check or enforce types is what introduces sort of static checking and dynamic checking and this is
kind of the thing that it’s taken me way too long to figure out. So I’m running out of time so I wanted to
give you a brief whirlwind tour to set context for the other papers I brought up and I why I think they are important in this context. So I wanna kinda focus mostly on the ones I think are the most important The single most important next paper in my view came out like 20 years later, almost. So things take time and this one is called
“A syntactic approach to type soundness”. The syntactic is really important. So Milner came up with this conceptual blueprint for analyzing types, and people went off and started trying to use this technique and a few people managed to be successful. And there were a few soundness proofs like I described, but not a lot. Then in the ’90s, kabam! This paper came along. And it really provides like, a practical blueprint for analyzing types, especially with respect to proving that well typed programs don’t go wrong. As described to me by a friend of mine, Neil Christian Murphy at Cambridge Basically before this paper was written, like
basically no one ever proved type soundness of anything. After this paper was written, it was like
“soundness soundness soundness soundness soundness”. A bunch of people were able to do this for various languages, low level C like languages, high level
functional languages. This really came up with a nice practical
technique for doing it. And almost everyone uses these techniques these days. If you’ve ever heard of progress and preservation. Most of that was in this paper and a follow-on paper from Bob Mellor from Carnegie Mellon the same year. Now from another point of view, there were also these two papers which were about a decade apart but are really close in flavor to one another. So the way I was describing the behavior of
type of values, you could be like, oh, I think of the type being as a set of values that
have this particular behavior. So Jim Morris who wrote this one paper, he’s like, no, don’t do that and he’s very clear about it in his title and he’s like, types
are not sets. What he’s arguing is And its a beautifully written conceptual argument, it’s not that it’s a matter of
fact, but it’s really useful to think about types as like comparing multiple programs
against one another with respect to behavioral specifications and this becomes really important when you start talking about things like abstract data types and information hiding and the
only way to prove for sure that your particular type system supports information-hiding is
it to use this different relational description where types relate to one another. And Reynolds came along and actually showed how to do this in math. So then the last one that I wanted to mention and there’s plenty more. This is actually a Ph.D. thesis so it’s not
short but I should mention that I really like reading Ph.D. theses, because they tend to
be written by someone who’s just discovered how things work and is sort of close to you
— well, she’s not, she’s way smarter than me. But is able to say things in a clear fashion
over a lot more space with more details and it basically talks about here’s a practical
way to do the things that John Reynolds who’s like, oooooh, could do that the rest of us
couldn’t, and use some techniques that are very reminiscent of Wright and Filisin did. And this comes many years later. So that’s the end of my talk, and I just want to put up basically one of the the main takeaways that I wanted you to get from this talk. Which is really that, the way to think about types is they’re a
language in their own and that we then use that language to think about the behavior
of our programs and figure out how to enforce and check them. So thanks a lot. [applause]

Leave a Reply

Your email address will not be published. Required fields are marked *