Keynote: Typelevel in 2016

scala.bythebay.io: Miles Sabin, Keynote: Typelevel in 2016

Recording: scala.bythebay.io: Miles Sabin, Keynote: Typelevel in 2016

I you well good morning everybody and thank you very much Alexei for that great introduction and also thank you to Alexei and all the organizers and and all the people here at Twitter for arranging such a fantastic event glad to see everyone has actually managed to get into the building out as well which is good so I just want to be I just wanna make a very very small disclaimer I mean Alexi was was I think kind of over complimentary to me when he saw suggest that you know type level is my my thing something I created that's absolutely not true it's it's it's created by the people who the people who make it up the ice opposed the it's fair to say that the the it's fair to say that that I was one of the cofounders of time devil and along with Lars la sao paulo and Jericho steinberg but it's it's it's definitely more than just us and it's definitely led by by the by the community and okay so what is tight that what kind of a quick show of hands who who has heard of time ever or uses a tight level project okay that seems like pretty much at least three quarters i would say which is fantastic who in the room has actually contributed to a higher level project that's fewer but that's still quite a few people and I kind of like to encourage more people to get involved in contributing to type level projects or orangie bringing their projects to type level if they can if that's something i can i can i can get out of this this talk about be actually great okay so what is type level so on the one hand if you go to type level to org you will see a a great big list of projects which which fall under the umbrella is is a sort of a catch-all late for for this collection projects and i think for a long time people people really just thought that it really was just that and but but we have we have I guess we have a number of we have we have strong opinions about really two kinds of things and one of them is about if you like technical opinions about how how functional programming scholars should be done and also some sort of non-technical opinions about how we think it's important to kind of reach out to people who aren't necessarily immediately attracted to the kind of things that we do how we make our stuff accessible and so on and so forth and I think we've between us and I I think it's the consensus among the people are involved in the projects who are part of tide level bit that both both both the technical and the non-technical aspects of time level are important things that we really need to try and try and promote so we have kind of kind of a kind of a mission statement I suppose it's a it's a community of projects a community of people organized around pure type for Punk functional programming in scarlet by Mitch by which we mean multiple things and one of them is obviously we're doing functional programming we are interested in controlling our FX and and we are interested in tights so one of the things which is a characteristic of most of the most of type level projects is that they're not merely interested in referential transparency but they're interested in making use of exploiting the advanced features of scholars type system which make it distinctive this programming language and the final bit in schuyler is actually important it's certainly true that many of the projects under the title of land briella have been inspired by projects which originated in other programming language communities it's it's it's it's fair to say that a lot of influences have come from from from a haskell community and also in places from from the dependently tight functioning communities around languages like actor and a dress you know in larger or smaller ways and but ultimately we are doing we're writing code in Scala we need to be able to bring these things back into code which is idiomatic for Scala which isn't just some sort of rather elaborate sort of transliteration of say a fairly complex piece of haskell into a piece of completely impenetrable Scala we want we want stuff to be idiotic and comprehensible and readable as as scarlet coat and independent free libra and open source software and type level is a bottom-up organization it's not it's not as I said at the outset it's not it's not it's not coming from me or Lars or Eric it is it is it is an association of separate independent open source projects almost all of which are our open source mostly BSD style rather than copyleft licenses but but clearly open source and it and in no case is controlled by I mean there are community projects then alters they're not control or operated by any commercial entity and we think this is kind of important I think I think it's important that we have both those kinds of projects and also that we have an organization which is able to help represent them we're also very keen to share ideas and code and what does this mean concretely it means that that that the many projects provide many opportunities for collaborations and I think that's something we've seen quite loss of and speaking from my for my own my own project shapeless one of the things that we've seen a lot which is giving me huge amounts of pleasures to see how many people have been building things on top of shapeless and this is not a phenomena which is unique unique to that there are many projects within the time devil site the tide level stable which which seat to collaborate with each other and build on each other's stuff rather than reinventing wheels and this is difficult I mean we know that there are problems in scarlet when it comes to to having having dependencies on other projects we know that there is a an improving but still awkward story about binary compatibility which which can make life difficult but I think one of the things that we want we sent you want is to try and face those those issues head-on and try and do something about them and accessible and idiomatic learning resources also a key thing is one thing to have fantastic fantastic ideas fantastic software very sophisticated things going on in your project not so great if it's completely impenetrable to an outsider so one of the things we've made a point off is to I I wouldn't say we've necessarily always succeeded or have yet got to a point that we're happy with but we are certainly trying very very hard to to produce documentation and learning resources for the type novel projects which which will provide people with her with her with a hopefully a relatively shallow on-ramp into into this style of style of programming in Scala and we've got a bunch of tools which have hugely hugely improved the the ability our ability to do that things like Rob Norris's tarts for instance which provides us with a mechanism for providing type checked plan checks documentation which is which which is a great boon for lots and lots of purposes and and finally but by no means least we want to have an environment that people feel comfortable in where they feel welcomed which is friendly and where people can are not expected to know everything up front where people can can learn and explore other people are helped in helped in the right direction and so that's and that's what type of Liz okay and um Eric awesome did a fantastic toolkit scholar world a couple years ago and his kind of summary of basically what what all of these things all down to is is we are trying to remove the barriers to functional programming and Scott I think I think that's if you think about it in those terms I think I think that's that that's our goal and we want to do as much as we can to kind of promote that okay so you can find some more resources here time devil dog is if you like top level entry point as an organization we basically do everything in the open we aim to reach any kind of decisions that we make by consensus consensus involves basically opening tickets on github commenting on those things and kind of iterating on that kind of stuff until we reach some kind of some kind of visible agreement we have a gated channel it's fair to say the most of the type level projects exists that exist on github and have by and large adopted get ur as a communication channel which seems to work very well so that's we can go for more so let's so we have as i said its community of projects which projects well there is now an extraordinarily large number of projects I was quite surprised actually when I came to put this slide together just see how exactly how many there are on the banner that's 50 which is quite as I was asking a few people earlier on how how many projects they reckon we're under under under under under the umbrella and came up with 20 was the most most ambitious guess now a few of these are sort of incubator project some of them a relatively recent arrivals but i would guess that probably everybody in this room nearly and uses at least one of these projects which is kind of interesting so clearly there are lots of people who are interested in what we're doing and want to be associated with whilst we have and we would encourage as many more of you with your projects to become involved as well and type level scholar is something which didn't appear on that list it's something which I want to come back to a bit later on in the talk so as well as being a community project is also a community project and people up until the beginning of this year type level had existed exclusively exclusively as a like an online umbrella thing with a few communications channels we decided at the end of 2015 that we really needed to try and arrange for some some meetups and coverages legacy mentioned the type level summit in Philadelphia and this is what we've done so we've we've now held too if you like headline type level events and the first was the Philadelphia stomach which was in association with any scholar this year that's a fantastic event those are the round tables that that Alexi was mentioning and there are a couple of laptops i think i can see that despite what he said it did work very well as as a as a model and that was great observance a day of day of invited talks and a day of unconference we had a subsequent sonnet in in oslo associated with flat map the reason we picked these two conferences to to sort of piggyback on is that is that many of the type levels if you like pivotal moments have happens at those conferences out the year so for example when Lars announced the sort of creation of time level had think three four years ago I suppose that was done that was done at any scholar and various other kinds of conversations around typify have happened by the any scholar and flat map when when when the various organizers of the Constituent projects have met up at those so it seems very appropriate to have events there more recently we've been having a series of monthly hat days in London hack tau is a fantastic event which is organized by Salesforce they've got an amazing amazing building and they basically give open source community groups the free run of their entire offices at on for a Saturday a month with incredible views as you can see from the window there and we've been doing this now I think for six the last six months in doing this and it's a mixture of mixture of stuff and some scarlet compiler hacking some working on tight little projects and some introductory stuff it's been it's been a great it's been a great it's been a great experience kind of organizing now and again it's something which very much like to encourage other people to do elsewhere and and also you know anyone anyone who's visiting London around mid month is very welcome to come and join us at those sessions we've had a bunch of sponsors who've been very helpful we're helping this stuff happen and and beyond the the sort of a high high profile things we've had a bunch of again recently out a bunch of on conferences and hack days in various places Scarlett Wells grr i 0 lambda world and are coming we'll have a hack that scholar exchange in london at the next month and we're also planning next year's any scholar and flat map companion events as well and again we will all please please do if you if you were inspired by any visitor to organize some kind of local type level events then please do get in touch this we would love to we would love to arrange that kind of thing ok so that's what type level is I mentioned earlier on tight level scholar that's the thing that I I personally been working on I think most over the last six months or so so type level Scala is its fork of the Scylla compiler but that was kicked off the end of 2014 and the aim was to address some issues in the scrum compiler of particular concern to people working on tight level projects and so in particular that's say the cat's project or shapeless throw there a number of long standing open issues against the Scala compiler which really really getting away and which which we'd hoped to be able to focus you know we're that we're the people who are most directly concerned by these issues so we wanted to be able to put some effort into trying to solve these problems for ourselves it was stalled at beginning of 2015 the reason as some people may remember there's some drama around scholars Ed's involvement in tight level this led to the the the beginning of the cat's project at that time and what that actually meant is that basically absolutely everybody who had previously committed spent time working on type level Scarlett was was involved in working on cats and that continued really and for the whole of 2015 and the underlying issues though that that we were hoping to dress like the old scholar that hadn't really gone away I mean they're still looking at background and but we found a number of other routes sort of less ambitious ways of trying to to deal with those problems and some of them were addressed using Scala compiler plugins so things for example like light projector addresses some of the some some of some of the awkward syntactic issues around using hi Kylie types in Scala and maybe using macros so for example things like simulacrum to ease the pain of defining type classes and instances and various other things so we sort filled in some of the gaps using using using plugins at macros and so on and so forth and but there was still lots of issues so I I kind of made I kind of stuck my neck out at the beginning of this year and and decided that I was going to see if I could come up with some kind of fix for I saw to someone to quick show of hands who knows what s I to someone to is ok so that's about half the people in the room ok that's not surprising really and I'll explain what it is they liked it suffice to say it's a big one if you are interested in in in in the kinds of size of functional program that you find in cats and scholar said you will be intimately aware even if not by number you will be intimately aware with with with the problems that it causes in some way or another and so I was going to be doing a talk at flat map on yet another kind of work around for SI 2712 that that I had come up with in the context of working on a project called Kings which is my attempt to use shapeless type class derivation to derive type class instances for cats this is king philippe shins to all of this so one of the things that so I / / / 2015 I've been a lot doing lots not to work on on type class derivation but mostly for type classes like codecs for example which our index by by fully applied type so you know types like a string or a case class or something like that but something without type parameters and the type classes in in cats are not entirely but but are predominantly issue index by by by higher kinda types types with type parameters so instead of funk tough so instead of you know a codec of string you have a function of list where list is an unapplied type constructor and it's these kinds of things which which almost immediately need you to run straight into SI 2712 so I run into it when working on kittens and had come up with yet another workaround for dealing with dealing with the problem in that context and I was going to be doing a talk of flat map on this new work around for it but I thought that you know in the context of doing that talk I probably ought some kind of review of where we got to in our thinking about site level Scala and where we going to be able to kind of address this time problem or more so I thought you know idly maybe I can have a stab at seeing if I can I can come up with a solution to it and I thought I'd give myself a weekend to have a go at it and it turned out to be an awful lot easier than than I had actually expected and fairly rapidly I got to an initial proof of concept that actually fixed bug then with a lot of assistance from the Scala compiler team of my bed various other people and got to the point where we actually had a full-blown fix for problem and it turned into a pull request against the Scala compiler and and then was merged and this led to a certain amount of reflection really it turned out that a long-standing problem I mean if we see if we can find a ticket [Music] where are we one oops yeah here we go so here's the ticket and you can see was created november two thousand nine you can see um actually the number of watches has gone down i would guess that's because although 83 votes for the issue now which may not seem like a huge number but but bear in mind that the average number of votes on any issue is basically just above one where one is the minimum that you get because if you if you if you I think of you if you learn add the ticket you automatically get to vote for it and so so that and it's also a long-standing baby it's too similar to it is a four digit issue number it's not one of the three digit sort of northern tickets but it's only been around for a long time and a lot of people of Canada bath you very much so we had this kind of situation where something which had seemed to be intractable impossible to fix already stiff not impossible then you know why why why why why hadn't it been fixed him he's been around this long and causing so many people so much pain you'd think that somehow or other we would have we would have we would have found our way to a solution [Music] and so this led to a little bit of reflection and I had this this exchange with Bruenor bouncing on the shakers gated channel the thing is it that the solution was kind of in staring us in the face all the long way and the actual the actual solution that I thought I implemented in my fix was was actually proposed by porches are know in a comment on the ticket itself you know it was see it was there all along it's really just adopting the solution to this problem that you find in Haskell and and I think lots of this kind of looking at this group yeah it seems like we've got that idea so much try but but but just nobody did and so so I kind of conclusion that really there is you know the only thing that's hindering us here is is that is that we aren't actually just rolling up our sleeves and digging into the staff so um I I kind of having having if you like achieved my my 2016 new year's resolution decided to add some stretch goals and this these were the these are the things I kind of announced that Scala days Berlin but I thought it with things that we really ought to look at we had a bunch of stuff which is has been hanging around for ages so this is something which was originally worked on in the in the in the first iteration of the type level skyla fork so these are the literal types something actually being able to use say literal values is in type of positions which that can be very useful a number of contacts and so this was this was worked on who's worked on an original by Georgie and teeth actually most did some more work on and then it kind of got part because it just wasn't enough there wasn't enough impetus behind it so that bag or left as a git branch gathering gathering dust so I seem like it pick this up continue it to try and get it over the finishing line and that's that's that's that was one of the things and there another a number of a number of a number of issues which in one way or another cause annoying roblox annoying Road books people trying to use 22i bevel projects one thing that people anyone anyone using checklist for example will know that that compile times can be absolutely horrendous for the particular style of kind of inductive recursive in places that are used in shapeless and I certainly wanted to see if I could try and make some progress on it so that was that the status if you like the DD the wish list at scala days berlin this year and since then we've made some progress on there and that's okay there it is so the the literal type stuff it is done there is now pull request for that against live in scarlet and there is some work on multiple in multiple interested parameter blocks which that that that does exist as a pull request against like pence Carla but we kind of decided in discussion that we could actually do something a little bit more ambitious than than than was originally a planned and something which would get along well with what dotty is is planning to do as well and and I have also been doing a lot of work recently on on improved compile times for induction vessels which hopefully I'll have time to give you a very short demo of and at the end of this and ok so so the next thing so we can do all this work on non-tidal scholar and so this is a fork of the Scarlet compiler it's all good but what difference does that make to us in our in our in our working lives can we actually use this can we put this stuff into production do we have to wait for light bends to to merge this stuff which you know who knows how long that might take maybe look very quick maybe it won't is that and so what what would make it possible for people to use a type of Islamic compiler and so thinking about this led to ask coming up with some set of constraints on what we were going to do in type of the scholar which we we hope will make the choice to use type level scholar in production systems kind of much much less risky than it might otherwise seem so for someone to be both able and willing to use type level scale up right now as in you could go back to work on Monday and start using it without risk of getting fired we need our releases to be completely compatible with the existing ecosystem we can't require you to kind of rebuild the entire world to be able to use stuff so it has to be the case that you can carry on using all your existing binary dependencies and so on fourth absolutely unchanged normal there's going to be a big win it's got to be a real benefit I mean there's no point so one of the first things I did were the first country whose contributions I made to the very first iteration of time Excalibur's the ability to have a little Prime at the end of an identifiable existing it's kind of cute if you're sort of doings of a little kind of expository bits of code where you to work your way through a series of definitions it's nice to be able to have a foo and a food prime and a food prime prime and that's great and that's the way this kind of stuff appears in that in a general of functional programming or something in Haskell and it's kind of cute but it's really not the kind of thing that matters enough that you would be motivated to switch your production builds away from unofficially sporty compiler something that is not quite so official so that kind of thing is is not good enough so on the other hand things like a psycho 712 or improved apart times those those those I think arguably are good enough that you could be persuaded to do that there must be minimal disruption and it's got to be possible for you to drop type level Scala into your existing bills without with the absolutely minimal changes required to your existing building frustration and and the risk should be low and I think I think I think like I said you don't want to you don't want to switch this over and then and then have some terrible disaster happening which in your way or in your production systems okay so how do we meet those constraints so we set a policy and the goals of the policy are that we track light bends calories so that means for every light Bend Scarlett releases there is there will be a corresponding type level scholar release the tide level Skylar release will generate code which is binary compatible with like been Starla and that means that type level Scarlett binaries can be linked with like been started by memories and vice versa so you can you can you can compile your top level project with type level Scala and you can use upstream light Bend Skylar compiled binary dependencies similarly if you are working on a library which is an upstream dependency of something else in many if not most cases you can compile with type level scholar and expect downstream projects of you which are built with the tight devil Scala compiler to be able to consume you artifacts without any problems and the reason this works is because most of the changes we envisage for type level scholar involve changes in same type inference or for example in the case of the inductive in plus its staff and they well now that is also that is also a kind of type inference problem but anyway there are things which don't have a incompatible effect on the resulting output pirates so it's safe to mix in both directions so here are the rules that we have to kind of like implement that policy so every pixel feature included in a tight little scholar release must be submitted as a pull request against like Ben Scala first so among other things this this is if you like a statement of our intent that we really do we don't but this is not a sort of a divergent this is this is a feel like a collaborative cooperative fork of the light bends Carla compiler we want it to be possible for every single thing that we do eventually to be merged back into the main tonight's Carla compiler and really the only way to guarantee that is to have a policy of this sort to say it's gotta be alike then scholar poor request first there's going to be reasonable chance that that that that core request is actually gonna be merged so for example it would not be you wouldn't satisfy the the first policy rule here by sympathy pull request which deletes the entire Scala compiler tree and replaces it with so the Idris implementation for instance that that would not be acceptable because I think I don't know is I doing here yeah I don't think he would I don't think you would do I don't need much thats a mess and it's got a lot of a significant pixel feature which doesn't have any kind of reasonable work around and obviously there is a lot of scope for discussion about exactly what counts as a reason reasonable work around or not but certainly the kinds of things that we've had to do to deal with this I 2712 I think I think we kind of by and large agree that those workarounds are just too clunky really they're too painful and it's got to be binary compatible with like thanks Carla unless of course an actual binary change is the point of one to the pull request in first place and there can be some circumstances where I'm true okay so what's the result we have our first releases of type level scholar so this is all happen quite quickly I mean so so so this is all kind of a pipe dream around discovered ice Berlin which is really not very long ago but we now have a and we have two releases of tight little scarlet available now the first is relevant to rep relative to light men's Scala to 11 n so the two of them know you can pilot that you're almost certainly all using yourself it includes the fixed SI 2712 occlusive fix for SI 7046 which is probably less familiar to people unless they work with shapers doing type class derivation on on algebraic data types in which case they they will know of it too even if not by number i'll give a demo of of that fix of it later on if I've got time includes the literal types stuff and some minor G ATT fixes we have also very release relative to scholar to 12-0 so like I said we are we are planning to aggressively track the Lightman scholar esis I think you know within a matter of days we hope to be able to get corresponding tide level scholar yourself this includes the fix for SI 7046 I just mentioned the literal type stuff and well and the fix for SI 2 7 12 and the JTTF exist they have already been merged so and this is this is this is kind of this is kind of the ideal outcome i think really to have stuff which is of immediate value to people working in their tight level kind of ecosystem being able to use type level scala take advantage of fixes in advance of those things being merged into type and scholar but but we do want these things to be most eventually so going forward so we're here we have a site ism 12 and the GOG fixes like that they've been merged into 12 the literal types and SI 7046 fix they're under consideration for 2 12 1 so all of those things have been backported four to 11 9 and it turns out that I was actually about surprised that Adrian method 2 d's five minutes geez okay mostly so quickly but basically these these these these are all now merge someone someone did actually say to me sort of asked me you know it's really strange question miles you must be really upset that you know like bender merging all your fixes this is terrible I mean there's nothing distinctive left about tide level scholar anymore which is kind of kind of missing a point really ER because we really really do want to stuff out okay so um it's it risky to use it I would actually argue that it's it's it's risky not to use it and if you are facing the problems that those those fixtures and new features solve you are better off using type level Scarlett than the clunky workarounds all the various kind of the Scala compiler plugins the workaround so for example is that I put together a plug-in version of the fixed SI 2712 if you are using that you would definitely be reducing your risk by using type level scholar and step because the the proper fix in the compiler itself is I would say more robust than the one that you'd find at the plug-in and how do you use it that's it so please go home and try this today I try this try this in the break try this with your project there are only a couple of constraints you must be using in your SBT build started to eliminate or to 12-0 and you need to be using SBT 0 13 13 or later and the reason the reason for that is that basically I had to do quite a lot of work internally to us BTW to make it quite as simple as that to do the switch over the scholar organization stuff as it for a while initially it was introduced support scala virtualized but because it really didn't have very many users it they'd had quite a few bugs in this features which which needed to be addressed before it could actually work so if you want full details on that if you go to github and then type level scala you'll find full documentation how to do that okay so how long do I have now Alexi how long a couple of minutes okay well I'm going to show you one one quick demo can you hear me here hello yeah okay so um actually I'm not sure that it's going to work and let's have a look IIT was that Mike what I do not like focus okay so um i'm going to show you this is so this is working progress i've been working on accelerating the compile time for inductive implus it's so this is the kind of thing that you see in shapeless if you're doing typecast derivation using shapes on the directory indirectly because you're using a library like s code a call sir c which is use shapeless for automatically generating codec instances for a DTS so the trick is for the people who've seen us or not seen this kind of thing we're trying to select well here's here's the example so this is this is an NH list type this is quite a big one so wait let's just let's see and see how far does it go right so we've got a boolean ln at the end so there's actually five hundred elements in a socialist now believe or not people do actually try and work with HSS that big people working on absolutely monstrous kind of Enterprise enterprise DB schemas of simple or another and and do actually seriously try and use shapers to do this kind of stuff and then send the emails complaining about how smoke is coming out back there build server and has been coming out of the back of their build server for the last week and is it ever going to stop so so it is it is it is it is quite a serious problem so basically what's going on with this so this is so the thing that we're trying to do here is we're trying to find the first element of that age list which is a boolean and we use a type class called selector to do this and it's defined inductively so basically there are two cases for selector one which is where the the type of the thing that we're looking for is actually the same type as the head of the ageless that we're looking at in which case we're done that's that's our induction base case and the other is if if it isn't in which case we look in the tail and so that that that's the mechanism so it's basically we recurse through the structure of the age list until we hit until we hit the base case and in terms of the way that this is implemented I mean this is this works beautifully in a way in Scala it implicit search will do some kind of very naive backtracking search for implicit instances to satisfy these equations and it gives us the right answer it's just that it will be unfortunately superlinear in terms of in terms of in terms of compile times do it so for small instances and I usually recommend it to people in you know if you if you if you're working with a chalice up to I don't know about 50 elements or something like that you can kind of get away with this if you don't mind a little bit of compile time like but certainly anything beyond that it makes like very very difficult indeed so one the thing about this is though that it is a very very simple pattern and it's actually quite easy to spot this pattern in the compiler when you're doing implicit search and if you do that then you can take advantage of the fact that is inductive and you can apply some heuristics and say okay that looks like I'm solving an induction rather than using the the naive backtracking search what we're going to do instead is sort of directly as an induction effectively unroll it immediately and it turns out this works remarkably well I'm going to show you a quick graph so the top line is this is this is this is to 12-0 and so that's for the 500 element h list instance that i just showed you to pick out the booty at the end of it compile-time is 450 seconds which i think i think you'll agree this is kind of its kind of not really feasible if we if we apply the the induction heuristic that reduces up to 30 seconds and and that's really actually without without trying very hard i mean this is this is kind of surprisingly low hanging fruit in a way I mean it'sit's is good that's my timer telling me I'm out of time I think I have probably a couple more ok so that's the result joy No okay well anyway so I guess I will summarize by saying there is a lot whatever whatever whatever people might tell you about the current state of the Scala compiler actually it's a fantastic piece of code but there is lots and lots of low-hanging fruit in in there things that people can work on is it so it's a project that people can is actually surprisingly accessible to work on and for things which are your particular interest but not necessarily general interest if you want the fixed absolutely i encourage you to dive in and try and do it the more people who do that the better it's not something we can just leave to the like benzene they just don't have been at halftime the resource to it so that's what I want people to do I want people to go away try out top-level scholar fork the Scylla compiler work on issues which are a particular interest to them and we will all then get up at a scholar compiler after that thank you very much you