Edwin Brady Tells Us What's New in Idris 2

welcome everyone to the final edition of the berlin functional programming groups summer series of online meetups we're not finished forever just for the summer i'm going on vacation but i will be back in september to do more of these but i think that we are finishing off the series with a real bang tonight i am i'm thrilled and honored i should say to to introduce edwin brady uh i can't believe he said yes he's obviously a very generous soul for doing this i know he's very busy and i know you all know who he is so he does not really need that much of an introduction he is the creator of the idris programming language and also idris two which he's going to tell us about tonight and at the moment he is a lecturer in computer science at the university of saint andrews where i think they invented golf pretty much not at the university somewhere nearby in my office in fact right right um uh so i'm really looking forward to this talk because it's just such a such a pleasure to have someone uh of your of your stature influence visit our tiny little berlin group and i think everyone is very excited to have you and i hope everyone has lots of interesting questions to ask so i'm going to ask the audience if you have a question type it into chat and i will find an opportune moment to interrupt edwin to let you ask your question and he has promised to try and create a few opportune moments and i think everything will go swimmingly so without uh anything further i am going to hand it over to you edwin and allow you to share your screen and take it away it's all yours hey so if i um where are we do that is that good do we have the whole screen yep looks good fantastic well uh thank you for that uh very kind introduction um i uh i'm very happy to be in virtual berlin i i'd much prefer to be in real berlin um one of my one of my favorite cities but uh alas soon i hope hopefully i'll uh i'll be able to come and visit you in person at some point in the not too distant future so um oh actually an important question i should have asked this earlier is how long have i got i'm pitching it by about an hour is that uh you have you have absolutely as long as you need oh but i've done this i've done these for two hours and three hours so don't feel obligated to go for a very long time but you have as much as required so well we'll see how it goes so um as uh as stephen said what i uh what i want to do is um introduce idris 2 so this is uh to show you the the new things that i've been doing in idris too but i'm not gonna i'm not gonna assume that that the audience is even really aware of what the old things are in idris one um so rather what i'm gonna do is tell you what idris is and illustrate it with several hundred examples so we'll we'll go until until i get hungry i suppose um so um idris is a functional programming language which is a good start for a functional programming group and i think that the thing i like to say about it that makes it kind of sets it apart from other languages you might know is this idea of first class types so when we when we talk about functional programming particularly pure functional programming i'm kind of guessing that there's going to be a significant number of uh haskell programmers in the audience for example so we talk about first class functions as in ability to assign functions to variables we turn functions from functions past functions to functions and so on so functions are just like anything else so an address the thing that's the thing additionally on top of that is we have first class types that is uh functions can return types you can pass types to functions you can even in address two um in inspect types at runtime which leads to all sorts of uh interesting possibilities so um so i'll illustrate all of those things and i'll give you an idea of um of what it means to programming it is what it means to do what i like to call type driven development um so i'll talk about what type driven development is i'll talk about um doing interactive programming so i think that where things get really interesting if you have um expressive types is programming becomes more of a conversation with the machine and this is if there is one overall um point to why i why i like working on makers and why i'm having so much fun with this is that it's turning programming more from you know you you don't write your um uh your hieroglyphics and send them to the oracle and then get a get a message back saying it went wrong you know see me after class rather you you you write part of the program you leave some holes in the program to fill in and you let the machine help you find your way towards the working program so it's kind of deliberately by analogy with test driven development so in test driven development the idea is you write the test first because you want to think about what you want that to help you design what the program is going to do how it's going to work and the tests are there to help you think about what the problem even is you're trying to solve similarly with type driven development the types are there to help you think about um what the problem is you're trying to solve and have a machine help you get there i suppose now's as good a point as any to say i want to be totally explicit about this up front there is absolutely no conflict between type driven development and test driven development um i do test driven development as well sometimes sometimes i i write this program and i write the test and then try to work towards getting that test working so there's no conflict there don't let anyone ever tell you that there is um types and tests work really nicely together so type driven development having having expressive ties for your program helps you maybe write fewer tests but you still have to write tests so the new thing in interest too and you may not know this if you haven't seen idris one but the the the most interesting new thing in idris two for me is the idea of quantitative types so quantitative types the idea here is that every variable every binder has um a quantity associated with it um and in my world there are three interesting numbers zero one and i don't care so zero is a variable that is not going to be used at runtime so something we can talk about at compile time but it's not going to be there at wrong time one is for variables that have to be used exactly once at runtime um so this leads to all sorts of interesting things and that's that's most of what i'm going to show you and then don't care that's basically back where you are in a regular everyday programming language so i'll show some examples of that i'll show you how xero gives you guaranteed erasure i'll show you how one gives you linearity and i'll show you how that helps you write nicer apis for some of the things that you just do every day when you're programming right that's enough slides for now um i'm going to move on to i mean this is what i like to do i just like to write programs at you so i'm going to write programs at you for the next you know five hours um right um so this uh is this visible is this good is my font size okay yep yep i can see it um i mean you should be seeing exactly what i'm seeing but um the problem we have here is that we're using computers so who knows yeah yeah no it's definitely big enough very good um i want to start with something so i sort of see i'm assuming that the audience knows a bit about functional programming but i'm not going to assume you know anything about we're talking about first class types so i'm going to start with something that you've almost certainly seen before in some form and that is i've got a little function here that takes a pair of integers which is imagine a point in a coordinate space and another pair of integers which is the amount we're going to move it by and all it does is move that point along so if you're writing something like this let's say you're doing it in haskell um what you'd probably do is say well that that pair events that's actually that's a point we'd like to encapsulate that somehow we'd like to at least not have to write in comma into every time so what you do in haskell is you write a type synonym so when you write a type synonym that's you are you're really doing type level programming but in my world um so what i like to call type level programming is uh is programming so so in my world i would rather than write a type synonym i would write a type level function i'm going to call it points which returns type and point just a paragraph so we've we've already seen first class types in action here in the to write that um to write that function i've said i'm going to compute a type i'm going to call it point and everything everywhere i have incompetent i'm going to i'm going to call that point so that's the type synonyms by type level programming by writing a function that returns a type um so far so good hopefully not very controversial so another thing i should say i might notice what i did there this is i'm doing this in um in vim so just because i'm just i want to alienate half the audience who use emacs sorry about that um but also because it's my favorite editor at the minute um but vim has a way of talking to an idiot's process or there is that there is a mode that allows us to talk through this process you can do the same thing in emacs you can do it in atom believe this visual studio mode in development um so the point about um interactive editing is you want to be close to the compilers the whole time so you want to be able to ask the question ask questions of the compiler the whole time compilers know a lot of type checkers know a lot of stuff about your program we don't want them to keep that knowledge to themselves in particular i want to be able to regularly check that what i've got is is working so if i hit that comma r here it will it will reload the program and check that it's okay okay so the basic idea of functions can return types we'll see a bit more of that as we go as i want you to see that that's possible so another thing that we're going to do quite a bit of is interactive programming so um i've got a the type of a function here that's going to repeat some elements a number of times so so nat is uh the type of natural numbers so unary natural numbers uh zero or successor um and this tie the fact that this begins with a lowercase t so the the rule for types and addresses is that uh if you have a name that begins with a lowercase letter in your type that is a type variable and it will abstract over it so this is this is kind of for syntactic familiarity with uh with haskell so i i was a haskell programmer before uh before idris and so kind of like some bits of a haskell syntax so it's a little bit mostly familiar to our school programmers right so we've got a type we start with the type you'll notice that it type checks even though i haven't given a definition so we have a we have a whole for this program that repeats a number of elements and the way we can implement it is we can say to the machine give me a candidate definition or skeleton definition for that function um and there you go it'll it'll talk to idris in the background and um it'll give us that uh candidate definition um and this thing here this rep rhs the query wrap rhs this is a whole our job is now to fill in so if i if i ask the machine type of the health i can hit um backslash t does this work if i yeah show type in the menu there and it will show me the type of that hole and it will say you've got tie that's the type we've got x of type tie we've got k is a nat and we've also got this mysterious zero next to tie and what that zero means is that we are had to talk about that type so that is that is a thing that's in scope tie is a variable that's in scope but we're not allowed to use it in any position that's going to be used at runtime so this is the first instance where we've seen a quantity um okay so in order to um in order to write that program well what happens if um what happens if there's zero of these and what happens if there's a successor so that you'd see a bit of syntactic sugar here send the z into an actual zero um so for zero of these we'll return the empty list i'll just fill this out um um i just do that to show you this isn't a video and things are actually happening um so again hopefully something that uh if you've done a bit of functional programming before you'll have seen this kind of thing but the point is we're doing it interactively we're only doing it step by step step by step and checking that things are okay as we go so i could leave this hole here and it would still type check and i could check the type i just have a question about the two different um syntaxes for the lists just because it's a little bit different from haskell you have a type level version and is it like a value level version or how does that it's always the same so um oh right i see what you mean so um so in haskell this would be written as um something like that so it's a list of type and uh i really dislike that by the way i i i teach haskell to our undergraduates and a significant amount of time is explaining to them that these these two syntaxes are not identical one of them is a type level list one of them is a is what one of them is the type of lists one of them is the value of lists and these are different things so the type of list is called list and the value is you know we can write the square brackets that syntax for it or we can write um uh the the um we can write it in the form of a x cons so yeah i i personally i think that was a mistake uh in in our school i don't know i don't know whether people agree or this i don't really care whether people agree or disagree um but i've decided not to do that in idris yeah that's what it looked like i just wanted to clarify also the usage of colons is blowing my mind ah yeah so um i heard that the reason haskell uses double colon for so in in haskell this would as long as you define the the type synonyms the other way around now i i'm told that the reason haskell does it with a double colon for types and a single colon for list it's come from miranda so one of the precursors to haskell and the creator of miranda david turner who incidentally was uh was a professor at st andrews um some years ago he thought that he would be writing more lists than types so he wanted the shorter syntax for lists and haskell inherited that so idris uses a single column for types and a double colon for lists for exactly the same reason that is we're going to write more types than lists well i think the single colon is the uh original gangster of uh type definitions anyway absolutely the exception here you you've brought us back to basics that's the way it should be okay so that's uh that that's how you interact with idris anyway so um you'll see here i have several hundred buffers to get through well i'm not gonna get through all these but we'll see how it goes now here's um more interesting use of quantities so we're going to be using quantities quite a bit here so this this function um duplicate so we're going to take this x and all we're going to do is duplicate that x so you know i can write it i can write it by saying i'll duplicate the x great um but what happens if i could say that i don't actually want to duplicate that x i could say that i want to use x exactly once so just spoiler this isn't going to work but let's try let's see what happens so if i check the type of this uh this whole rhs says right we've got time we're not allowed to use that at all and we've got x and we have to use x exactly once so i could write a partial program so i could return a pair of x and something and well now i've spent my x i can still talk about this but there's none of them left to use so i could blunder on and try using it see what happens and the machine says uh nope there's two uses of linear name x and uh and that's an error um just because people sometimes ask sometimes people ask what happens if you put the hole before x and i think imagining the type checking works left to right i think that you know is is x usable here well um so we still spent x but we've spent it a bit later on so we have to use x exactly once we're not allowed to use it more than that we're not allowed to use it less than that so the um the intuition for how quantities work i know you've written this already but if you have something if you have a type of this form so if we have some function type of one x of type a goes to b then that means if you have f of some expression e that means if fv is used exactly once then e is used so it doesn't mean that we're only allowed to pass things with only one use to that function so it might be that we have some either is some arbitrary expression that's duplicated and used all over the place that's totally fine the only guarantee that that gives us so if we have something we have an argument with with a linear a function with a linear argument the guarantee that gives us is this function will use it exactly once meaning that if the function is called with if if the function itself is used exactly once then its argument is used exactly what so when you talk of when people talk of linear types there's all sorts of things they could mean by that and you have to look at the exact details of the the system you're working with in order to know which one so the guarantee linearity gives us is the one gives us here is the thing will not be duplicated in the future it doesn't give us any guarantee that the thing hasn't been shared in the past so we might have something some some shared type passed in and it won't be shared anymore but it will be exactly once we have a question about that yeah so torsten wants to know what does use x exactly k times mean what constitutes a use and what doesn't by contrast what does we can still talk about x mean that's that's a great question and um i'm trying i'm just pulling because i'm trying to decide whether to enter it now or to uh just to wait till it comes up later let's give a quick answer now so if you do a case split on something um so if you if you deconstruct something that counts as consuming it that counts as use of it if you pass it to a function that uses it that is if you pass a variable to an argument where that argument has quantity one or don't care that counts as a use if you pass it to an argument that has quantity zero that doesn't count as a use so um we sometimes call them multiplicities because it's it's kind of like uh you're multiplying the usage so if you if you have in fact this is how it's implemented so if you have an argument with an argument with unrestricted multiplicity and you pass a value with one use well what's one times unrestricted one times unrestricted equals unrestricted that means we're not allowed to do that so we're not planning to pass a something of one use to an unrestricted argument i think it becomes clearer though uh just by working through a lot of examples so so this will come up in a couple more cases and um we'll see that um hopefully that'll explain this and maybe i'll check later on whether it has um you do also see some other functions on this screen that i've left as a bit of a teaser i'm actually going to skip them for the moment if anyone's interested in what's going on we can come back to it a bit later on i just don't want to i don't want to miss the really good stuff for the sake of laboring the the kind of core theory stuff so um one thing that i'm particularly enjoying with uh idris too and it just won't have this to some extent but it's the idea of interactive editing and giving precise types to things means that the machine should be able to help you with finding implementations of things so as an example we've got this function on curry that's so uncurry is a function that takes a curry function and turns it into a function that takes a pair of arguments so um got a function from a to b to c we'll turn it into a function from a pair of a and b to c and we can write that by hand we can look at the check the type of uncurry rhs and we see that somehow we have to deconstruct x and pass it to f so we're going to take the first element of x and the second element and we pass them to f so one thing we can do in idris is say i don't want to have to think about how to do that let's let the machine do it so i've got a command in dim here um backslash o for obvious and it will it will essentially it'll just search it'll it'll search through the environment um it knows about pairs so it knows whether to deconstruct things and it finds us the implementation um but it's more fun to do that just right from the beginning so i have one button pressed that leads you to the whole thing so um fans of fans of parametricity will will realize that there is there's only there's only really one implementation of this function i guess there's a couple because you could you could pan match on uh av but there's only gonna be one thing that this function does so we can ask the machine to generate a definition from the type and essentially it's doing the two steps that i just did so skeleton definition search uh if it doesn't find something it will it will carry on um what's kind of i just hacked this off yesterday and i'm having enormous fun with it um if you're not satisfied with the first thing it gives you you can ask it to keep looking so i said there's another possible implementation of this we could patent match on on x and then feed the the results uh feed the the components to f so so i can say to the machine let's keep going and we'll keep going until you either run out of definitions or we find a definition that i'm satisfied with basket again it's run out so no search results for no more results okay so we'll generate these things so curry works as well um select things this is just a kind of function that pulls things out of the path kind of contrived thing but see that it's able to lock inside pairs it's able to to compose looking inside pairs and then um append this this is entertaining what uh what do we reckon this is gonna do um if i search for an implementation of append on lists um well that's probably not what we wanted uh it's definitely type correct but it's probably not the implementation we were thinking of and again we can just say to the machine i'm not satisfied let's try another one nope no no no no well almost that'll do so we got there in the end um so there's something about this definitely like we that that's that's a bit more what i imagine i'm hitting it with a hammer until i eventually satisfies me um but there's there's something about this definition that uh we kind of maybe knew in advance that we didn't explain to the machine which is that we know when we're appending two lists we want everything from the first list and everything from the second list to appear in the result so we can we can cut down that search space by saying you have to use that list first list exactly once you have to use the second list exactly once then generate the definition and there you go you get the one that you'd you totally get entertaining you can keep looking see what it see what it comes up with if uh if you keep looking but uh um yeah it's getting a bit silly now um but it um the the the point here is that by giving that additional bit of information we've hugely cut down the search space of possible programs and uh and we've made we've by giving a little bit more information to the machine the machine is able to help us a lot more there is by the way this is this whole field of um type driven program synthesis it's a fascinating one it's a massive field and i'm not really doing it justice here with with what's implemented in idris so um it's um it's kind of a magic trick it's it's just sort of conjuring it's it's um if you know the secret you just think ah anybody can do that so all you do is look for the the type you're looking for if it's a function type add an argument um if it's a list well we've got nil and cons so we'll try nil and cons um we also know we're defining append so we'll try a pen so we'll build the program bit by bit if we ever hit anything if we ever hit any kind of incremental step where it doesn't type check we just rule out that entire corner of the tree and we just keep going that's literally what idris does it just keeps going and um until it finds something complete the type checks okay uh any questions on that i don't see any questions in the chat right now okay but if someone is very quick up well we do have a question uh frederick wants me to read the question no mike does lowercase type do lowercase type variables automatically quantify over type uh no it's uh it's over whatever um it quantifies over whatever would make sense in that context so they've all been typed so far i haven't really shown you any dependent types so far um but we're about to see we're about to see a case where i quantify them something a lot more interesting um there's a question about other operations on lists um andreas do you want to unmute i'm not sure what you're getting at hello andreas here i am sorry yes the question is um if we have a list why it should look for append so it doesn't know about a pen you could take from two lists you could do a lot of things you could split them select several elements from these those two lists so i think appending to this is just one possibility from several thousand right the only reason it even looks is that it's because it's defining append so so it looks for recursion that's that is all so um that's part of the reason why this is really it's it as as it stands it's a bit of a it's a bit of a magic trick um and there is scope for giving it more hints so so you can you can give it hints you can say when you do your search search for this particular function so it only knows about things if you tell it about things and if it happens to be the function that it's currently defining and if it is defining a recursive function then it will try to discover the bug in this earlier but it will try to make sure that the function it's uh generating is at least a recursive call on a different argument so it's not going to just define f of x equals f of x yeah i mean we have we have one other question um from alex what are those underscores up to oh it just means i don't care about the name um what some somehow what we'd like to do is be able to write something like this um and the only reason we can't be oh i don't know i guess we could uh linear logic fans might like something like this um so the only reason we don't do this syntax for example with one list is that that's actually one list a is actually a completely valid uh expression that pauses and um because types of first class and functions oh that literals are turned into values using a from integer function so you can overload literals and it's not out of the question that you might actually mean to do something like this because you might you might define one to be a a church numeral which is you're applying a function once so this just doesn't work syntactically so um much as we'd like to so um so the underscores are just a sim a shorthand for um the syntax requires me to give it a name but i don't want to give it a name um so there is one question that the um sort of preempt which is that you know i uh i just said this is a magic trick i'm kind of i'm cheating by by using things that i happen to know work so when does this when does this sort of thing become useful in practice and um without worrying too much about what all this stuff means um this this might be one way of defining a heterogeneous list in a type safe way so defining a list where every element of the list has a potentially different type so we have a list that says what the types of the element of the list are if we define a function that explains what type and element of the list is we've kind of already defined a lookup function by explaining what the type of each element is so i shouldn't have to i shouldn't have to write it again so so that basically where this is useful in practice it is uh most often for me anyway is that if i've gone to the trouble of defining an expressive type that explains the relationship between two things i shouldn't also have to write the program to find that relationship so just as a small example of in practice okay so that's uh quantities that's search that's how quantities help search we haven't actually seen any dependent types yet though and and i've got a little example of of dependent types that i quite like as an introductory one because hopefully everyone understands uh the problem and it's it's a little bit more realistic than some of the ones we sometimes use so um so you might have seen uh run length compressions a run length encoding of some data so this is if you have some data where there's there's lots of values in a run so you've got like 10 x's in a row then then that would just be 10x rather than x x x x and so on so one thing that dependent types i find really useful for is if you have two pieces of data that are maybe represented in a different way but they mean the same thing and you want to say to the machine these two things are the same i'm probably going to get it wrong keep me right so tell me when i've i've messed up the distinction between these two things so a run length encoded um a bit of data so what we're defining uh the type of run length and code of data and it is parameterized by a list of some element types so we've declared here a dependent type so this this rle depends on some list so it's it's um it's predicated on some lists so rle of x's is the run length encoding of the specific list x's so empty you can read these in a sort of prologue programming style leave these kind of predicates on the list so um mt says that um empty brackets is the run length encoding of an empty list and the second argument run takes some number and some value and if i have some run length encoded rest of the list and then i have n repeated x's then that is a potential run length encoding of n repeated x's plus more stuff uh by the way this is um i'm claiming that this is a sound representation of run length encoded data i'm not claiming it's complete by which i mean it would be perfectly possible to write one x one x one x and so on so um when we write down types for data structures so this this is i think an important point about programming and idris and programming with dependent types in general it is really tempting sometimes to write down the most expressive type you can possibly think of that captures every possible constraint on the data you're working with so in this case i might have to do something to i might have to add a predicate that says x is not the first thing in this list here and that will give me a a complete definition of run length encoding rather than merely a sound one turns out usually in practice that adding more stuff is not guaranteed to be a worthwhile thing to do so my rule of thumb is is to start with the least possible and only add a bit of information if i've either run into an error and i think a bit more in the type would help or if i run into a situation where i have a case that i can't deal with because the types aren't expressive enough so it's generally a good idea to err on the side of from my experience anyway generally a good idea to er on the side of not having much in the type and refine the type as your understanding of the problem develops so what we're going to do is we're going to write a function that um converts a list into its run length encoded form and then we're going to go back again um so we're gonna have to so we've seen rep actually we we saw rep at um at the beginning um it's just kind of entertaining to see what the program search comes up with for this um rather unsurprisingly it says well that's the empty list that's all right um i i tried this out yesterday i thought there's no way this is gonna work and you know it it comes up with increasingly long lists of just x until it gets bored so okay you weren't happy with four of them you're probably not going to be happy if i had more and more and um but kind of amusingly quickly it comes to the definition that we that we actually want so that's a repeating uh n copies of some value and um i think rather than writing the run length and coding first i'm going to write the uh the decompression first just because it illustrates something really important about quantities and putting quantities in types so we've got um we've got some wrong run length encoded data so the run length encoding of x's and we're going to return a singleton of x so singleton here so this is like a value singleton of some um some value so so a singleton of x is a type that can only ever take the value x so this uncompressed list it can only ever take the value of x's and it's really tempting you can do this this works perfectly fine in idris one it would be really tempting to say what i'm going to do is i've already got the list i'm going to bring it into scope and so what am i looking for i'm looking for singleton of x's well that's obviously just singleton x's isn't it so this would this would type check an address one um but it says no i'm not going to let you do that because x's isn't accessible why is it not accessible well if we look at the um we look at the type of uncompressed rhs we'll see that well i'm allowed to talk about x's and the fact that i'm allowed to talk about x's is crucial because i need to prove that the value we're returning uh is equal to x's but i'm not allowed to actually have x's we can bring x's into scope in a valid way so i can say i'm going to be explicit about the quantity of x's and and i could say okay well now x's is something i can use so i can uncompress this list just by looking at the type and we're done that would be a really bad idea though um any i mean maybe you can guess why that's a really bad idea but uh this would be a really bad idea because i haven't actually compressed it anymore i'm now carrying around the compressed version of the list and the original list so the fact that this doesn't have a quantity on it means that it's available at runtime so so by having that um we're in the right place now yeah so so the fact that we have these quantities means that we are we are constrained in what we can use at runtime and just by looking at the type we know what's going to be around at runtime and we know what isn't um idris one has a um a really fancy mechanism for calculating what is used by runtime so um so done by my former phd student uh matush attends jack and if i pronounce his surname anywhere close to right or it'll be a first um it's a marvelous um algorithm it works but the problem is it's fragile if you accidentally use something but you didn't mean to suddenly you're leaking um runtime data that you didn't mean to so having having it um in the type that something is unused um turns out to be a really uh handy thing to have so there's no um there's no way we're just going to have to write this function so we'll do a case splits um by the way i i think this function that the program generation should be able to write this function on its own uh there's enough information in the type that there's only really one way to do this at the moment it can't that makes me sufficiently sad that i'm going to work on it so i'm going to make this go but for now we have to do it ourselves um so what happens if we uncompress the empty list well that should be easy enough yes it can do that so uncompressing the empty list gives us the empty list and uncompressing the uh the non-empty thing well that's going to be that's going to be n copies of x plus whatever the recursive call on uh gives us here so um i'm just going to do that so we have to we have to deconstruct it so we have to uncompress will give us a singleton we have to have to pull the value out of that singleton and um so we're we're producing a singleton of rep mx plus plus rec surely the machine can find that for us yes thank goodness for that um so we've we've written on compression we've uh we've made sure that we're not storing that um expanded list at run time so we have to calculate it and that's giving us back this is a guarantee that the list that we're getting back is the same list that we put in in the first place um the time is running short so for rle i've got a question for you yeah frederick has a question and i need to ask it um no mike again does explicitly quantifying a type impact type erasure uh yes that's in fact that's uh that's exactly what it does um so if i were to so uh the the choice of syntax here is that if you don't explicit if you've got one of these um implicitly banned names so x is here and you don't say anything else about it you haven't written anything else about it then it erased that's given quantity zero so if you want to give an implicit type variable um a quantity other than zero you have to say what it is or you have to explicitly write it down so this will give us um an x's with an unrestricted quantity so we don't give a quantity in a binding like this um then um then it's unrestricted and we can also give it a zero if uh so in this case this is this what i've written here zero x's of some type that's equivalent to what i wrote without writing this explicitly oh and by the way this isn't this is a case where um uh where we have to infer a type that's not type so they're not automatically they're not automatically uh abstracting over types here that could be whatever makes sense in the context so it will infer from the context so i hope that answers the question and uh i mean i do actually want to run this and and if i did someday i would work through rle but it's um i think it'd have my page buffering so um yeah here's what i made earlier and um let's just show that it does now i haven't run any programs yet and this it's an easy track to fall into i'll just fall into it again um to um um to say i want a type check so you know ship it um whereas it'll be better if i uh let's uh let's show you what it does so uh what i'll do um i won't do because where is it there it is okay that's what that's what we'd hope to get so three a's followed by four b's and then uh uncompressing that it gives us the list we started with so great we can evaluate functions as well as right isn't that exciting right um this is a point to go back to slide a good point for a short break if anyone has any more questions because uh we'll take a short interview just talk about idris ii itself but um i'm guessing from the silence that uh there are no questions at the moment um i'm watching the chat and i will uh let you know if any pop up okay um so i just want to say a little bit about idris too itself uh because a lot of what i've been doing over the last year or so has been rewriting idris and i want to say a bit about why and a bit about the things i've learned on the way so i've only spent a couple of minutes on this so um idris one had got to a point where you know we i didn't really know what i was doing when i started writing it because you know there's not a lot of experience at the time of of writing dependently tied programming languages so and and i didn't really have much experience of writing an actual programming language of any form so there's a lot of funneling around and some design decisions turned out to be bad ones but they were they were okay we could live with them because we weren't really doing anything big we were just trying out you know what can you do with dependently type programming what kind of problems can we solve but then it kind of started creaking at the edges a bit it was becoming increasingly obvious that if we wanted to scale it up to anything we need to do a bit of re-engineering and i was thinking i want to write a bigger program in idris to show that not to show that you can and we've now got to a point where i don't really know how to write anything other than a compiler so opening all of these things together it maybe it's a good idea to to have a crack at implementing idris in itself at the same time um for conor mcbride and bob atkey have come up with uh qtt quantitative type theory and i saw that as a really nice way of describing eurasia in a in a type driven way well okay let's put these things two things together let's implement this again in itself let's implement it using quantitative types and let's just see how far we get um sodastream is now implemented in itself so what i did was implement it in idris one and then essentially over a weekend just go through the bits where idris one thought so in one we weren't being explicit that something was needed at run time and it was too we had to be essentially that's that's the only difference that we had to worry about um so i thought it into this too and to my astonishment it actually worked so now we have this system that's implemented in itself which is a lovely thing to have because it means every time you try a a new thing with the runtime or a new thing uh with the type checker or maybe change some bit of the the core of the system i have this ginormous test suite already in the form of it has to still be able to compile itself and it's uh it's it's it's amazing how often that's called problems uh early um but also we've so i mentioned this thing when i was talking about rle that that you you can go a long way with the kinds of properties you can express and i spend quite a bit of time trying to decide what kinds of properties i should use the type system to express so just not many the same as in haskell and write it just like haskell with a little bit extra or do i go full-on prove the correctness of the compiler um now neither of the extremes i think would make sense we've gone somewhere in the middle and uh what we've ended up with is the core representation of programs is parameterized by the names that are in scope the variable names that are in scope so um probably uh several people in the audience have had some experience of playing around with representations of lambda calculus and you probably found that representation of names is one of the most annoying things to get right and it was certainly the um the source of a number of errors in idris one the great thing is in industry those areas simply can't happen unless unless we have kind of two levels of bugs i suppose where where a bug in idris ii causes us not to spot a thing that is a bug in idris too but you know bearing bearing in mind that sort of um possibility that kind of error can't happen another kind of error that can't happen is in idris two every program or every function has to be covering by default so covering all inputs by default um so we can't have missing cases uh unless we uh unless we turn off you know there's it's always a good idea to leave a leave an escape hatch for a programmer but we haven't used it um so there's there's uh so every program it will complain if a program doesn't cover um all the possible inputs that means that if there is any kind of input where we maybe don't know what to do we're very tempted to say oh this can't happen well we can't do that we can't make that assumption we have to we have to come up with some um some explanation of what happens in that situation it usually turns out it's to report an error so that means that idris ii isn't going to crash because of a user error it may crash because of a system error like a file not existing or even like a user interrupt but it's not going to crash because there's a missing case in a function definition again you know modulo bugs there may be bugs but um we've certainly massively increased our confidence that that kind of error isn't going to happen so it's implemented uh of compiles via scheme so you just want to compile to c using a runtime that i'd written and just as a let's just hack this up quickly i want to have a compiler i thought compile to scheme scheme doesn't have um compiles i'm type checking so i can be completely free in the kind of code i generate and um pleasingly it turns out that uh scheme is significantly faster than my hack.c runtime so this is basically what happens if you have your runtime written by someone who is experienced at writing runtimes shock turns out it's a good runtime so um idris two programs run significantly faster than idris one programs um scheme you might think well it's a dynamically typed language so surely it's got to do runtime checking and you've done those runtime checks and this is true pleasingly scheme has an option to turn off those runtime checks so we do that and that gets us like another maybe thirty percent speed up so scheme has turned out most kind of stroke of good fortune has turned out to be a great way of of compiling it so you can install idris too just by installing scheme and then we distribute the the generated scheme and you can uh you can build it that way so it's relatively quick to build and say it's about about an order of magnitude faster than idris one and uh i can give if you've played around with idris one you probably run into this frustration that it's that it's it starts feeling sluggish really quickly um i just want to give you a feel for um how much better it is so we've got it quite happily building itself here um if you're a go programmer or even a c programmer you're probably thinking wow that's incredibly slow but the thing you need to bear in mind watching it build this is that not only is it um type checking the thing you're also getting these guarantees so it's that um that all the names are in scope that all the functions are covering all the possible inputs um and so on uh so that'll take about takes about a minute anyway so that's um implementing idris too and i say this two reasons firstly i want to advertise um a summer school that's coming up so free registration um it's the scottish programming language and verification summer school and it's online so you don't have to come to scotland uh to do this so there's several interesting courses but i'm going to be explaining some of the internals of how um idris 2 works and we'll say the reason the other reason i want to tell you about this is that uh there's a lot of stuff to do and i'd really like more people to know how the internals work so that i don't have to i don't have to fix all of the stuff so um so i'm very happy for people to come and report uh any issues that you encounter but i'm super extra happy if not only do you come with the report of the issue but you come with some idea how to fix it and i'd love to get more people um in that position um okay so um i've been talking for a very long time so uh i'll i'll talk for a little bit longer because i don't want to do this um the thing that i um the thing i'm enjoying about having quantitative types is that quantitative types particularly linearity allows me to express things that have previously been really awkward to express in types so a kind of problem i've been interested in for a while now is is dealing with external resources so um types typically uh they're very nice at explaining what kinds of inputs a function can take so the they're nice for explaining functional properties of things but they're not necessarily so great for expressing non-functional properties like resource usage properties and i've been interested for a long time in how to express resource usage properties and types so that you'll look you're expressing not only what can happen or what what kind of inputs are allowed but when those inputs are allowed when those operations are allowed to run and the way i've been typically handling this is by writing um a state monad that is uh parametrized by the state of the system so the input state and the output state and how the output state is computed from the result of an operation and this works you can you can absolutely express all kinds of interesting systems in this but they don't compose so if you have if you have two things with some states and you want to put them together well good luck you're just gonna have to do that by hand and this this i found really disappointing came up with all kinds of increasingly complicated ways of of managing to deal with that and then qtg comes along and i think i don't have to do these i don't have to write a an index statement on that anymore i can just write linear functions so i'm going to illustrate that with um the simplest example i could think of which is a data store it's kind of unrealistic well it's a very cut down realistic thing um so our data store our secure data so we've got two states that we're in we're either logged out so that's where we start or we're logged in there's a secret in that data store that we can read um and we can log in i guesses into log in stage log out yes into the logged out state but the tricky thing is that we can't just call the login operation and expect to be in the logged in state so when we do these um when we represent these machines we have to consider that as programmers we're not fully in control of the environment that we're working in so we're not fully in control of whether login succeeds we might give the wrong password or the system might be there or any any kind of other reason well i might go wrong so we're gonna we're gonna do this as uh we're gonna represent this system as a linear type system we're gonna write a program that works through the state of the system so wow one minute 56 it's usually about one minute so that shows you how much uh zoom is uh taking up um right so uh where is it did i just did i close my vin window that's silly that was silly because i had all the fonts set up right size um i think 32 is the secret number good i'll do uh right so so this is how we might represent that kind of system uh as a linear type system so uh well you just have to imagine that this is connecting to them some external services bit of a mock-up the important thing is the types of the operations so one thing about uh quantities is the quantities are on binders only so we can't um easily put quantities on the return type of an operation so that's that's a question of like design of the call theory it's the design that they chose for qgt everything works out nicely that way so i've picked it that way we'll just have to we'll just have to live with it so that means that if we want to make a new thing that is only to be used once the way to do it is in this kind of continuation passing style so so we're going to write a program that connects to some store so it's some io operation but it's it takes as an argument this continuation that says you if you can write me a function that takes one logged out store and then ends up as an i o program then you have a you have a correct implementation of your store usage protocol so this is the only way of making a stall that's what i'm saying so the fact that this is the only way of making a store means that every store we have there's going to be exactly one of it so we can do all of these things that i showed in the diagram uh log out is probably the easiest type to look at first so that takes a store that's logged in and it returns a store that's logged out now remember the uh the rule that uh if if you've got some linear thing and you pass it to a function the rule is that if that function is used once then the linear thing is used once um that does have some implications for the way we we use this we're only ever going to be able to use this log out function or given that it takes a linear thing and given that we have the only the only stores we'll ever have will be linear then calls to log out i'm not going to type check unless we're using them in a linear context which means that the store that comes out is also going to be linear so again i'll walk through that again by an example but this is why we don't it's just to say this is why we don't need to worry about the the quantity of the store that's returned is that we'll only ever be able to use this in a linear context so the most complicated type is the one of login so um so it takes a log out still on a password and we won't necessarily get a logged in or logged out store back and i've done this by returning um pair so this res type this is a this is a dependent pair where the first thing is just some value that we're returning and then the second thing is a type that we're going to compute from whatever that first thing the result of that first thing is so i could return an either here so either store logged out store logged in um but this way of doing it is much more flexible so returning a store and if the if it's if the b if the result is okay then it's logged in otherwise it's so let's just write that program um so it's always good to do these incrementally just by saying you know help me out here what have we got so i've got a store that's logged out and um i need to somehow get to i o so basically i i'm only going to get through this if i manage to discard this store so um in fact i could just i can discard it by calling disconnect but let's let's let's try to connect it first so we can call we can try to log into the store so um so this res type we don't actually know what this res is and i'm not going to tell you quite yet i'm just going to assume it exists and we're going to try uh logging in what are we going to guess for the password let's let's see if that does anything so that's told us that you know great we've we've tried to log in and our rares well it's the results which is a bool and this other thing so i could at this point i guess i could look up the documentation for res but it's rather more fun just to blunder on and see you know i guess it's a it's a data type so i guess we could uh i guess we could pat and match on it and see where we go so let's do that uh so we've got another shortcut for making a case block i i'll do anything to avoid typing so i've got a shortcut for doing that and uh if so there was a question earlier about what does it mean to use something so this is what it means this is one example of what it means to use something so res had had linear usage um and this res we've now put it in a case so it's been used and it has a result which is a case valve which is not being used we can look at the types here um so we now have one case valve so this this thing the result of the case split is a case valve and the res has now it's now been spent so we can still talk about it but it's being spent and my favorite way to illustrate exactly what's going on here just to get some kind of intuition in your mind is um it's it's 7 p.m here now so i think the sun is over the yard i'd like to illustrate through the medium of saint andrews yippee ipa so i have one of these this is my this is my resource and i can do a case split on the resource so this is this is what i'm let binding to and by doing a case split on the resource so i now have let's not spill it in any interest so this is this is now empty i have zero of these but i can still talk about it it's still available it's still in the context and i have one of these and by doing kind of whatever kind of disposal so whatever kind of analysis on this i will end up having none of these um i'm going to leave that alone for now now for two reasons firstly if i finish the protocol the talk is over and that'll be bad and secondly that's a scottish beer and it needs to warm up before uh before i can drink it um probably some people wondering whether that's a joke or not i'm not going to tell you right so here's my uh so what we'll do to find out what's going on we've got a we've got a case value we don't know what red is let's have a look at what res is and it says ah you've got a you've got a vowel and an r i'll take a look at what they are i mean this is this is the process this is the this is the process of interactive type driven editing is that at every step make one step towards the program refine the program a little bit then ask the machine what it knows ask the machine if it can help you some more so this whole well i've i've now got some resource r uh i know the type of that result as well if it's if if the value is true then it's logged in otherwise it's logged out so that's kind of a hint that um that if i want to make any progress with this store then then i'm going to have to look at what val is i'm going to have to inspect this value so a general principle or general thing that happens a lot independently type programming is looking at one thing can tell you about the type of another thing so just by looking at the context here we can say that looking at the value of this mysterious vowel that can tell us uh what uh what the type of the story is going to be so i'm going to rename that s before do a k split on this so in this first case uh the result was true we have a logged in store so we can make progress in the second case we have a logged out store it didn't work it failed and i guess something we could do is give up that work good um so again i'm not going to work through this whole protocol i just want to show you the the basic idea of how you progress through a protocol and i think as before is one i made earlier i picked a different password earlier um so so this is um an example of the whole thing so we so we have to work through this protocol if i try for example if i try not disconnecting if i forget to disconnect and then and then return it it will say well you didn't you didn't use that linear name there's no uses of it you didn't finish the protocol therefore i'm not going to let you quit yet so what we've been able to do here is encode an api and encode the state transitions and particularly encode when we're allowed to do things by using quantities in types and just a little bit of dependent typing going on to um to to refine this type according to some results we've got um so it's worth pointing out actually if um uh um we could have returned um an either type so either store logged in or still logged out one reason why we might not want to do that is that um it might be uh so let's do it here okay haven't even drunk the beer yes right that's where that's that's still not where i wanted to be anyway let's not know this now the point is you might want to do some operation on the store there might be some operation that you can do without actually knowing its state so for example you might have a ping operation you might want to know whether the store is alive or not and you might want to do that independently of whether you know it's logged in or not so you might want to do that before you you test the result of the operation for example so just allows you that little bit more flexibility uh right one last example and then then i think i'll stop is as an example that um i think it really does come off when you when you're designing a new language it's good to think about um what the facilities of that language might allow you to do in your standard apis so um one that uh that comes up in everyday programming is is network sockets so uh network socket programming is um i find it a little bit fiddly myself so there's an api for this that uh that they have in order to get a socket up and running to a server socket off and running you have to say i'll bind it to a port i'll start listening for connections when i get a connection i'll accept that connection that gives me a new socket that's now open um and it's not represented in this diagram but that listening socket is still going so so there's a there's a lot of state transitions going on and each of these operations might fail because maybe some of some external results maybe there's maybe you're out in memory maybe there's maybe you're not not able to bind to the port because something else is on that course and so on so all of these things might go wrong and if you're writing um if you're writing a program on sockets uh in everyone's favorite typed programming language c you get this um nice typed api that tells you um tells you what it is you have to do so we create a socket and um we know what to give for the main type of protocol because they're all hints so there you go and that returns an int that that hint is the um id of the stock but i think it also represents whether it went wrong so there's a lot of hints going on here so it's useful to think about which of those some of these are representing error cases and some of them are representing actual sockets so just to give a bit of help um the blue ones um so this one this one this one and so on this one and this one these are representing uh the socket id and then uh these ones these red ones they're representing possible errors so the inputs uh the index being returned is kind of doing a double duty in some cases so some of these inter-representing sockets somewhat representing errors so these are the primitives that we have to work with and um so i'm not mocking c here because it's this is a 1970s technology it's uh and it's a natural it's like the low-level way to do it it's fine but if you've got a higher level language it's good to think about how you might give a higher level api to that so idris has uh its network primitives so it's a little bit more informative i've simplified this slightly because uh we're not using uh we've abstracted over i o but we can at least say that what these int mean that these ins have an actual meaning and the operations might return an error so it's either an error or a socket or in this case it's just a result code or in this case it's uh accepts is so when you accept connection you get the initial socket that you had and you get a new socket that is the socket that you do the communication on so we're a little bit more informative here also we're saying that um we have to make a choice about what to do about errors so the idris runtime um doesn't have exceptions uh this is a deliberate choice this is um this is because we want we want errors to be explicit in the type so this is a language for type driven programming it makes sense to you know if there is a choice should i put a thing in the type or should i not put a thing in the type if there's any doubt at all i should put the thing in the type so it's perfectly possible to implement an exception uh api on top of this so in fact in the implementation of idris 2 we have sister or um user errors are done using an exception implementation and low level system errors i've done just using this form yeah we have to make that choice so we've been explicit in the type um so what actually is in the primitives is is we say uh this io this is this is an interface so if you're a classical programmer you'll think of that as a as a type class and then this using notation this is just a shorthand that allows us to say anywhere you see io in this block it needs to be i need to have an implementation of this interface as io so in haskell terminology it needs to have an implement i'd have needs to that needs to be an instance of has i o that has i o type um so it's only slightly simplified but just think of this as i o now really what we'd want to do though that that's that's capturing errors so it's capture and it's capturing what the things might do and how they might go wrong what it's not capturing is when things are meant to happen so it's capturing what's what happens but it's not capturing when things happen i really like to somehow express that i can only call bind on a socket that's closed and i can only call listen on a socket that's banned and so on so um so without going into all of the details of what this mysterious l is well i will say it's a it's a monad transformer that turns a monad into something into a linear monad that's all i'll say about it in practice what it allows us to do is say how many times the result of the operation gets to be used so bind takes a linear socket in the ready state and it returns something that i have to use exactly once and it's one of these res again it's it's a pair of a result and a socket that's either closed or banned depending on whether that operation succeeded uh close is a bit simpler it's a socket in any state so i um just made that choice that you can call close at any but you can give up at any point so this is this is another reason by the way why we don't return either for errors we return this uh we return to some arbitrary expression because i couldn't pass an either to this i'd have to resolve which one it was here i can just pass the socket whatever state it's in even if i don't know the state and in that case it'll give us a close circuit back and then once we're done we can only discard the socket once it's done and the other operations follow the same form as this uh this bind operation so um just see what that looks like in into in a real program so i i wrote um an echo server that all it's going to do is is start up a server and then it's going to receive a message and it's going to send the message back so what we have to do again i'm not going to do this in full because it'll take too long and you've already been very patient with me so so what we'll do is um run the operation and then see what state has come back uh from the socket so a problem with like let's you have to make this choice about how to deal with errors and there's all sorts of pros and cons of do i return uh an error code or do i throw an exception or do i return a type that indicates an error so the problem with having to re returning the time to indicate an error is that you have these massively nested case blocks um and you don't really want to have the massive you know you'd be far off to the right of the screen so um idris provides this um uh pattern matching uh do notation so you you might see something like this if you program in haskell that you can run an operation and then bind the results have this uh i think haskell calls them irrefutable patterns so if it's true then we'll just carry on down the happy path uh idris allows you additionally to say what to do in the other cases so it's it's like we've programmed to the happy path but because we have some coverage checking and because we need to we need to clean up with whatever state the socket is in we need to somehow get to the right state we we have the these um alternative paths so if anything goes wrong we we go into the the pattern matching alternative and so in this case you'll see that um if binding succeeded uh then we have a closed socket sorry if any phone we have a closed socket if it succeeded then we have a bounce socket so this by the way uh i don't have any pull programs in the audience i used to be a pearl programmer uh this this is like i saw this this idiom in perl where you sort of open a file or die and i saw that idiom throughout and i thought that would actually get me out of this problem of the massively nested uh case blocks without having to um without having to uh introduce exceptions so i find this a a reasonable way to work and then the rest of the program i'm going to leave that um i'm going to leave that bad hole in there because it doesn't type check no it doesn't because um okay so that's type check we've got this hole but um i don't care so uh don't care for now i'm just going to show you what happens when we try uh running this let's do it the way i tested rather than making something up and just to say what this is uh ipackage is a way of describing the contents of a package and if you say find ipackage it will just find the one in the current directory that tells it what dependencies it needs so there's there's a different there's dependencies for the linear i o and dependencies for the network uh anyway so we have a program developer yeah ron echo just starts up that server uh and runs it um and it says warning compiling whole main.bad so as long as we do something i do this just to show that you can you can run incomplete programs um realistically the majority of programs you're ever working with are incomplete in some way certainly if you're a developer they're incomplete in some way and i don't want to stop you being able to test what those programs do if you haven't finished them uh in this case thankfully the server has started so it didn't encounter that whole if it does encounter that hole it will just crash uh run time so so it's um it's okay to do that obviously you need to if you want to ship it then it's a good idea to just to fill them all in um so let's let's actually try telnetting to the um [Music] there we go so just to prove that it is an echo server it is doing something and okay i guess i only really prove that uh it's it's my server doing something if um if i shut it down and it doesn't work so let's let's just do that very good um okay i haven't left any points to ask questions maybe everyone's gone for dinner does anyone have any questions at that point we have a number of questions actually um some of them are general sorts of questions uh will you take anything right now or do you want to wait until the end for the general ones if there's any specific ones let's see the specific one but let's go to the general ones um in a moment um i don't know if there's anything that's relevant to what you're talking about right now oh let's go general then okay okay um nobody has a mic today apparently so i have to ask uh most of them so uh actually there's a question relevant to the interlude that you did from christian and he's curious are you at a point where you'd welcome new code generators for uh for example beam c etc as contributions so there is already um an erlang code generator rather than b so the way i'm going to take the same approaches as uh saying like wagon several of us working on it uh as we did with idris one which is that we'll have a couple of built-in things so the problem with having lots of code generators is as soon as they're in the idris2 system i have some kind of obligation to at least know how they work and at least be able to do minimal maintenance on them and i can't do that beyond just a couple so we have um we export idris as an api so you can you can link to um you can link to the whole system and you can write a driver that adds your own code generator um it's a relatively easy thing to do and and i i encourage people to do that and there's a few already out there so there's a there's an erlang one out there um there's a special secret effort to work on the oh camel run time which is making some good progress it's actually uh amusingly it's only slightly faster than the show scheme which um just shows you how good show scheme is because ocam is fast um so there's so definitely do that um we we have this same philosophy the the um you know platform just because you're running on a particular platform doesn't mean you should have to write programs in the language of that platform so just because you're running on the web that shouldn't mean that you have to write your programs in javascript it should be possible to write it in you know whatever language you want maybe you have to run on the jvm for whatever reason so so idris will the language itself like the internals the language is agnostic about the the target and that there's there's ways of of writing foreign function calls to have multiple calling conventions to say or if you're on the jvm do this if you're if you're native do that so so there's not going to be any big assumptions made about the runtime so i mean that that's a really long way of saying yeah go ahead and do it it'll be cool okay address in the browser i'm going to be waiting for that javascript uh back end but is there's that one actually is part of um the uh main idris 2 repo and uh i haven't tried it yet but um the tests pass oh you know so it could be could be good enough for front-end work then um yeah i mean i can't i'm not going to commit because i haven't tried it but i mean this is always you have to remember people keep forgetting this i think idris is at the end of the day it's it's got research funding behind it it's a research project i work at a university i'm grateful for the funding i get from six uh scottish informatics computer science lines from epsrc engineering and physical sciences research council but otherwise it's um you know that that's that's all we have we're not a big team of uh of developers so um it might work it might not but if you try and it doesn't work the best way to make it work is to get your hands dirty and i'm gonna i mean the fact that we've been able to implement interest to you in itself says at least something it doesn't tell you very much but it tells you something it tells you it can scale to that sort of level i think the javascript back end if it compiles to node rather than in the browser i think it's got enough to be able to compile to run idris 2 in javascript not tremendously efficiently but um but it does work so that that gives you an idea of where you're at so if your back end can compile in this then you've pretty much got it uh working but don't always bear that in mind that uh you know you probably have to get your hands dirty if you're doing anything other than what i've done kind of on that point um just curious what your vision is for idris you actually are showing some very practical examples now and um i'm wondering if you have a similar kind of uh avoid success at all costs philosophy or you could actually see idris someday being used in production or just strictly speaking um a research project um so let's uh so i guess we all know about the two different bracketings of avoid success at all costs um i would bracket that as avoid success at all costs so being a research project so we i i'm i write papers about idris i don't necessarily get them accepted or at least i like them uh which means i'm trying to do things the right way so i'm not gonna i mean there was an early stage where i was taking various short cuts just to see how things might work out but i'm not gonna do that anymore this this has to work the right way so it's not about um you know taking shortcuts to get success or just leaving uh cutting corners uh yeah to to have some success at the same time if people do want to use idris for something real um i'm certainly happy to help out um there are people using this for real in industry where i'm helping out um but you know i can only help out one person at a time or one team at a time so it's um this this this doesn't necessarily scale um so the so what is the vision um my goal is in some sense to optimize for fun so i'm going to work on the corners of the of the the programming language design problems that i find most entertaining while still bearing in mind that programming language research exists for a reason it exists because people have a problem that they actually want to solve and i think the next thing that is going to be that there's going to be the right balance of interesting fun and important is this program synthesis so you only really got a taste of it here and idris really does a a tiny bit of it but um it's well if there is one philosophy that uh kind of covers the whole thing you know what one one overall problem grand problem that we're trying to solve is how do you make it cheaper to make software that works and be confident that you have made software that works i think type systems help you do that because type systems move uh more of the understanding what the program does and as as compared to what it's supposed to do moves that sort of thing to the machine this is something that machines are extremely good at doing they're extremely good at checking whether something fits a specification they're not really so good at generating something that fits a specification a human might look at something and say yeah that is that's the program i want to write so you know so your program synthesis can give you a little bit of help as to generating the program you look at it and think yeah that's probably the program i want but the machine has a machine knows that that program type checks so using what the machine knows to help you ride a program that works be confident that that program works but you still have some kind of input into what that program is supposed to be that's sort of my goal for how you might reduce the cost of writing correct software and have some fun at the same time i feel like i should edit that down into like two sentences because i felt very rambly but um there you go no that was that was interesting to hear honestly um i have a few more general questions if you like ah sure go for it i mean i'm now on the summary slide and i i do have more so i i promised concurrency but then i realized that if i was going to do concurrency i'd spend the entire talk setting it up um well should we do the summary and then come back to the general questions um yeah i mean i think i've basically said the summary uh just there but the the thing that i want to highlight is this idea of programming as a conversation um partly because um we have a new project that's just started so uh guillaume male is uh working with me on on this project for how do we make programming uh more like a conversation with the machine how do we make it more interactive and uh but with with like sound um theoretical foundations so so what is the language of interaction with the machine and um i think yeah i think the answer to that is elaborate reflections for better meta programming better ways of um kind of programming the programmer so when i show you these uh program search what i'm doing there is a i'm doing a case split and then i'm doing a search and if that doesn't work i do another case split and then a search and that's not far off what i'm sometimes doing when i'm exploring um what it means to solve a problem so this this this project programming being a conversation is to some extent about programming the machine to be a programmer using algorithms rather than when i say algorithms um i mean algorithms i don't mean heuristics i don't mean machine learning i mean i mean being able to really explain what it means to write a program from a type so yeah that's that's that's kind of what it's all about that's that's where we're going here um so what do we do with that um so session types is a fun problem to solve in that space so session types are a way of describing concurrent processes um so they're describing the messages get that get passed by concurrent and distributed protocols so how do you guarantee that that um um that approach that that you have an implementation of the protocol that is correct according to the specification and crucially what happens if you change the protocol so everything i'm showing you here has been about how do you write the program in the first place i haven't really said anything about what happens when the types change what what about maintenance so i think there's a lot to be said in the interactive editing space and the interactive development space of refactoring basically what what can what can types do to help refactoring and uh yeah otherwise you know that that's that's kind of all i have to say types are a lot of fun adding quantities to types makes them even more extra fun and um please come and have fun with us so um yeah i'll stop there i'll move on to questions and i think i think this is now warm enough to drink which is yeah i have to say you're horrifying the germans in the audience by drinking warm beer oh that was deliberate um i mean i was i think and houring about whether to have the beer i'll say oh that's terribly unprofessional i thought yeah but i could do the warm beer thing it humanizes you um before moving on to questions let me just thank you for the talk i actually find that as much as it's nice to be together in person to do these meetups one of the advantages of the format here is we can kind of follow along with you as you as you code and as you work much more closely and that's really interesting that's really fun to see i'm really glad you did that thank you uh so much for the the insight into how you're thinking and how you're working through the problems interactively and there's a lot of trade-offs in all of this but from my point of view everybody might have less and i'm non the wiser it's marvellous uh no you you kept an audience of uh 30 some odd people for the entire time well thank you all for saying so frederick has a question how does idris flavored linearity inform garbage collection ah that is a great question because um i have another student who who is working on just this problem now the um the the annoying thing is that it doesn't really at first because um so as i mentioned sometimes three hours ago when we began um the idris quantities only promise that things aren't going to be shared in the future they don't promise that uh things weren't shared in the past so so one thing we'd love to do but can't easily we'd love to be able to say right this this function is inspecting a linear list uh we've got uh the head and the tail if we're going to make another list we can just reuse that head and the tape that would be lovely but we can't do that in general what we can do though is the the type checker knows when it creates a new value it knows the the quantity or the context uh when it's creating it so it knows whether it's creating it in a one zero or unrestricted context and the runtime representation of constructors has a few spare bits so you could use one of those bits to say this thing was constructed in a linear context you could do that at compile time and then instead of splitting on you know the compilation saying this is new or cons you can say this is nil or cons linear linear cons and in the linear branches you can you can use that information at runtime now i don't really know how well that's going to work um because obviously it has the cost of making the program much bigger um and maybe there's some analysis we can do to say oh this is always linear but um my uh master student andrei vadella has done some very promising initial experiments that suggest if everything lines up this could be being linear correct uh could be a really big win because you're not allocating you're not garbage collecting as much but that is that is as yet unexplored apart from this very small amount that uh that andre has done but i think it's very promising because it is at the end of the day it's it's an it's an additional bit of compile-time information and let's see if we can use that additional bit of compile-time information to do something useful so other things we can do with that is um you know we can already do things like have a type that represents the fact that the test has been done so we don't need to do the dynamic check again as long as we're still hanging on to the proof so that's one place where we can use times to improve performance but this linearity thing that's that is one more thing again that's a long way of saying i don't know but we're working on it so thank you kk asks can you say a little bit about the origins of qtt what made it a good fit for linear types in idris how does idris's design compare to say linear haskell or rust even oh yeah okay i um so where qtt came from that that's essentially the uh um the the amazing mind of conor mcbride who who wanted to solve this problem and essentially solved this problem but for a small bug which um which bob ackey found and fixed and part of the reason that the qtt therefore became a good fit for idris is the um i don't know it's this this is probably an unsurprising reason it's just i've known connor for a long time and he was uh heavily involved in the superversion of my phd and a lot of that involves thinking about eurasia and one of the things about qtt was let's stop doing eurasia by ad hoc analysis you know however much we we show the correctness of those analyses let's let's get it in the type let's work out a system that gets in the type kind of figured that out um i picked it up off connor what made it a good fit is really the um the linearity side of it is is kind of a happy accident it's it it's not really linearity that was the thing uh i was bothered about the thing i've been bothered about basically all the time i've been interested in dependent types is how do you know what's there at runtime and how do you know what isn't and you know i wrote a thesis on this or an analysis that works out what to erase based on the types and i'm delighted to say that that my thesis is now completely the wrong way to do it because um because connor and bob came up with a better way so it's the fact that i was i was interested in the uh in zero multiplicities not so much that i was interested in one multiplicities and now i can write that so i use that run length and coding example uh we used to use that run length encoding example as as a way of showing how tricky it was to think about eurasia now i can use it as a way of saying how how clear it is to think about i think it's clear maybe people don't agree but uh um how clear i think it is to just say what's there at runtime and what isn't so the linearity thing is just another thing that works in the same system um and as for how it compares with haskell um the intuition that you have for how linearity works in haskell is exactly the same as the intuition you would have for how it works in idris the uh the difference is that they don't have the zero multiplicity at least as far as i know they don't have the zero multiplicity and to some extent they don't have the need for the zero multiplicity so in in haskell you have this you have the the very distinct um type language and value language term language program language whatever you want to call it whereas in idris we have the same language for for both it's part of what makes types first class um so we have this additional problem that we have to think about zero multiplicity that haskell doesn't have but other than that uh difference they're pretty much the same um or one thing uh haskell does have um if i remember rightly it's been it's been a while since i looked at the lenny haskell paper but i or the first linear haskell paper is i they have um i remember it quantity polymorphism so you can not only so you're not only abstracting over types and values you are pressing over the possible quantities of things and you're able to do some manipulation with that um i would like that i would um that would allow a lot more expressivity the question is it might come at a cost it would potentially make libraries and apis harder to think about we have to think carefully about what went in the prelude so you know adding new stuff to a type system isn't you know adding more stuff isn't it's not necessarily free it doesn't necessarily like it gives you more things you can do but it might give you more problems so it remains to be seen what um uh what the right way to um uh to deal with that is but um actually another reason why the main reason why idris doesn't have quantity polymorphism is uh more that uh i don't think uh bob has worked it out for not as far as i'm aware bob has not worked it out for qgt and um my strength is in implementing type systems not improving them correct so i'm going to wait for uh i'm going to wait for someone to figure out uh the right way to do it before i uh before i dive into it but yeah they're very similar and the the programs that i showed you actually the um apart from that uh so the fact that i'm returning a pair of a boolean and something computed from that boolean so that's that's kind of a small implementation detail those examples with the uh the the state um the state of um sockets and with uh the data store you can absolutely do those examples in haskell you don't actually need full dependent types to do those examples uh depend types make it i think a little bit more expressive what you can do with them but you could you could do those in linear high school since the question also mentioned rust i've been trying to think i've been trying to think of an intelligent question myself and uh uh and i can't come up with one i wanted to ask you something about the relationship between linear types and dependent types because i always thought of idris as that dependently typed language and rust as the linear type language and here you're bringing them together and i'm wondering how you would explain their relationship for for someone who is not as deep into the subject as as yourself so i i don't really know an awful lot about rust i enjoy reading about uh i very often get rust envy when i look at some of the some of the low-level programs that they're writing and are able to you know make these pretty strong correctness statements about so um so i would like more of that in idris but um let's uh oh let's let's massively oversimplify um um because that's all i can deal with when it comes to rust um so i think we can probably or many of us will agree that shared mutable states is is a bad idea and it's where it it's the one of the biggest sources of where programs can go wrong so idris and haskell and pure functional languages they remove the mutable bit of that whereas rust removes the shed this is that is that a is that a reasonable way of maybe about to think about that a bit more um but no no that's that's that's that's good actually i hadn't thought of it in quite those terms that helps say that idris is is the duel to rust in some sense um so we can add mutability but if you add mutability and idris your types tell you that you've added immutability and in fact the implementation of idris too i i make no apology for this the implementation of idris 2 is extremely mutable there's a lot of mutable structures in there and that's just because when you're when you're type checking um dependently type program information doesn't all turn up at once so so you've got these implicit arguments you don't know what the type is you have to wait for things to show up before you can fill in those tags and you'll get gradually you'll get more and more information it's just faster to do that um with with mutable types but the types tell you or mutable structures the types tell you that there's mutation going on so you know that um if there is some problem with mutation you know here's the red flag this function has the red mutable flag um saying this is this is where it might go wrong uh and i guess likewise rust has um you know unsafe and uh i i assume i don't actually know this you can i'm sure you can do shared beautiful things in rust but uh somehow i'm um so yeah there's there's there's the distinction i um i think rust has um so you've got you've got ownership and borrowing and we don't have um we don't have a sense of borrowing in idris and sometimes i would like that like i'd like to be able to pass a linear thing to a function and say um i'm only lending that to you it will still be available to me when when you come back so um so we need to i need to figure out the rules for how that might work um it would basically you know you can you can case split on it but you can't do anything with the things okay split on for example um so be nice to think about that and how would we allow borrowing it will make programs look a bit nicer i guess there's another distinction yeah i suppose they're thinking a bit more about memory and rust which is not something you would typically do in a functional programming language i i think that there's something that might be quite fun actually i'd only very briefly looked at this but we we talk about uh we can talk about erase things when we talk about any race things so we could say i'm going to show you with um with the run length encoding you've got this relationship between the list and the run length and code of representation of the list and the list that you've got we had a zero multiplicity well maybe a similar thing you could do is you could have i don't know an array of bits and the meaning of that array of bits is determined by some other higher level type some other you know complex data structure let's say it's a i don't know a balanced tree um but if the balance tree has multiplicity zero your array of bits has multiplicity unrestricted so that you can maybe program in terms of the nice high level structure but the thing that comes out at runtime is in turn with the low level bit representation i have no idea if that would work how it would work but but pretty cool if it did um with types showing you that the two things are essentially the same thing but the runtime representation is cheap or the runtime representation is something that you can be precise about well thank you uh the point about sharing um is informative i think i probably i i personally concentrate on the immutable part i never really think too much about the sharing part but as you were saying we're on this journey toward making programs more safe and more correct and these are different parts of that right i don't know it's been it's probably hard to tell my differences between idris and rusk really easier to look for the similarities well understanding linear linear types versus dependent types i i think is what i was curious about doesn't have to be specifically about rust um so um actually this this is a um i don't normally get around to mentioning this but it's popped into my head so i'm gonna say um so having a core language with linear and dependent types i don't know about this outrageous claim that you know there's your one true core language any any language you want to implement is um you can do this with a core language that has dependent and linear types and i'd partly say this sort of thing because it'll annoy someone they'll disprove it and in doing so they'll come up with something really cool but the other way the other reason i say it is that there is that core language that this part of idris and the way the system is structured so you've got the high level language then that com that kind of desugges to an intermediate language that's just like the call construct so it's um pattern matching uh function application uh case box so that is exposed as part of the api and i think it would be quite fun to write a different surface language that's not this you know language that looks a bit like haskell only strict um and is otherwise a functional language instead of doing that let's have a surface language that instead emphasizes the linearity and becomes an imperative language with dependent types with the linearity making sure that things are only used in the right state and sometimes you know when i'm out for a wonder and letting my brain go to old places and i start thinking about what that language uh might look like and i think oh when i get back to my machine i'll start sketching it out and of course when i get back to my machine i've got some email about a thing i forgot to do so i never get around to it but i think using that core language that interests here exposes i think i i would love it if people not only had fun with uh writing new backends for address but also have fun with writing new front ends for address so what what can you do with this um this this thing i'm claiming is the one true core language well i'm glad this conversation uh elicited that response uh we have a few more questions from the audience and apparently nobody has a mic tonight and i have to ask most of them evgeny asks is it possible to take a function that is in fact linear but not declared as such and build a proof that it is indeed linear uh not within the system not not in idris itself um i could imagine some kind of analysis like a a linter that says hey this function is linear maybe you should make it linear because i did this coming back to the the garbage collection question from earlier so if if you let let's say the function is linear safe that might give you some some opportunities for optimization so i can imagine a compile-time analysis doing that but um i can't think of a wave that we don't have that level of um introspection on on data types united we did but we don't thank you frederick has another question i think he's our number one question asker tonight and just to bring another language into the conversation does idris have something akin to agda modules agda modules are sort of like function abstraction but with a few extra niceties yes i sometimes thought about you know should we have a modules it's not necessarily anger style but um ml style and i think active modules are kind of similar in similar in style and um the reason i've ended up not doing that is interfaces in idris are almost but not quite like modules and and i sometimes think we should explore further what that even means so their modules in the sense that they provide an interface you can you can you don't have to provide like only one implementation of an interface like um so in haskell you can only provide one implementation of its ipad in idris you can provide uh multiple implementations of an interface and you know that's that's that's got pros and cons that has been debated at length in various other places but one one thing it gives you because you can have multiple implementations is you can say right well i'll treat an interface as a module we'll write this signature and then we'll just write lots of different implementations for use in different contexts um so this doesn't quite work in address two yet it will at some point but interfaces are a high level construct they translate down to the core language in that sense they are first class so that means you can calculate buying the fact that the de-sugaring doesn't quite work yet um you can write um a function that computes um an instance of the interface so that gives you something a little bit like first class modules in that you could say i have this interface quality module um i have a data structure that you know if there's a small number of elements i'd be better using a list if there's a large number of elements i'd be better using a tree say so you can write a function that calculates at runtime which instance of that module you want which is that interface you want um so yeah it doesn't quite give you full modules in one sense but it gives you a little bit more than modules in another sense and you've got this first class um uh property so i think interfaces are probably the the right way to um to do abstraction in address probably uh ringer rather than just having things separated by namespace but um we haven't really played enough yet with what they can do so yeah the short answer to that is no no but thank you we have two more questions right now um do you have time for two more yeah yeah i mean i still got this left oh great great okay so these will maybe these will be the last one oh still i i'm i'm too slow a drinker for this now it's even warmer so sell a temperature that's what you want both of the questions are from uh an andreas but they're two different andreas so first of all and they both have mics so they can unmute and ask their questions so first uh i hope i don't mispronounce their names andreas euler it's good it's good no okay so i asked may idris contribute some notion of equality as far as i have understood in haskell we don't have a class of equality for functions itself and it's interested to reason about functions if they are equal or not can it just provide something in this direction um [Music] yeah not really um so this this this question opens a whole can of worms so the question of equality and how to represent it there's a if you go through a tight theory conference the way to start an argument is is to ask a question more or less you know like the one you've just asked what does it mean for things to be equal so um so there is a there is an equality type so we it did come up in passing uh when i did the rle because i wanted to have proofs of um in order to have a proof of soundness of um of the wrong length encoding compression i needed to have a proof of uh so you don't see that explicitly but you need to have a proof that the things truly are equal so that works fine for um you know any any value that you can compute but as far as functions go so it's only sort of intentional equality it's only it's only about equality of definition of the function so you're not going to be able to let's say prove that two functions if two functions always produce the same output for the same input then those two functions are equal that would be nice to have so we don't have it in the in the type theory uh behind idris which by the way um disproves my one true core language thing so uh it's not a pity so we could extend it in various ways so um we could go to observational type theory uh which says a bit more about equality of functions we could go through homosophy type theory about which i know almost nothing um so there's all sorts of um other ways of representing equality that we could have but don't that's that's really a question that i've left for um people who are much more knowledgeable about that sort of thing i guess it's an example of you know if if someone comes along and wants to investigate better ways of representing equality and ideas i'd love to hear from them uh help them along so we can't do an awful lot more than what you what you could do in high school i i just took part at some round about a category theory and there was a programmer who used idris to to answer some questions or to reflect things okay yeah i mean so for um you you can certainly do equality proofs like that that are you can do to proof of the quality of all kinds of interesting things but you can't do proof of equality of every interesting thing that you might want to so like you start running into trouble when you try to prove things about higher order structures for example so um but i mean my my goal here is is whenever you if we if we think of the overall philosophy about uh being about how do we make um uh software the correct software cheaper to produce then maybe we can get away without worrying too much about proofs so the the thought of proofs we have to do tend to be a bit simpler i i do a lot of i i end up having to use a lot of proofs about you know associativity of uh of appending lists that sort of thing these things do naturally come up in practice but um maybe not so much the equality complex properties of complex functions yeah much as i'd like to be able to say it's possible to do that at a minute it's not thank you so our next andreas is andreas bernstein els braunschweig yeah um hi hi um i have an implementation question you said that the language core is permanent right so a list of names so i'm curious uh how this list is then used uh local variables indexing and that is how does it work right um so uh is it a good idea to show you this um oh yeah i pretty bad enough it'll get too deep because i'll just i'll try to explain in words rather than showing you the type um firstly i'll say i'm gonna go into this in in in huge depths in this summer school that i talked about which uh will be recorded so you'll see this in much more depth in a few weeks but for now what we do is local variables are um if you've done any programming any implementation of a functional programming language you've probably encountered the brand indices so the brand index is a representation of variables by um i'm assuming you know this i'm just telling i'll be telling the whole audience rather than any individual but so the brand index is a way of representing variables by counting the number of variables since it was defined so zero is the most recently defined variable one is the next most recent and so on so this is part of why uh scoping becomes a bit of a nightmare when when implementing uh a language particularly one where you have to manipulate terms a lot so we have to do uh evaluation of terms we might have to do substitution into the term um we might have to unify two terms that have uh that have local variables and one might have fewer local variables than the other so we have to make them match up and that involves certain kinds of manipulation and using but so using indices works really nicely for some things not so nicely for others but at the same time you don't want to you don't want to have things represented as just a name because if things are represented as just a name you're going to get clashes because you know you know if if we were all issued at birth with a name supply and they were the only names we were allowed to use when we're writing programs then we might be okay because we wouldn't get any fashions but realistically you know we're functional programmers so we call everything x or a so we can't just use names um people wondering whether that was a joke or not um so you maybe you could decorate the name in various various ways so i've done there's various libraries in haskell probably other languages for helping you deal with this so what i've chosen to do instead with the address 2 implementation is i have a mix of both so it's nice to use names for displaying things to the user it's nice not to have to invent new names unless you really have to so it just one would defensively invent new names just in case and you get some very strange messages sometimes um so we have this mix of the ground in season names where a variable is represented as a pair of a number and a proof that that number represents a specific name in the list of names in the type so at run time all you get is the number you just get that index that tells you how far to count back in the context to find the variable you're looking for this is good news for the evaluator because the evaluator it just has an index it just has to look up at a particular index um and the fact that there's a proof is also good news for the evaluator because it means i'm not going to make a mistake overrun the environment and have a crash um it's also good news for implementing any kind of manipulations that we've got so i like i might need to like when you go when you're traversing a term and you have to go into a binder you encounter a variable sometimes you have to increment the index because you're referring to a variable um before the binder sometimes you have to not increment the index because you're referring to a variable after the binder and i've got that wrong so many times but now the type checker tells me what i have to do so as i'm traversing the term um i come across a local variable it's all right do i do i increment the index here or not well what does the type tell me i have to do to type um i'm basically going to have to write a function that says um that counts if it if it's before the binder increment if it has to divide the dot so um yeah that's that's basically how it's been uh how it's been used so rather than having some library for dealing with names there's some really useful libraries for dealing with names in haskell um in particular so i don't have to do that i just let the type checker um tell me what i need to do i'm also worried answering that sort of question because i i don't quite know what um what technical background the uh the asker has so apologies if i either assume too much or not enough but um um let me know if that helps yeah thank you that was super interesting anyway more on that in the summer school because um it's i mean it's writing these programs with with these proofs is enormously frustrating at times but because you know basically it's not type checking so you can't try it but at least you know once you finally get the program working you know it's going to work so you know we make this joke it type checks ship it well this is a situation in this very small setting this is the situation where that's actually true so uh so thank you um to everyone named andreas for your questions and i was going to cut it off there but we actually have one more very nice question which i think is a perfect closing question right for the evening so bernt please go ahead and unmute and ask your question which i think we'll all be excited to know the answer to uh hi uh you uh published a few years ago uh type driven development the book and now it's um a lot of changes happened to ios 2 and i want to ask if it's also be published like uh title real world iris 2. uh that'd be nice yeah um so yeah i i i get asked this question in a slightly different form occasionally so i'm gonna ask answer that slightly different question first um so the question is uh should i should i still buy your book now that you've implemented idris ii isn't everything different um and the answer to that is well i've written a page that explains the differences and i think what you should do if you haven't used idris before and and you want to work through the book i would actually recommend for the first maybe four or five chapters just use idris one and and then look at the uh so i i've got this document so i kind of started and a couple of people have helped with uh explaining how to update the examples for interesting but it's true it would be a good idea eventually if um if there was some kind of uh longer term document actually explained the languages i think people should use it so i'm i'm now saying if you're gonna do anything serious with idris don't use idris one anymore um it is two yes the version number does begin with zero but um it's still so much better than idris one it's so much faster it's more robust like yeah okay the error messages are still kind of ropey but then they weren't in just one team now the system isn't as polished as it could be but you know that that that'll improve in time so i think if you're gonna do anything real do you do do it in address two yeah i don't leave a question of you know what's the point in the idris book anymore um so i'd say the the the the the type of development with idris is is was always meant to be about the ideas behind type driven development rather than about idris itself so obviously idris is the language that's being used to introduce the ideas well that's why a lot of the examples are kind of small and we don't really build up to any huge example so yeah that's the answer to the question that uh that is often asked just just to have that on record that uh um you know yes you should still buy it obviously because you know buys me a cup of coffee a month if people died um but you you can still use it with idris too provided that you're willing to um look up what the differences are but i mean your question was more about is there going to be another book that goes a bit further and goes a bit deeper in the the real world um it kind of seems funny to say real world idris kind of kind of strange world that have i wandered into where this happens um but uh i think that there could be a place for that um but it now is not a good time to start working on that kind of a book simply because there's a lot of questions still to be answered in how you even use idris too so so i've learned an awful lot about how to use a zero uh multiplicity i've learned a little bit about how to use the one multiplicity but um i've given a few talks about idris ii over the last year or so and i think in every one i've been using linearity in a different way and what you can take from that is i don't actually know how to use linearity best yet so i don't think it's a good idea to write anything down until we've all figured that out uh but i'd also say you know i don't have a monopoly on writing books about idris any anyone can have a crack at it and i'm willing to help anyone who wants to write some more detailed documentation i've done that i'm not doing that again but uh maybe one day yeah there is a place for such a book but not quite yet well edwin you've been exceedingly generous with your time and i feel like we're uh privileged to have you join us rather later than i thought and the problem is once i started talking about this i start getting too enthusiastic so you know for fortunate for fortunate for us uh we can't offer you a proper round of applause but people have been uh dropping um a lot of plaudits into the chat and i can at least wave my hands at you my thanks for your time and uh and your generosity and joining us virtually i hope you can come to berlin look us up if you do at some point in the future when all of this is over so do i and um yeah i really mean it when i say berlin is one of my favorite cities i i would love to come back and i i was supposed to be there a couple of weeks ago um for um e-coupe but sadly sadly not yeah well in person at some point yeah it's a shame uh but at least we have this opportunity which we wouldn't have had otherwise so i'm looking for the the silver lining that's what this meetup is a kind of silver lining and uh in an otherwise dark time and uh and you've been a light for us seriously this has been great uh it's not often that you get to learn about a programming language from its creator well thanks very much for having me so uh i guess everyone is if you want to look at the chat you can see everyone saying goodbye and i'm going to stop the video and i'll if anybody wants to unmute after i stop um recording then feel free to do that and thank you again edwin okay thanks very much bye everyone

Channel: Berlin Functional Programming Group

Views: 4,601

Rating: 4.9083967 out of 5

Keywords:

Id: nbClauMCeds

Length: 128min 34sec (7714 seconds)

Published: Wed Jul 29 2020