Constraints Liberate, Liberties Constrain

transcript

[Music] I want to start kick off this conference by by talking to you about this sort of uh rather counter-intuitive thing which is sort of this this tension that I think exists between expressive power on one hand and analytical power on the other hand and as you sort of expand one of those things you necessarily contract the other so as a as a wee young Runar I was programming in Delphi on on Windows anybody any Delphi programmers in here yeah all right so don't you know why object Pascal didn't take over the world I will never know but um so yeah I was you know programming in Delphi on Windows and uh I was working for a publisher of poetry of all things and uh and this is the first program I ever sold to anybody um and so one of the things that this thing needs to do was to print out sales reports for the publisher and I needed to do that on this beautiful piece of Machinery right here now unfortunately at that time Delphi did not have very good facilities for printing so I did what any you know any hacker would do I got out the the star dot matrix printer reference manual and I just took their SQL tables and I turned it directly into printer control codes over the parallel port now of course once you've printed something on the

paper you know it's on the paper and there's there's nothing you can do so then the client comes back and says hey these reports look great but you know I got a new printer so you know can I can I print this out on my new printer and I had to say no uh and then they asked well I'd like to take you know this report over here and this other report over here and then sort of put them together side by side on one sheet of paper can you do that and I have to say no um so so about going directly to the sort of full power of the parental control code by like having complete control over the printer you know I I wasn't making making use of any kind of abstraction that would allow me to sort of you know abstract over the over the printing so what I should have been doing was to generate some kind of intermediate form that allows for composition you know some kind of syntax tree or something that I could then you know go and render out to the to the printer as sort of the last possible step so that's some other point uh I was working with strings that that rather uh looked like this so uh some strings that contain some SQL right so it's you know select some stuff from some table where some condition is true uh now the problem with with this is that it's a string right so the the structure of the SQL in here is sort of lost inside of this string so if you want to do something like add a column or add a condition or something uh that's actually really difficult to do because you know you have to sort of

ReDiscover what it is that the structure of the string actually is or you know you have to do some horrible hack which you know I've done a lot of so again what I needed here was an abstract representation some kind of intermediate form that I can then manipulate and then at the last possible moment when I'm really sure that I don't want to manipulate it any further I compile that to a string and then I send that to uh to the database right so maybe sort of what I was discovering was this principle that any problem can be solved by just adding another layer of indirection uh and so David wheeler here is a little bit uh tongue-in-cheek about this but it makes a good point about abstraction and composition so as an illustration when uh when we're working with explosions as you do you want to work with a representation like this right so you want to work with the unexploded form right you want you want to well be you know because it's compositional for one thing like you can take two blocks of of TNT in Minecraft and and you can put them together right to make a larger explosion um and then you know just like when we're working with side effects in our in our programs you know we want to work with them also in the sort of unexploded form we do not want to work with them in this form right so so whenever I see side effects in in code you know this is what I want

to think of it's just think of explosions going off everywhere so so yeah once you've sort of detonated your Dynamite or your side effects uh composition is is out the window and when we're working with explosives we really want you know that extra level of indirection so I think that this is a mistake that a lot of people make I know that you know I make this mistake a lot and it's a mistake that's really easy to make which is uh choosing to work in a language that is sort of too large for the task at hand it's insufficiently abstract and insufficiently uh precise and so we tend to optimize for for the task at hand for the thing that we're working on right now and uh and forget to optimize for the task that's down the line which is integrating our uh our code into a larger system or a larger conceptual framework so go into a concrete representation of what we're working on sort of too early and this comes up in all kinds of situations and not just with side effects for example in this very simple geometry problem uh let's say we want to find the area of the yellow square right really simple we know that this red triangle is a right triangle and we know the two sides that they're both two so you know we know our Pythagoras and we just say like well you know 2 squared plus 2 squared is 4 is 8 and then we

take the square root of eight and we get something like 2.828 something right and we you know obviously turn that into a double and then we square that right so when we square that we end up with something like eight so not exactly eight so so what has happened here is is that you know we've sort of detonated our our square root too early you know we've lost Precision we've gone to a representation uh that is sort of insufficiently uh precise and uh and it doesn't allow for this kind of compositional reasoning right so we've we've sort of created when we take the square root and go to doubles we created this barrier that this allows further uh composition and something has been lost here more than just the the sort of precision of the answer what has been lost is the algebraic relationship between these squares because the Pythagorean theorem is really about the relationship between three squares that all lie on a triangle like this and the relationship is that you know the area of the square that's on the patent hypotenuse is the sum of the areas of the other two squares right so hopefully you can see the analogy here between this and and side effects so we're using side effects is like working with you know distances and doubles and using algebraic data types and pure functions is rather like working with you know the algebraic relationships between uh squares

so the moral of the story in in this case is that you want to work symbolically right you want you want to manipulate symbols for as long as you can and then sort of detonate to decimals or to some kind of representation that is uh uh larger or sort of uh like they could mean more possible things as the last possible step so yeah this kind of problem of uh of having concretized too early comes up in situations that are much closer to our hearts right as scholar programmers for example the problem of binary compatibility so binary compatibility comes up because of this kind of problem of having gone to a binary representation sort of too early so when the scholar compiler goes in and generates a binary from a Scala file you know it's it creates this intermediate form this kind of tree like the syntax tree of the Scala and then it goes and throws that away right and just leaves the the binary for you to then consume to construct further code right so then you write some more code and that consumes the sort of the library that you had just compiled before but now what you're consuming is a binary and the binary representation is sort of strictly larger and less precise than what you want right so we've we've sort of you know done the same thing as when we like took the square root and went to doubles

um we have thrown away this abstract relationship between uh entities in Scala and so then when we try to combine that with other things you know what we're thinking about is combining trees but what we're doing actually is trying to recover uh sort of hypothetically the idea of the tree from the binary which may or may not represent that actual tree because we may have done things like oh gone to a different version of that library or gone to a different version of Scala C altogether a partial solution to to this that Martin odersky and others are working on is this idea of shipping the abstract syntax tree along with the bytecode so and they're calling this tasty trees which I think is kind of an awesome name uh and so yeah the reason here is that you know the byte code representation is sort of too large and and it's a barrier to composition and reasoning and so not throwing away that absolute representation uh helps or is going to help enormously I so the moral of the story here is that you know we want to work with syntax trees for as long as we can we want to work symbolically and then we want to go to binaries as late as possible we want to compile as the last possible step because really uh compilation when you really think about it is is an optimization step like you really only need to do it when you want the thing you know to run quickly on the machine and as we know parameter optimization is

the root of all evil but uh more than that I want to say that that's really just a special case of something else that the the root of at least sort of a moderate amount of evil is uh premature loss of precision or compilation or folding or going too early to a uh too concrete or two large representation so to a representation that is sort of too unconstrained and too powerful right and this is uh sort of a classic mistake or a classic error I think that is really easy to to make and it's not just something that beginners do I think experts make this mistake all the time uh for example if you open up any uh calculus text you'll see that they go directly for the most powerful number system they could possibly think of like everything that could possibly have uh everything that they they might possibly need all right and it's easy to think I mean it's interesting to to think about uh what kind of structure we're missing out on what kind of reasoning we could possibly be doing sort of within calculus if we you know restricted ourselves to maybe something slightly smaller than a number system that includes you know uncountable reels and non-computable numbers and and things like that and I want to say that this is sort of the same phenomenon as doing extremely

type programming uh where you know like with SQL where you know I have just a string that represents whatever I'm working on because you can always represent anything as a string right so why not just work with strings well because you know then you have to ReDiscover what is the the structure of the of the string and I want to say that reaching too early for things like General recursion and reaching for languages that have side effects are also a species of this same kind of thing so because you know when we're doing these things uh when we're when we're coding you know we should ask ourselves like do we really need General recursion do we need really need to go to a string here do I really need a side effect here and what am I missing out on well the fact is that the more expressive something some language can be the sort of larger it is the less we can analyze what we have expressed in that language because the more kinds of things something could potentially be the less we can actually reason about what it is like what it actually is right so you know as as the potential stuff gets larger they you know this sort of a number of things that could that we could actually sort of predict about it uh is is smaller so my point is here that we want to choose representations that are sufficiently abstract uh or you know sufficiently indirect because abstraction buys you this

compositionality and and failing to be abstract enough creates this barrier uh so you detonate sort of too early but abstraction also buys you precision and uh now many people might think that abstraction and precision are opposites but they're not in fact I want to say that abstraction is what makes Precision possible in the words of escrow Dykstra the purpose of abstraction is not to be vague but to create a new semantic level in which one can be absolutely precise and to demonstrate that in a very simple way here is a a signature that is not very abstract so uh if you ask yourself how many implementations exist of this type like a lot right it's something like 4 billion to the to the four billionth power and and you know that's a huge number and that's not even counting the ways that you could do side effects and throw exceptions and you know involve nulls and absurdities and things like that in in a program that meets this type signature but if we allow the uh the type to vary that is if we abstract over the type so this type signature you know is is sort of the same as before that it's you know it's a function from one type to another except now the type has been abstracted out so now how many implementations exist for this signature one right well

there's only one that actually you know makes sense you know without side effects and without nulls and so if we don't appeal to to those kinds of things but there's only one way that you could take a value of type A for any type A and then return a value of type A for that same type A you have to return the value that you were given right so here in allowing the type to vary we've introduced a freedom to the caller yeah so they can choose any type but this Freedom constrains the implementation yeah and that in turn introduces a Precision because this type specifies precisely what this function is and this is very sort of counterintuitive that you know making something more abstract is making it more precise that you know making something freely vary then creates a constraint um but I want to I want to say that sort of in general that for you know if you introduce a freedom at one level then that leads to restriction sort of further down the line at a different level and this works the other way around that if you constrain something sort of Upstream then that leads to freedom and power further down the line because now you can you know once things once something is very constrained you can now reason more about what that could possibly be

okay so let's take some examples for example monads versus applicatives to give you a quick sort of refresher on on monads and applicatives so a functor is just something that you can map over right it's some data type f for which there exists a map right so you if you have a function from A to B you can get a function from F of a to f b for this data type f for example if f is a list then you know you can map over the list with a function that takes all the changes the elements to some other type all right um now applicative functors are functor so you can map over but they come with these additional capabilities uh the capability that you can take any value and sort of put it inside of the context for example you can with with a list you can take an element and you can put it inside of a single element list and then the other capability of applicative functors is that if you have two of them if you have an F of a and an F B sort of side by side you can put them together and you can do so only if you have a function where you can combine the elements right the the A's and B's in those two f f a and F of B if you can combine them into C's then you can combine the F of a and F of B into a combined F of C all right so you can sort of sum them yeah or multiply them uh

and then an applicative functor that comes with one additional capability is a Monet so a Monet is is an applicative functor that has this additional method join where we can if we have a nested F if we have an F of f of a then we can turn that into an F of a for example uh I'm gonna go go on with the lists if if you have a nested list of lists then you can concatenate all those lists into a single list if you have you know a three with threes you can graft all the trees into the nodes of the tree and you have a sort of a flatter tree if you have an option of option you know you can collapse those things together right and this allows us to do you know it allows us to write flat map so flat map is is map then join and then you know it allows us to use four comprehensions and so it allows us to assign to variables and then use those variables later on in our sort of nested in the inner context but uh in doing so something is lost and when we go from applicative functors to monads we we gain this additional capability of joining and flat mapping but we lose something as well we lose the ability to mechanically compose these things so if you have sort of two data types or two languages or you know two two applicative functors f and g uh you can always mechanically compose them into a composite functor FG

so for example you know if you have a list of options you can you know map over both of those structures at the same time and you know you can combine two maps of options or list of options or whatever and combine them together using the applicative uh and coming up with an applicative instance for the composite is completely mechanical and can be done once and for all and the implementation is is really really simple all right it's just like you know for the pure thing just lift the pure thing and you know literally just compose the appears and with map too uh it's literally just composed the two twos all right but if we want to do this with monads this is not possible in a mechanical way composition of monads requires a mechanism that is specific to the monads that are being composed so we need to know something extra we need some additional information about the individual monads in order to be able to compose them and this is why we need things like Monet Transformers uh I want to say that uh this this applies to Monas that you want to compose in this particular way you might be able to you can use things like code products and other things to compose monads in other ways but if you want to uh you know if you have two monads f and g and you want the monad FG uh then you may be able to get it but you cannot get it in a completely mechanical once and for all way all right so this is an example of where

something is strictly more powerful than another thing but then is less compositional right right we lose some kind of composition so monads offer more uh for the first order like we can we can take a moment we can immediately do more stuff but amona can participate in fewer applications right it can participate in fewer compositions of things yeah so I can I can participate in fewer systems of solutions if you want so again this is an example where a constraint at one level we constrain ourselves to applicative functors and this creates a freedom or power at a higher level in the at the level of composing systems all right another example of this is uh actors versus Futures and I kind of wanted to put in a little parenthesis like fight right um so so Futures are more constrained than actors in the sense that they have an algebra uh so you can do sort of algebraic reasoning with with futures uh so for example if you have something like a monadic future you can do uh things like Fork you know you can take an a you can create a future a uh you can map you know you so if you have a function from A to B and you have a future of a you can extend that future just by sort of appending that function and say Hey you know once you're done with this do this other thing as well and then you can join that as you can

tell if you have you know a process that spawns some sub processes you can ask that process to sort of wait on its child processes and this all sort of behaves according to the monad laws and so that fact gives us the power to use this with Magnetic libraries and to reason about it as a monad right and so that gives us this algebraic reasoning now contrast that to uh you know a type like this right so this is the type that that actors are in akka at least are built around so this is you know a function from any to unit and so this is completely unconstrained right uh so you start with you know anything you could you could receive a value of any type whatsoever uh you don't know up front what this what this could be uh and then it just returns a unit and even that is not really true what it does is not return a unit it actually goes and has a side effect right so it'll you know the type of this is even bigger than this right right um so so there's no algebraic uh theory about this type right there's there's no way we can sort of reason about this algebraically um and the the this is aggravated by the fact that not only can the actor at any you know can the actor be anything like you know the thing that's behind the

signature any two unit could be anything it can become something else like between calls to to the function right so if somebody has called become an unbecome like between two calls of your of your function it could be doing uh strictly different things so uh I was given I was given a talk uh at one point about you know Scala concurrency and somebody said well why would you not want to do this right well you know if I if I can have this power you know obviously you know AKA actors are are more powerful than Futures why would I ever want to use Futures because I can do strictly more with Arc actors well precisely because you can do more with AKA actors you should want to rather use futures because uh you know they're more constrained and that makes because they're very unconstrained that makes our actors hard to to reason about right so not only can it be anything at all it can become something else between calls so to take an extreme example um or sort of actors are sort of the the extreme example right they're really really powerful right you can do you know it's it's unconstrained side effects right you can do anything you want when somebody calls your uh your actor but uh precisely because they're so powerful a reason about programs is severely limited right because you know like the right honorable John Dahlberg

Lord Acton once said uh Power tends to corrupt an absolute power corrupts absolutely now he was obviously talking about political power but in in the case of side effects uh what is corrupted is our ability to analyze and compose uh for example if you consider this simple kind of equation right so I'm going to stop picking on actors for now but if you consider this kind of equation uh where we want to say that oh if you have a list called x's and you map over that by subtracting some number n and then you map over it again and you want to add another number n um shouldn't that be the same list that you started with yeah make sense but what if n has a side effect right so if n has a side effect and this is clearly not going to be the same right n could throw an exception it could be null so X's could actually just be you know a list and then you know this other expression could be a throwing an all pointer exception uh so in the presence of exceptions and side effects and general recursion we don't actually know this to be true like we don't know that mapping over a list twice and sort of doing inverses or something that should or should obviously work we don't know that it does but if we restrict ourselves to Total pure functions we actually can do this

sort of reasoning all right so this is an example of where a constraint at one level affords us improved reasoning at a higher level so uh you don't want to pick on actors and side effects too much you know I have a I have sort of a larger a larger point but but the the cost of side effects which is just one of these examples is that we lose uh the ability to reason in this way we lose you know compositionality we at least elude the ability to reason uh modularly modularly about concurrency and about parametricity and other things like that right so our programs can do strictly more things if we have side effects but we can conclude strictly fewer things about them all right so let's go now to another example of this principle outside of programming so enough about side effects um I want to talk about where this comes up in information security so in information security there's this principle called the principle of least privilege which says states that a user a program or component should have exactly as much Authority as necessary but no more right so no why no more well because uh if you minimize the Privileges that a particular component can have then you maximize uh the the ability of composing that component with other things right because a composite system requires the

largest privileges of all of its compo of its components it requires the max right so if you have a composite component you just find the one that needs the most privileges you know the sum of all the Privileges is what is required by the composite but the fewer the Privileges a component needs the easier it is to deploy in a large environment and then modularity is maximized as well by minimizing privileges because uh we know that the interaction of that component is limited and we know we can reason sort of mechanically about where that interaction actually happens and so we have overall sort of better guarantees about system stability and uh and it's also easier to test our limited components in isolation all right so another example of where the more A system can do the lesser we can predict what it will do yeah and this kind of relationship and it comes up in all kinds of things for example you know with applicatives and monads with side effects versus algebraic reasoning uh and in context-free versus regular grammars for example if we have two regular grammars we can we can mechanically check whether they are equal we can check whether they describe the same set of strings but if we go to context-free grammars which are strictly more powerful we cannot conclude this right there's no known algorithm that

will tell us whether to concrete context suite grammars are in general the same euclidean versus Cartesian geometry right so if you start you know if you start with euclidean geometry like all space is isotropic right all the directions are the same space is the same everywhere all the dimensions are compatible all curves if they look like they intersect they actually do but if we constrain ourselves to coordinates if we constrain ourselves you know to the sort of Cartesian plane um then uh you know we gain algebraic reasoning we gain the ability to reason about geometry algebraically and we can reach for things like you know linear algebra and category Theory and other things to inform our our reasoning so another an example of where a constraint creates a freedom or power and you know things like roadways uh you know the fact that you can't just like derive uh you know or the fact that you choose not to drive you know from your hotel directly to the conference venue just like over the hills right it and you drive on the road it gets you to the conference more safely and more quickly and and uh and it's compositional because you know you can get a lot more people you can get a whole bunch of people uh very safely along the road uh and very quickly and you know things like commodity components like if you have uh you're building some kind of service and you want to be able to reason about you know you want to buy

like a Linux server that it has like these specific sets of components and so they're all interchangeable the system is compositional it's like you know uh going to your wardrobe and you only have one set of clothes like you know lots of lots of instances of the same set of clothes you know you can the reason compositionally about your wardrobe and you know you never have to worry like when you get up in the morning like oh what should I what should I wear right you just like put something on and you don't have to worry about it and you know other things like you know like putting together Legos uh they they fit together in a very obvious way uh rather than like building something out of like actual concrete and steel uh and you know Tony Hawk pro skater versus actual skateboarding and things like that like obviously Tony Hawk Pro Skater is easier to do than actual skateboarding because you're sort of on Rails right so all of these things have in common that a restriction at one semantic level translates to freedom and power at another semantic level all right so if you make something maximally general for the first hour application you reach for the most power that you can when you're building you know the immediate thing then you minimize your possibilities for composition and for reasoning about higher order applications and it's it's important to go not to go too powerful too quickly because if you constrain yourself to a small language you can always embed that language in a

larger one later on right you can always take your small language and then just translate it to a larger one that fits both what you were saying and also a whole bunch of other stuff that you that you might want to say in the future but this does not work the other way around right you cannot uh you know take a a large abstraction and sort of fit it into a smaller one right uh when you when you do that you get what people call a leaky abstraction right you you have there's certainly more stuff that you need to be able to say than you can fit in the uh in the language that you're that you're actually using right I mean it's like when you detonate your your Dynamite right it's really difficult to to then take the explosion and sort of put it back in yeah it might take a while so another way of putting this is that the more capable your syntax is the fewer sort of logical semantics you might be able to choose for that syntax in the words of uh William lavier syntax and semantics are a joint right um so what does that mean what what does it mean for syntax and semantics to be a joint well it means you know something very similar to what what uh we've just been talking about so let's uh you know let's do a little game where uh let's consider a category C of all the concrete things in this room uh or actually of con of groupings of concrete things in this room right so

for example an element in the category C might be like those two seats over there or you know Dean and miles and one other person or something right so you know so so these are concrete groupings of things this is the category C and we want to say that there's a partial order for this uh for this category that is there's an arrow from A to B uh when B is a subset of a right so so when B is a smaller or it's contained in the grouping a you know for example you know those two seats over there are contained in all in the group of all the seeds right uh and then we have this other category which is ways of describing those things you know for example we might say uh like seat or chair or something um and that you know would be a way of describing some objects in this room uh or people right uh that might be another way of describing some objects in this room yeah and so and then we have a partial order for this category as well that is we want to say that there's an arrow from A to B from the concept or the the description a to the description B when B is a more specific description than a for example uh you know if you have something like uh thing or let's say furniture and then that is strictly larger a less specific

thing than saying like you know Auditorium seat right okay simple enough so now we have a functor from C to D which is a mapping that takes a concrete group of things in this room and then finds the most specific description in our Arsenal that that fits that group of concrete things right so for example you know if we have those two seats over there we might want to uh map that to like the most specific description with my which might be it might be seat or we might have something like a red seat right it depends on on what our descriptions uh contain but the important thing is that F will find the most specific description that we have available for that group of copied things and then there's a functor that goes the other way which given a description um D or a description in D it will find the most generous group or the most capable group of elements that all match that description right so for example if I say seat and then I apply G to that I want to get like all the seats in here yeah so uh you might say that g sort of sort of or F it will create a generalization for something and then G will forget that generalization and go to the sort of the canonical example of that generalization so this obeys this kind of relationship

where if we have some grouping a some group of concrete things a and then we find the best available description of that grouping so that would be F of a and then we want to go back to concretes we will end up as something that may be larger that is the best available description of some concrete group May apply to a larger concrete thing right so for example those two seats over there I might you know go to seat but then when I go back from seat to the room I will get all the seats right so that's the the lower one uh and and the upper one goes the other way where if I get the most generous group described by some concept B that group May in fact be described by a more specific there may be a better fit for describing that right that larger I mean that concrete grouping okay so there's this sort of relationship that goes in both ways so the important thing here is that as we go from smaller concrete groupings to larger ones we get strictly more objects right that is the the set is more capable yeah so but the number of possible characterizations of that set gets smaller

that is uh we can sort of reason less about that set uh where the the most specific characterization will actually get less specific as we grow the set of concrete things that we want to describe right so for example you know like a a group of two seats uh that might be best to characterized as seat right but if we go from a group of two seats two you know two seats and and you know miles um you know though you know that group is more capable right like two seats and miles are more capable than just two seats you know we would like to think anyway so we can do strictly more things with those right but they're harder to summarize right what because what do miles and two seats have in common right that might be it might be difficult to come up with sort of a very precise uh generalization of that right uh and also if we find you know some generalization and then we go back to the room we may not find miles in two seats again we might find a group that is much much larger than that because that concept will apply to a number of number of other things yeah so this kind of thing this kind of a relationship is uh is called the galwa connection uh after uh Everest gawa a French mathematician and there's a specific kind of a junction we were talking about how syntax and

semantics are a joint so you can see that these two categories c and d right where we have we have Maps between them they're sort of mirror images of each other in a sense so there's a one-to-one correspondence between two partial orders uh in a very precise sense uh and uh the the sort of relationship that we can uh what what the relationship that we were describing previously what it sort of means is that the most efficient description of any concrete group a uh will be less specific than any description B precisely when uh this is that green thing so precisely when a is smaller than the largest group largest grouping described by B right so uh we can go so instead of instead of considering just functors between categories of you know sets of objects and and descriptions we can generalize this to any category and since we can generalize to any category that's just pick the Scala category right so we can say the same kind of thing about at Junctions in Scala right so f and g are then just ordinary Scala functors and then there's a one to one correspondence between these arrows right if that is you can if you could go from F of a to B then you can go from a to G of B and vice versa right

so you know that's all very sort of abstract but let's uh let's say that in Scala code so we can write a trait like this a junction uh where we can give an example of an adjunction between two Scala functors so f and g are functors and then we can say that well we have to implement two methods one of them takes arrows from F of a to B and gives you an arrow from a to G of B and the other one goes the other way that is it takes hours from a to G of B and it gives you an F of F of a m and the sort of canonical example of this in Scala is the adjunction between uh sort of the Tuple functor and the and arrow and the reader functor right so uh well between producers and consumers you could say so here uh you can see that this Junction is witnessed by currying and uncurrying right so F in the in the sort of in the abstract is now in the concrete a pair with r right and G is uh now in the concrete a function that receives R right so then we can we can show that this relationship holds because we if we have an arrow from A and R to B then we can construct an arrow from a to R to B right and that is just Curry and then if we can go the other way and that is just uncurring

so what I want to draw your attention to is that these two types pair with r and function with r they sort of fit together right you can feed one from the other and as the producer the pair becomes more capable the corresponding consumer has to become more capable as well yeah so a freedom in the producer becomes a constraint on the consumer and if we make the producer less capable it becomes compatible with strictly more consumers that is a constraint becomes a freedom and this is important because most software that we write are consumers most of the software that we well at least I hope that most of the software that we write is going to be integrating some systems it's going to be abstracting over something that has been you know some kind of concrete stuff or or something right so most software that we write is going to consume some things so most of the software we write we have not yet written and we're going to consume the software we're writing today in that software so it's very important I think to constrain for the first order application to allow ourselves a freedom and power at the higher order um and so yeah we could tie this into into variance right so the Tuple uh type has R in the covariant position but then it's uh in the contravariant position in the function type right so as R grows in in one uh it contracts in the other

okay so the the other sort of canonical uh a junction we can talk about is the junction between free and forgetful functors so free as in free monads and free monoids so a list is a is a free monoid and that a junction if we take lists for for example that a junction is witnessed by the fact uh well so the left side of the adjunction the free side is witnessed by the constructors of the list data type and the other side is witnessed by fold left and fold right so it's saying that there is uh an adjunction really between data types and then let's be doing the constructors of the data type and then the algebras that we can use to deconstruct those data types right so the producers of the thing of the data and the consumers of the data yeah so I want to summarize here and say that when we you know when we're writing software we want to reach for the least powerful and most precise abstraction that we can the thing that will allow us to say exactly what we mean and no more and then you know we want to want to sort of build that and then we want to detonate that as late as possible and turn it into a sort of more powerful larger language and sort of Let It Escape right at the last possible moment because once it's out we can't put it back in right we're now in a larger language and I want to say that this this kind of

premature loss of precision or loss of uh loss of abstraction is uh you know is the root of all evil in the in the Donald knuth sense that it it creates a lot of problems for us down the line that we then have to go uh and fix like it's a creator of technical debt so yeah a constraint at one level leads to freedom and power at another level and for that reason we want to plan ahead when we are when we're building something we want to up you know know that we are going to want to integrate this into a larger system so plan for that plan for algebraic properties and compositionality and don't always just reach for the for the most uh expressive thing that you could the thing that will do everything that you might possibly need because then you know you might paint yourself into a into a corner uh and that's all I have thank you [Applause] now do I have time for questions one okay okay what is the question uh can you just answer that because we have oh we we I we may have to abandon this already because so people set the Wi-Fi okay has anyone anyone's found that

okay so uh in future shout out questions if if speakers can repeat the question that's good for the video okay uh only one question Daniel do you have a question oh yes you do okay bought if there's any oh the question is whether I thought of whether there's a correlation between this and scholomization that is the relationship between existential and Universal quantifiers uh the answer is I haven't thought of that so lots of other people have thought of that and there definitely is an adjunction between existentials and universals so that is exactly and it's it's in fact one of the canonical examples of this kind of relationship [Applause] [Music]