scala.bythebay.io: Adelbert Chang, Spoiled by higher-kinded types
Recording: scala.bythebay.io: Adelbert Chang, Spoiled by higher-kinded types
Uh today I'm here to talk to you guys about higher kind of types. Uh this talk was in part motivated by what I hope were tongue-in-cheek comments by a lot of my friends and co-workers about languages that were coming out uh like Java 8 uh with first uh first class functions and these comments generally went along the lines of well Java 8 has first class functions so there's not really any big reason to use Scola now right uh especially because so many more uh uh is this better is the mic on this maybe it's not on the Is this there? Okay, there you go. Cool. Uh, so yeah. Um, a lot of my co-workers like Java 8 is out. There's not really any reason to use Scola. And for me, that's frankly not true. And I'm sure for many of you, that's not true
Uh, what Scola has to offer, I think, is much more than just first class functions. Uh, first class functions tend to be sort of the bottom the baseline against uh which I measure languages. When I look at a language, I sort of expect it to have first- class functions at this point. Uh, especially languages that operate at the scale or at the level that Scola does. Uh and so one of the big things that Scola offers in terms of uh features is higher kind of types and this is a feature that I don't see in many other languages uh but I find extremely useful and I well I'm spoiled by them at this point. So many many times when a co-worker tells me about oh have you checked out this language one of the first things I go look for is higher kind of types and sadly more often than not uh it doesn't support it. So my goal in this talk is to introduce higher kind of types and motivate why uh we should care about them. So to get a sort of uh feel for the room, how many people have used future.sequence or future.traverse from the standard library
Yeah, a lot. Um so one of the most common questions I get both at work and in IRC and in Gter uh is how do I do something like future.t traverse except instead of future I want to use option or I want to use try or I want to use either. Um, and so it turns out, let's see, can everyone read that? Uh, can everyone read the screen here? It's all good. Uh, so I have a simplified version of the future.t traverse here. So for those who who don't know, uh, futuretraverse is, uh, sort of like a scattered gather thing. Uh, you have a list of A's and a function from A to future of B. And what it does is it takes, uh, every single element of the list. It forks off some computation and then, uh, gathers all the results into a future of a list and then returns
Um and a lot of times people want this same behavior except instead of future they want to do something like option or use either uh where they're doing something like validating uh a dynamic list of inputs right some user input and they want to run some validation function again uh against it um and they want to do this with other data types like IO and and state or whatever but it turned out the standard library doesn't provide this as far as I know uh and you could actually go off and write traverse for option traverse for either and at one point I did have like a single file at work that was just traverse option traverse either. And when you do that, you'll quickly see that there's the code is largely the same. Uh so similar that you it's kind of screaming for like abstraction. And it turns out this abstraction is only you can only really encode this kind of abstraction if uh your language supports higher kind of types. So to give sort of sneak peek about uh to give a sneak peek of of how this function looks like, I'll just go ahead and write it. So I'm going to write a traverse that's uh parameterized over some f right. So this f is going to take the place of the future in the standard library and other than that it's going to remain largely the same. So we're going to start that's going to bother me
Uh we're going to start by folding over a list and we have we have nothing to collect so far. So we're going to start by uh we're going to start with an empty list of these. We're going to lift it into whatever this f is. So if f is future, we would start with the future an empty a future of a list of b's and the function is going to expect uh the the the next a in the list the accumulator we have so far and we need to return another f of list of b. So we can do that by first applying the function to a. Then we can tuple that uh that FB with the accumulator we have so far and then we can map over it uh by uh prepending the the first element with the second element. Cool. So uh now what we can do is we can take a list and I'm going to traverse over the list and I'll do something like future I* 2 and this will give me a future of a list of int
So that works right so now we're at feature par with the with the standard library. Now we can use the exact same traverse function and I can do something like if I mod 2 double equals z sum of i / 2 else none. So this is sort of like a a dummy uh validation function and this will give me an option of a list event. So it's the exact same traverse function uh but I'm swapping in uh instead of future I'm going to use option and we can also do something uh like this maybe if I wal left oops else right of uh 1.0 / i and this will give me an either of a string of a list of double I believe and the compiler actually needs a little bit of help at this point. So I'm going to annotate the types and that works right. So so we're seeing uh we've written traverse once once and for all and we're able to plug in whatever types you want. Uh and it turns out that in order to write this traverse this way we actually need our our language to support higher kind of types. And so in languages like Java 8 that don't have those uh we actually couldn't write traverse at least not uh not easily
So uh I'm going to try to introduce higher kind of types now uh to sort of give motivation for why we care. I'm going to first talk about uh things at the value level. So in many languages uh we have this uh we have two separate notions between values and functions. Uh values are sort of things that we can assign to variables things we we have a hold of we can pass to functions and get values back. And then in a separate world or a separate universe we have functions which aren't values but they are able to take values and produce values but functions themselves aren't values. And so in these kinds of languages uh we quickly run into certain situations where we can't talk about things we want to be able to talk about. So uh a very simple thing is if I have a collection of elements I want to apply some function to each element to to get a new list right and I'm using recursion here and many languages will just use like a for loop and this becomes this be this has become so natural to us that we sort of we know it's like code duplication but our eyes sort of like see through all the the noise and and uh see what we want to do. So in this case I'm just doing something uh really simple
I'm just taking each string and duplicating it. Uh in another case maybe I want to take each character and get the integer code associated with it. And then in some other case maybe I just want to check if the integers equal zero. And you can see that the code here the code remains largely the same. Um and the only thing that's really changing is what function we're applying at each element. And we'd like to be able to say we want to write this kind of uh this traversal once and for all. But in a language without uh first order uh first class functions, we we wouldn't be able to say give me a function as an argument and I'll apply that function to each each element, right? So we end up having to either uh do a lot of duplication, write the for loop multiple multiple times. Um and that's not good
So of course we in Scola we we do live in a language with uh first class functions. So we are we are able to write this kind of thing map once and for all and say give me a list of a a function you want me to apply each element and then uh I'll go ahead and and do the thing you want. So without again without first class functions we wouldn't have been able to write map right at least not not in a nice or easy way and we can write all the previous functions in terms of map but usually this is just so simple that you would just inline it instead of defining it this way. a similar situation uh we run into a similar situation uh at the type level. Right? So now we're going to go from values to types. U in many languages we have a distinction between uh proper types or fully applied types or uh what's called uh types of kind star and then we have sort of functions at the type level or type operators uh functions that so you can think about uh type constructors uh which are things that take a type and produce a type right? So these are sort of like functions at the type level. And again um in in a lot of languages we have we have this distinction and just like with the in languages where we don't have first class functions uh we we run into uh problems where we want to be able to abstract away something but we're not able the type system doesn't give us the feature that we uh that we need in order to talk about these kinds of things because we have this separation between fully applied types and type constructors. So uh here's an implementation of traverse future, right? Where uh we're we're specifically traversing the list using a future
And if you compare this to the code I wrote at the beginning of the talk is it's largely the same. We're going to start with empty list, lift it into a future, uh take two futures, zip them together, map over it to prepend, uh and we're done. That's the code for traverse option. Uh you there's a little bit of noise just due to the way uh zip works on options in a standard library, but it's largely the same. lift into option zip map and there's traverse either. So you can see at this point like code is pretty much the same here, right? The only thing that's changing is is how we're lifting it into whatever f we choose. We need to be able to zip them together and we need to be able to map over it. And so we want to be able to abstract that notion out and allow users to sort of tell us what f they want and uh just write a traverse once and for all
And so there's an abstraction that um that exists that's very useful uh called applicative. And this is where the importance of higher kind of types comes in. Right? So applicative sort of encodes the three operations we need. We're able to lift some A into F. We're able to take two fs and tuple them together and we're able to map over it. And if you look at what applic or or a vector of A. It's applicative takes it as an argument a type constructor. This is sort of like writing a function that takes as an argument a function
Uh and you can see this when we implement applicative for future or for option or for either where we're not saying uh I'm defining an applicative of a future of int. I'm I'm defining applicative for for future the type constructor itself. And with applicative in place uh we can write traverse once and for all right just like what uh we did in the beginning. And this so where before we had map uh for map we gave it a a function that that allows us to plug in the behavior we want for traverse we're giving it a type constructor uh that allows us to define how we're doing the traversal over the list and just like with uh just like with map we're able to define all the the various traversals we want because traverse is usually it these are sort of trivial uh and indeed for future an option and it should be the case for either uh the definition is same these are usually just inlined, right? So now we're able to talk again uh about abstractions that we otherwise would not be able to talk about without uh higher kind of types. So I've mostly been talking about traverse mostly because that's like by by and large the most common solution to like to many problems I see. uh we there's sort of like a joke in in a lot of uh IRC and gitter channels I hang out in where if your question starts with I have a list of something the answer is probably traverse and turns out often enough that that tends to be the case but now I want to show you guys some other examples because I don't want to say like the whole reason we care about higher kind of types is just so we can write traverse we want to talk about other things as well so let's see cool so we have our French traverse again uh but what I'm going do is I'm going to implement uh functions in terms of traverse but those functions aren't going to be like the usual traverse option traverse future that we've been talking about. So the first thing I want to show is uh map uh a familiar friend. So map looks like this right this is the this is the map from the standard library and uh I want to implement map in terms of traverse and if we look at the type signatures of the two uh they're kind of the same but there's some slight difference right so both traverse and map take in a list of a as argument uh traverse takes the function that traverse takes is a to an f of b whereas map just takes an a to b and traverse returns an f of a list of b whereas map just returns a list of b so we need to uh because we're implementing uh map in terms of traverse, we're able to pick what f we want
Uh so we're in control of what f we we we choose and basically we need some f that encodes exactly as much information as what its type parameter is. And uh indeed we could write a type uh that does that and that's often called the identity functor or just identity uh data type. And if you look at a definition, it's pretty straightforward. It literally just wraps a value of type A, right? That that's all it does. And and it might seem pointless until you see until you remember that applicative requires uh as its argument a type constructor. And now this identity data type is is of the correct shape. Right? Identity takes a type parameter and produces another type. Uh it just doesn't do anything else beyond that
Uh but with that in place we can actually write an implicative instance for identity. Right? So we need to implement these three methods. Uh pi says give me an given an a I want you to give me an identity of a which is straightforward. Uh to tuple together two identities uh that's also pretty straightforward. And then map is the usual thing you would expect. Just get the values out, apply the function, rewrap it. So we've got our applicative for identity. If we go back to that file, I can now say uh I'm going to traverse over this list and for each a I'm going to apply f to it
But traverse wants uh wants an f of b in the end, right? So we need to pick some f to give it. So we're going to say well I'll just give you the identity. And at this point traverse has given us uh so it's an f of list of b where f is identity. So now I have an identity of a list of b I'm just going to get the list of v back out. All right. Cool. So we've implemented map in terms of traverse. So so that was cool
That means if we're able if our data type is able to define traverse, we sort of get map for free. I want to define now I want to define a more interesting function uh beyond map. Map is kind of uh boring. So I want to implement this function fold map. Uh and fold map looks like this. Uh a to b. So this looks a bit different. And I'm going to stub something out before I move on
Combine So fold map says given a list of A and a function from A to B where uh B has a monoid instance I'll return a B. And what a monoid is is just basically if you if B is a monoid you can it means if you have two B values you know how to combine them to get another B another B out and you're also able to summon some constant identity value of type B as well. So full map basically if the list is empty returns the corresponding empty value for the monoid and if it's not empty it'll apply the function to the first a and then it'll just just go along the list and just combine uh the bs as it goes along and full map uh full map type signature looks very different from traverses right traverse uh is return is taking an a to f of b and is returning an f of a list whereas fold map is just returning a plane b and at first glance it seems like you won't be able to we want to implement traverse uh implement fold map in terms to traverse. But at first glance, it doesn't seem like this is possible. Uh it turns out you can actually play some games with uh that ft-type constructor that traverse expects. Uh and without getting into too much detail, I'm just going to sort of give you guys the answer. Uh but it turns out to be pretty interesting. Uh we're going to use something called a uh the const data type
And a const data type is also uh sort of dumb like the identity data type. Uh the only difference is it has two type parameters instead of one. Uh and the the peculiarity is it only stores a value of the first type parameter. it completely. So the second type parameter exists at the type level, but it does nothing with it at the value level. Uh and this might seem kind of silly and useless until we see what we're going to do with it. So we can define an implicative for const. Uh that's sort of expected if we're going to call traverse with const
And u the implicative instance for const says I can define it if the first type parameter for const uh is a monoid. And what I'm going to do is just fix the first type parameter of con and leave the second one free because applicative expects uh applicative expects uh a unary type constructor and con has two type parameters. Uh this question mark syntax I'm using is from kind projector which is a compiler plugin. Uh so to implement this we need to be able to take given an a I need a constant x of a. Uh recall that const doesn't do anything with the second type parameter. Uh so really what we need is to conjure up an x uh an x value uh to to put into a const. And the only way we can do that is through the monoid interface. So we're going to go ahead and just go monoid x
Uh to tupil together two cons. Again uh we're ignoring the second type parameter, right? But we do have two x values uh underlying these const values. And we need to return a new uh a new x on the on a new x on the other side. And conveniently, Monoid gives us a way to do that where we just use monoid combine. Monoid x combine and uh map. We have an x value. We have this function that we're sort of just going to ignore because we don't have an actual a to apply to it. Uh so we're just going to get it and rewrap it
So the implementation is kind of weird. It seems uh kind of like we're we're forcing it into this applicative uh interface, but it actually ends up being really useful. Uh so if we go back to the code now, what I can say is uh I'm going to traverse over this list and for each a uh I'm going to apply uh f to it, but now I'm going to wrap it in this const data type. Right? So now f is fixed to what const is and that will give me uh so this was at this point it's going to be a const of a b of a list of b which means it really just stores a b value because we only store something of the first type parameter. We just want a b so I'm just going to go ahead and get it out and the compiler needs a little bit of help at this point. So I'm going to annotate the types. Cool. So we've implemented two methods
So these are two methods implemented in terms of traverse. Uh and we were able to implement these purely because traverse has this new parameter uh this type parameter that we're able to play with. Um and a really cool thing is you can implement u fold left and fold right in terms of fold map and from fold left and fold right you can implement all the various methods uh associated with lists literally all the methods and and in a lot of functional programming libraries like scholars that are catch you'll see that uh we have a type class that abstracts over things that you can traverse and that type class is a subclass of uh funk which are things that uh can be mapped over and also is a subclass of foldable which are things that can be fold mapped Which means that if you create a data type and it fits this traverse signature like um if you can implement traverse for it that means you get map and full map for free and by extension you get full left and full right for free and by extension you get uh if I can bring it up where's my mouse you can get all these cool methods for free right all in terms of traverse which I think is really cool uh So we because again this is all possible purely because we were able to talk about applicatives. We're able to pull out this generic traverse and uh we were only able to encode applicatives uh because of higher kind of types. Uh you guys are all probably sick of uh traverse by now because I've been sort of talking about it uh for the last I don't know uh 10 minutes 20 minutes it looks like. So I want to give one more example that's not traverse related. Uh I'm going to talk about uh DSLs. Um, and so I wrote I'm writing here
I'm writing sort of like a a very plain calculator kind of a very limited calculator DSL. And notice that this uh this calculator data type is also a higher kind of data type because it's abstracted over a type constructor. Uh, and we're able to write programs uh in this DSL by doing something uh like this. uh we just write a program that takes a type constructor f uh give me a calc of an f and I'm able to write some program that returns an f of double and uh after we write our programs in terms of this dsl obviously we want the dsl to eventually do something right so at this point we've just written some abstract program uh we now actually wanted to do the computation for one right that's a pretty uh basic need so we can write uh an interpreter for it let's say uh ID calculator and I can use uh the the identity function that we used in the previous slide or not slide but uh code snippet. So we need to be able to implement each method. So uh oh we need to be able to implement lit which is pretty straightforward. We need to be able to add two numbers together which in identity is easy and we need to be able to take the square root of things. Uh so I think that'll be math.s square root i.get.2 double
All right. And I can get my final double out by calling a program with this interpreter. And then that'll give me an identity of a double and I'll just get that double back out. Uh it turns out you can do another really cool thing uh and this is something that I've actually done at work. This is running in production at my company and I thought it was really neat which is I can take that exact same program and I can actually serialize it uh and dump it into disk uh without any changes. So I can write a serializer that extends calc. And here I'm going to use that const data type again. Right? So, so that con data type doesn't really ex it turns out it's sort of like a dumb data type, but it's actually turned out to be very useful
So, here I'm going to use const and I'm going to fix the first type parameter to be string. So, string will be what I serialize it to. You can choose JSON or or bite vector or whatever you want to serialize it into. And I'll leave the second type parameter free. And so, here is where things begin to get interesting. Uh so I know I I'm I'm just creating a literal integer here but really what all I need to return is uh a string to lift into constant right because we ignore the second type parameter and so what I can do is I can just call two string on the literal here what's happening let me finish writing this out is I need to be able to serialize uh this add operation given the serialized form of the left and the right uh and in the case a string I can do something like uh PN l.get plus r.get and then for square root I'll do something similar. I'm going to take I need to somehow serialize a square root operation knowing uh the the expression that I'm going that I have so far and I can do that with const and square root of i.get Get I think what does it want? Oh, double. And now I can take my serialized form and get a string from it by just passing program uh the serializer
And I need to get the value back out. Uh and just to sort of uh drive it home, I'm going to print these results out. So result equals result serialized. Oh, serialized right? So, we got the result and we have the actual string form. Uh, and it's all with the same program. So, so in in in code that I've written at work, uh we have a DSL written in this style and we allow users to uh write DSLs here uh in directly in the source code but also using taking that exact same program without any changes just also serialize it and dump it to disk. Uh which is really cool I think and again uh this is all possible because uh our DSL is parameterized over this type constructor. So so calcier is a higher kind of type and it gives us a way to sort of plug in a different kind of behavior we want
Uh yeah. So everything I've showed you I thought I think uh has been pretty straightforward uh or pretty cool I think. But you might have noticed that like in certain situations I'm doing things like annotating the type here. Uh and so like in the in the simple example like with identity I didn't have to annotate the type. But uh if I remove the type here uh you'll see scholar C is not very happy with that. And I'm going to try to let me cool. Uh we get this uh error. Uh no type parameters for method program exist so that it can be applied to arguments uh serializer
I'm going to go back here and we did the same thing uh with this full map. Right? So I'm going to remove that. And we get the exact same error. No type parameters for method traverse exist. So that can be applied to const. And I'm going to do the same thing with the first example where we traverse with either. And I'm not going to show you the error, but the error is pretty much the same. Um, so there's some there's something going on here uh that I want to talk about uh which is in in in the simpler use cases, we're able to use higher kind of types and and just have everything be inferred and everything is nice, but it's sort of a pain to have to annotate types in the less trivial examples
And this is actually a bug uh or a ticket that's been filed with the scholar compiler for uh let's see four or five years maybe. Uh and so Miles talked about this at the keynote today and this is like a very infamous ticket uh known fondly as SI 2712. Uh and the problem here uh so here's a sort of simplified example of what's happening. uh we're defining a method that's uh expecting a type constructor uh that takes one type and produces another type and we're passing it a value that is of type uh that has two type parameters. So uh what the compiler is basically doing is saying well I expected a unary type constructor but you gave me a binary one uh one doesn't equal two so I'm going to fail. Um and you can also think of it as uh the choice is sort of ambiguous right especially in this case um if the compiler were to infer what you meant like which f you wanted to infer in this case uh it could have chosen a partial application of the type constructor like you can think of it as a partial application of cured functions. This is partial application of type constructors. It could have partially applied from the left or the right and it would have been uh at least in this case equally valid
So because it's ambiguous the compiler is going to you can think of it as a compiler saying I don't know what to do so I'm going to give up and a similar situation is happening with traverse. Uh traverse f is taking uh a unary type uh traverse is taking a unary type constructor f. Uh if we try to traverse it with an either which takes two type uh two type parameters one doesn't equal two. The compiler fails and so unless we explicitly annotate the types the compiler doesn't know what to do. Uh it turns out in this case due to the way we've defined the applicative instance uh for either uh the choices uh should be unambiguous right only the first one should really work uh if you substitute the second the second one in I don't believe it actually type checks. Uh so in this case it's sort of unfortunate in that there's only really one choice but uh just due to the way the compiler works uh you sort of need to explicitly tell it this is the partial application I meant and it's not able to infer. Um and so the big difference here uh because we we had this parallel in the beginning between values and functions and uh proper types and type constructors and this doesn't really manifest uh at the value level because for one we always explicitly uh tell it how we want to apply to functions right it's never the case right now where the the the compiler is able to infer programs for us uh not yet anyways uh and uh another thing is uh we we have this different view of functions that we don't uh usually see view type constructors. So uh in Scola and in languages like Haskell and even the foundation of the lambda calculus uh we don't really have you can view as we don't really have functions that take multiple arguments
What we really have are uh uh curried functions that and you can view functions that take multiple arguments as syntactic sugar on top of curried functions. Um so all function you can think of all functions as taking a single argument and you emulate functions that take multiple arguments by uh treating them as functions that take one argument and return a function uh as a result that contains like uh the next parameters you need and this is sort of how it's encoded in lambda calculus and this is how languages like Haskell and I think Okam will work. Uh but when we go into the type constructor gland uh we have these like binary type constructors or type constructors of three arguments but we don't view them as uh type constructors that take one take one type and potentially produce another type constructor as a result uh at least not in the surface syntax. But we can uh in our minds sort of pretend that that's the way it works. And so if we review type constructors as type level functions that uh that can be curried then the choice for how we disambiguate uh the earlier examples becomes clear right we clearly always apply left to right just like we do with functions uh and this is how sort of hasll does things in terms of resolving like the applicative instance for either so going back to traverse example uh you could imagine that traverse is instantiated with these types right I'm saying either is going to be a type constructor that takes a type and produces a unary type constructor as a result. So the compiler should infer a traverse of either string uh which will give it another type constructor. Uh and then the the the remaining type types are int and double and that resolves to that basically specializes traverse into uh list of int into either string double and then either string list of b uh or I guess list of double which that should be uh and turns out this is exactly what's happened in a recent fix that my put together uh earlier this year. So, uh, this was filed, let's see, April of this year
And this was met with, uh, a lot of thumbs up and smiley faces and and celebration. Uh, this has been merged in Scola 212, which came out, I believe, two or 3 weeks ago. Uh, it's in the process of being backported to 219. And if you want to play with it now in 211, you can go to the typele scalleta compiler uh, and play with it. Uh, you have to enable - y partialification compiler flag to get it. Uh but yeah, basically what the what the fix does is exactly what I've described is it assumes that you want to the compiler is going to when it meets a situation like expected unary type constructor and got a binary one, it's going to try to partially apply it left to right. Uh and it turns out that heristic uh solves like 90% of the cases that that people care about. Uh it's important to emphasize that left to right is sort of a design choice
Uh it just tends to be like the convention that people have adopted that we want to apply left to right. So the fact that uh the oblictive and mode instance for either is right biased uh is is influenced by this. So if instead like we decided to say infer right to left then in order to make things play nicely I believe we would have had to made a made either left biased instead. Uh but left to right is is what people tend to do and that's the heristic we've applied. So just to sort of drive this home what I'm going to do is I'm going to go to my build. So I'm running 212 here. I'm going to enable Y partial unification. Reload SPT uh and compile
And everything works now. So uh I think that's really cool. This has solved many problems that many people have experienced. Uh and that's all I had for you guys today. uh when the slides get put up, these will actually presumably link to useful things. Uh that first one uh is a paper by Adrian I think that introduced uh higher kind of types to scholar. So thank you Adrian. Uh and other links are sort of learning more about uh why higher kind of types are useful
That second one is a blog post by Steven Comple on the type level blog and the latter three are sort of the tickets and the pull request and the explanation. Uh, that's all I had for you guys today. Thank you very much.