Type Annotations

[00:00:00]
>> Richard Feldman: So as we have seen, everything up to this point. [LAUGH] We have not even discussed a syntax for type annotations because yeah, Hindley-Milner, it's decidable, it's great. You don't need to annotate your types if you don't want to but now we're going to. There are multiple reasons you might want to annotate your types.

[00:00:16]
The most obvious one is that these can serve as essentially comments, except that they are verified. So if your comments, you write a comment over that says, hey, this is a string, but then later on, it stops being a string. Nobody tells you about the comment being out of date, you just are unpleasantly surprised perhaps.

[00:00:31]
Whereas this thing, if I actually were to change this to not be a string, then I would get a type mismatch. So that's a convenient thing, that type annotations can do. A subtler thing, that type annotations this can do is that, although it is the case that in Hindley-Milner, well actually we'll talk about that in a sec, so I'll come back to that one in a sec.

[00:00:48]
There was another thing that you can do with type annotations and we'll come back to it. So yeah, here are two different type annotations, string and number. We're not gonna get into syntax too much of type annotations, basically just kind of TypeScript. Like I said, they're really an afterthought in this course, the main purpose is, let's talk about the type inference.

[00:01:05]
And then annotations are just a by the way, this is a thing you probably want to. So go through and do our usual assignments of these things, okay, all this very familiar. The thing that the type annotation gives us is that we can basically say, okay, I can go ahead and actually put an additional constraint here.

[00:01:23]
Now we don't actually, at least in the case of something like string, we don't need to go and make a separate type idfor it, because it's really only doing one thing in one place. So much like with our lookups, we can just say, okay, this is just a constraint, so we're just gonna unify, we're gonna do an extra unification here with string, but we don't need to store it.

[00:01:43]
Because nobody's ever gonna be like, hey, I have the same type as that thing's type annotation, that's just not a thing. So all we're gonna do is we're just going to be like, okay, I see this annotation, got it. I'm just gonna add one more unification on the pile and basically say, okay, because this thing has the type string, I'm gonna unify 0 with string, and then that's it, we're done.

[00:02:00]
We just have that one unification in the mix, and then the type annotation is essentially discarded at that point. Same thing with numbers, just like, yeah, just unify this thing with number. One way that you can think about it is that the purpose of a type annotation is essentially to just be an extra constraint or an extra unification.

[00:02:16]
And we're gonna come back to that word constraint in a second. So this does, it is a meaningful constraint, right? So if I did try to annotate it as a number, and then I tried to put a string here, well, that's end up being a string. And then I unified the string with a number, then we get a type mismatch.

[00:02:31]
So the way that you get type mismatches out of type annotations in a Hindley-Milner language is basically just the same way you get type mismatches absolutely anywhere else. You just unified two things and they were both concrete types and they were different concrete types, and that's a type mismatch, so this is exactly how you would do that.

[00:02:48]
Okay, now there's actually a more precise way to talk about what Hindley-Milner gives you, which is that it is not only decidable type inference, but it is principle decidable type inference. Now, not all Hindley-Milner languages have this, so there are certain type system features, which, if you put them in your type system, you stop.

[00:03:05]
You're still decidable, but you're not principle decidable, so I'll explain what that means in a second. But as an example, so if you have rank one types, definitely not gonna get into what rank types are. But if you're familiar with Haskell, there's some extensions called rank two types and Rank-N types, and the default being rank one types.

[00:03:21]
A really subtle distinction here is that if you have Rank-2 types, that means you are principle decidable in Haskell. If you have Rank-N types, you lose the principle part but weirdly, and this is such a strange thing because this so rarely happens in computer science, rank two types are still technically principle decidable.

[00:03:39]
Rank-1 and Rank-2 both are, bur rank anything three and above stops being that. I don't know enough type theory to know why that is, I just know that it's that way. Based on this, I looked into, hey, could we have ranked two types in rock and not sacrifice principle decidable type inference.

[00:03:54]
And I got two pieces of advice on this, one was from a professor at Upenn, Stephanie Weyrich, who was basically like don't do that. [LAUGH] She went down the Rank-2 rabbit hole and was like, no, it's not worth it. Just either keep your principal decidable or go all the way to Rank-N, just that middle ground is not worth the effort.

[00:04:12]
And then the other was we were actually looking into it with rocks like Cogen. It turns out that there are some type system features that actually interact with and restrict. What you're able to do in terms of high performance code generation if you're going straight to machine code or web assembly like we are here.

[00:04:27]
So for both of those reasons, yeah, Rank-2 types, maybe not the best choice. I mainly give that as an example of there are good reasons that a language might choose to sacrifice this. It's not like if you don't have the principle part of the type inference, you're just making a mistake but just talk about what that is very briefly.

[00:04:43]
So decidable, like we mentioned earlier, at the very beginning when we introduced Hindley-Milner type inference, this means that the type system always infers the correct type okay. Unless there's a bug in the type checker, which we would never write bugs. But if some other person were to write a bug in a type checker, then yeah, the idea is that the algorithm itself always produces the correct type.

[00:05:00]
So assuming the algorithm is implemented correctly, that's gonna happen and it never needs help from type annotations. So we've definitely seen that, haven't written any type annotations yet, and we're at the very end of the type checking section. Principle decidable type parameters means that the type inference always infers the most generic type, the most flexible possible type.

[00:05:20]
And the practical upshot of this, it means that it is not possible in the language to add a type annotation, which makes that type more flexible. But you can add a type annotation that makes the type less flexible if you want. So an example of this is you could have an array that's basically like I am an array with like an unbound type variable.

[00:05:38]
Really easy example of this is empty array, that's unbound type variable. Empty array is not an array of strings, it's not an array of numbers, it's an array of unbound type variable I don't know it works with anything. But if you want, you could say X equals empty array and slap a type annotation on there that says X colon array bracket string.

[00:05:57]
So you're like this is an empty array of strings, okay and if you want, you can do that. And the reason that that sort of just works naturally is because, as we've seen from the previous section, all these things are doing is it's just unifying whatever the annotation says with whatever this type is.

[00:06:13]
So you can of course, use that to constrain something, because that's just one of the things that unification can do. If it is going down and traversing down and trying to combine these things and find some common ground there, it might say, okay, well, array of string unifies with array of unbound type variable.

[00:06:29]
Well, we descend down and unify string, which is a concrete type with unbound type variable, which is null and string sort of wins. And this the null gets similar to that, or just outright replaced, either way, you end up with array bracket string if you unify those two.

[00:06:43]
So even though the type inference says, yeah, this could be this flexible, you can annotate it to make it less flexible. But principal decidable type inference means that you cannot annotate your way into it being more flexible than what it would be. If you can, then it's not principal anymore, yeah.

[00:06:57]
>> Student: I had a question to go back to the previous slide.
>> Richard Feldman: Yeah.
>> Student: Why is it that, for example, id0 and 2 are referring to the IDs of the other elements in the table, as opposed to just the concrete type string, for example, since you're doing unified zero and string here?

[00:07:18]
>> Richard Feldman: I see we're saying, why is this not overriding that one?
>> Student: Yeah.
>> Richard Feldman: Yeah, I mean that's, I think that's just a typo on my, like these, they're similar to each other so it doesn't matter. But you're right, they should be swapped but you'll end up with the type checker doing the same things but yeah, I think you're right, that's just a slight mistake.

[00:07:33]
[LAUGH]
>> Student: No worries, yes I'm not sure it was in a specific, you know what I mean?
>> Richard Feldman: Yeah, you weren't missing anything but yeah six one half dozen, the other, yes it should have been the other slot. [LAUGH] Good catch. Okay, so the other thing about Hindley-Milner is that is a sound type system, we talked about this earlier as well.

[00:07:50]
So basically this means that this type system has no concept of runtime type mismatches. So now that we're at the end of the type checking section, we can once again see this. There was no point at which we were like, and here's the spot where you can have a string here and a number here, and then if you got the wrong one at runtime, we crash.

[00:08:06]
It's like, no if you ever had a string here and a number here, potentially, that's where we have a type mismatch, and we report it to the user at build time. That's the only thing we even have a concept of in this type system, so all type errors, I should say, are reported at build time.

[00:08:19]
Also the implication of both of these is that all types are fully known at build time. So even if we know that the type is a bound, that basically means what we know about this type is it could be anything at run time. It's the identity function like, one of those type scenarios are in an empty array.

[00:08:36]
Yeah, the information about its type is that that type is maximally flexible because you can use it with whatever, it's polymorphic. Yeah, so in summary, basically, we talked about polymorphic functions, arrays and how they can be polymorphic as well. And finally, type annotations, at long last, we actually finally got some type annotations in here, right at the last minute, under the wire.

[00:08:54]
And yeah, that's because, with him, lemon type that prints, you don't have to have them, they're completely optional, yeah. Would it be fair to say that committing in ways to Hindley-Milner and the conventions of it helps us with polymorphism because it sets a more strict bound early, it defines our possibilities upstream, so to speak?

[00:09:17]
I'd say it's pretty subjective, the question of does committing to Hindley-Milner make your life easier in terms of polymorphism? Because you're sort of committing to a certain rule set that's pretty simple, but also pretty powerful. Yeah, reasonable people can disagree, I would say some people would say yeah, I totally agree, it's great, it's simple, it's awesome.

[00:09:36]
Other people might say, but the type of polymorphism I wanna do is not easy to do in this system. I wanna do subtype polymorphisms and stuff like that, so yeah, I wouldn't take a stand either way on that. [LAUGH] Personally.