[MUSIC] In this segment, I want to continue our discussion of how ML's polymorphism allows some types to be more general than other types. And then also point out this strange feature of ML, equality types, that you might accidentally run across on homework two, and it's okay if you do. So, to take a simple example, suppose that you were required on a homework assignment, or just as part of your job, to write an ML function that took two list of strings and appended them together. And you went off and you wrote a wonderful function for append like you see here. And you expected it to have type string list * string list -> string list, but as we've seen code like this in fact gets a polymorphic type of alpha list * alpha list -> alpha list. This is okay, your job is done and we want to talk about why. Now we already know the informal story that if you do write this code and it has this type, you'll be able to call a pen with two lists of strings and get back a list of strings that has four elements in it. Or, even though this wasn't part of your job, you could call with two list of ints. But what you couldn't do is call the list of ints and a list of strings. And in fact you can tell that just from the type, because what I want to convince you of is that even though this quote a this alpha, can be any type, it has to be the same type throughout the overall types. So these three uses of alpha have to be replaced consistently with some type, whether it's an int or string or pair of ints or whatever you'd like. So let me explain how that works, in general. We can say that the type alpha list * alpha list -> alpha list is more general than the type string list * string list -> string list, and in fact this polymorphic type can be used at any less general type. So it could also be used at int list * int list -> int list, but it is not more general than something where the first alpha is replaced by int and the second alpha is replaced by string and the third alpha is replaced by int. Because we did not replace alpha consistently. So the general rule is, a type t1 is more general than a type t2. If you can take t1, replace it's type variable consistently so every alpha replace with one type, every beta with another type either the same or different with what you replaced alpha with and so on to get t2. So you can replace alpha with int * int, you can replace alpha with bool and beta with bool. You can replace alpha with bool and beta beta with int. You could even replace each beta with alpha and each alpha with alpha. And I don't have an example of that here but you could take a really polymorphic function and come up with a different type that was a bit less general but still had some polymorphism in it, okay. So that is what we have been doing. Let me now combine this with a couple other rules I have told you about before. Remember our whole idea that if you see type synonyms, it doesn't matter whether you see the type name or what it's a synonym for, and remember that with record types the order of the field doesn't matter. So, here's an example on the slides, supposed I have some types synonyms where type foo = int * int. And supposed that you write some homework function and the type you get for some part of it, is some record type, where I have a quux field of type beta, a bar field of type int * alpha, and a baz field of type beta. Now, the question is, is that more general than this type here, the second record type you see on this slide? Because if I asked for this second one, and you wrote something of the type first one and it's more general, then that's okay. And it turns out that it is, because for this record type to be more general than in the next one, it has to have all the same fields, and it does. It has quux, bar, and baz, quux, bar, and baz, and each field of the less general line has to be created by this sort of consistent instantiation. And every beta has been replaced by string and then there's bar field is even more interesting, if you replace the alpha with int and it's the only alpha, so we are replacing the alphas consistently. You would get int * int and since foo is the same thing as int * int, indeed this second type is less general than the first type. Another thing that is less general than the first type is this written here. It turns out this last type is absolutely equivalent to the middle type. It has all the same fields, and all those fields have the same type. The only difference is, I've re-ordered the fields, which never matters, and I've replaced the foo for the type of bar with int * int. So, this is the sort of thing you might have to do on homework two, that ML type checker tells you one thing and you'll have to check using your own brain that it's more general than the type that you needed to produce. So, that's one thing that you might trip across, here's an even somewhat stranger thing. You might see some types that have two quotes before a type variable. So ' ' a instead of just ' a. So for example, here's a type that says I take an alpha list and an alpha and return a bool, but these alphas have this extra apostrophe at the beginning. What that means is that these are equality types. So indeed a function of this type is polymorphic, but you can't replace the quote quote alpha with any type you want. You can only replace it with types that you can use the equals operator on. Now we have mostly only used the equal operator for int, to compare to ints, or for string to see if they are the same strings, but it turns out it works for a lots of types. It works for tuples as long as all the pieces of the tuples are themselves equality types. But not everything is an equality type, it turns out that ML in order to enforce good style doesn't let you compare values of type real floating point numbers with equals, because that's pretty much always a bad idea, and doesn't let you compare function types with equals. Something that will get into in subsequent segments when we're passing functions to other functions and stuff. So, the rules are exactly the same. If you see a type like this, it works for any type as long as you instantiate the alpha consistently. But certain instantiations won't be allowed. So this is a rather strange feature of ML. It basically treats this equal operator specially, has special support in the type system for things that can be compared with the equals operator. And it's not something that I plan to study in depth, but in case you see it, I wanted to prepare you for it. Here's a very short example of how it may come up. Suppose you wrote this function, which is takes an x and a y, and if they're the same turns the string yes, or else is string no, and maybe you thought you were intending x and y to type int, but instead, you will get a type like ' ' a * ' ' a -> string. You would also get a warning from the ML type checker about calling polyEqual. You can ignore that warning. But you might not ever see this sort of warning. So here's the second function that uses the equals operator on this argument x. But since it compares x to 3, the type checker knows that you can only ever compare two things of the same type. That's the typing rule for equals. So in fact x has to have type int. You would see that over all this function has type int error string, because it must take an int and it must return a string, and there is nowhere we had equality types anywhere to be seen. So those are the strange things to look for. There's a very nice precise rule of one type being more general than another, and you'll now get a lot less confused if you see unexpected polymorphosis on your next homework
