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]