Scale By The Bay 2018 Unconference: Greg Pfeil

Scale By The Bay 2018 Unconference: Greg Pfeil

Recording: Scale By The Bay 2018 Unconference: Greg Pfeil

so hi I'm Greg I work at a company called formation we do a lot of fun stuff that I'd be happy to talk to people about we're always hiring and this is not really stuff we use we use doll but the stuff I'm going to be talking about here is kind of what I do in my free time with it just not stuff we do it work with it just to be very clear so who's aware of doll like who knows the name even okay it's good pretty good and has anyone like used it or or familiar with at least its syntax or anything like that okay so doll is intended to be a oh I didn't actually start recording apparently I have to click it one time there we go this is now the beginning so doll is intended to be a configuration language replacing things like Jason or or yam all especially things like camel and but it doesn't an interesting way in trying to be a total functional programming language it kind of avoids the you know the the Turing tarpit of a configuration language getting more and more features until it's just like another programming language with terrible syntax and everything by giving you everything up to that you know just avoiding the Turing completeness and giving you totality and kind of saying like you can do everything you want to do with this this language and it's going to still terminate you're still going to have you know things that you expect out of configuration languages as opposed to like turning complete programming languages but it turns out that you can do in a given a total language you can do anything and so so that's kind of what I try is to see what I can do or like how I have to jump through various hoops to to do things that I find interesting and so this start with like a little overview of like what Dahl is and what it looks like this is a blog post written by a co-worker of mine fintan that kind of gives a good overview of everything else is kind of just to give you some sense of the syntax and things that exist as a handful of native types basically there's no recursion in Dahl but there is a list type that is built-in that gives you some you know some bit of recursion and then to look over some of types this the syntax so this here is running the doll command feeding it some expression that will be normalized by doll right so true and false false pretty straightforward stuff ORS there's natural numbers you can add natural numbers there's integers you cannot add integers integers are basically just opaque data same with floating-point stuff they're just opaque text is almost opaque but you can concatenate it but you can't really do anything else to it lists can be concatenated there's also you can fold over lists as in this example here there's no type inference so as you can see in this list fold what it's saying is like it's going to take a list of boolean and here is the list that is going to fold and then the result is going to be a boolean and then here's the parameters to fold which are the you know and for the operation used on conses and then the nil will be true right so standard fold but again you have to be explicit about your types yes yeah yeah everything basically the function itself needs to know the types and we'll see when we see what functions look like you'll see how that works but we have to be explicit about the types here and then when you pass well you see I guess a function here we can look at it when you pass as a lambda right that we're passing through it takes two arguments and and yeah so a lambda looks like this it actually has a lambda doll auto format your code basically for you I mean doesn't have to but you run doll format and it's very nice it like gives you unicode things and like re indents and aligns everything it's actually been really really nice to like just like write code just without thinking about any kind of structure and when I save it at all like it's nice and pretty fide and like looks correct and I didn't have to do anything to maintain any kind of formatting so that's very nice so yeah so lambdas look like this where you know you have some variable and its type and an arrow and then you know the result of it or the expression you want to evaluate so let's see here so and yeah so there's there's less there optionals unit which is the empty record this is the unit type and this is the unit value records are look like this very similar to Jason except for not using equals it uses a or started not using colons for the values that uses equals that uses colons for the types so this is a record type and and records here's our value of that type oops right here so you can like you know in a very similar way again this difference between colons and equals is there but things that like look fine and Jason can basically be employed almost directly so you can break something looks basically like Jason and treated as doll with that one syntactic thing and it just it just works you can't do a heterogeneous like lists right you can't just like mix things in your list that won't actually be parsed properly let's see so you can project out fields from a record you can project out sub records of a record so there's no row polymorphism you have to be very explicit about that about which which field you you want in which cases and then there's Union types so this is like a some type here where you have the options or Monday Tuesday this is an enumeration right because all of the values so each Union type is a tag in a value and and the value here is all is all unit so this is just a simple enumeration but you can have looks like a so given some like this there we go merge that's what I'm looking for merge is basically how you pattern match basically and what this means is you have de which has been defined at that same kind of this is right this is the type of the Union so it takes a value of that Union type and a a congruent record that basically that means that has an entry for each option right so like for all the different oppas in the in the Union here this record has to have a handler for each of those cases right and so that's how you pattern match it and there's no there's no catch all it just as like 1 2 1 so there's definitely definitely restrictions in this language that you know when you're writing your code day to day like can get in your way or like don't don't give you quick the flexibility or expediency that you want but that's that's not the goal right it's to me it's to basically help reduce duplication and configuration files like and kubernetes configs and stuff like that where you can like define a function here and there and just like eliminate a lot of duplication so it's not trying to just be like you know a super like you know brief or concise some programming language like you know a castle or something which definitely there are things that come up that are very not concise and so so now that we've seen all these kind of things you know here's a kind of our first FP structure we're looking at right is either which is just a union type right where there's it has two type parameters used here a and B to specify what that is and let's actually bring bring that up so look here this is a sly Brera called I'll make the speaker called dal bhat which is one of the two main dal libraries we use at work if you look at the folder names they look maybe familiar and so you can do lots of things in dollars you can see from these things including like we have like con extensions and your Naida yo Naida has been extremely helpful and also pre-written believe it or not as has Co density stuff like that so anyway lots of lots of FP things so we'll just take a quick look at either and and actually kind of it'll give us a little bit thing here so so either has the way that we structure everything is in this kind of way everything about either is in this folder the first thing we'll look at is the type so you'll notice that like there's no names here right like each expression is just its own file and so you just import files to reference that expression and you can do you can do like let bindings within your within your files to give local names but those names don't escape or live outside of that in any way so you know we just refer to either type whenever we want to be either type and so this is just a function it's a little different the other ones because it's parameters are types instead of like bool or whatever right so this take this is a function that takes two types and returns the type that is the left or right of you know what we expect either to be and and yeah it's just this is just a type level function has the same syntax as a value level as a value level function but but it works at the type level and so again we have like lots of things here we have let's look at let's look at functor very quickly the way that we do type classes so there's no implicit and there's no inference on things so we have to pass all of our instances around explicitly like oh here's you know we want to do something with either here's the function instance for either and so here this is the definition of functor right it takes it takes some type some some type level function right from type to type which is what a function is right it expects the type and then gives you back a type so you give list expects the type like int and then gives you back list of int as your thing and so that's you know that's the f it takes here and it returns a record of the operations for that for that type class as we call it here so so we're just doing like kind of you know what you may have heard as you know what Haskell basically does under the hood right is and you know scotland's stuff to where it just kind of passes it handles dictionary passing for you we have to do the explicit dictionary passing and again map is just defined here as this is for all this is and again this is the auto formatting you type the word for all and it substitutes it with the for all symbol one auto formats Gabriel it likes to use Unicode I like the Unicode so I'm happy about that but but yeah so the type here map has a type where it you know takes a some function that takes two types and then takes a function between those two types and returns a function over you know over the new functor right so this is a standard functor that we know and so we can look at it's gonna look at the either functor but I'm gonna bet that that's not actually a useful one because it's going to just refer to oh no it works it does it directly sort of it refers to map right in here this is the implementation basically just import the functor type and the either type and so basically we can now say like given some type a right for the left whatever the left is we can give you a map that maps over the B to C takes a function where B to C and you go from either a B to either a C would be the result type but you know have to specify that because that can be so it's not type inference right it but it can basically identify that type without any additional context it doesn't need to use any contextual stuff so it is not technically inference and then we use this type annotation here it's not necessary but this is you know basically let's let's doll itself verify that we actually followed the contract of what functor is right so like if like it wouldn't be any different if we remove that but this will at least cause doll to error if we didn't actually define map the right way passing in the string we're like okay yeah let's get back to the funder so in the functor so i can find it again so so this is your this is your this f would be like list right so that is that is your function type so it is a function from type to type like it knows what the kind of that type has to be right and these types that are taken in here are just like if you had like if you had a list of string you would pass in like string and then pass int and then like this would be like length or something like that and then so you get a list of the lengths of the strings in the original lists so it doesn't know it doesn't know those kinds and in fact despite despite Dahl being this is something that I can dive into it right now so despite the spite doll being a configuration language it has kind polymorphism and shortly we'll have a full Tower of universes and so not only can we do things like to type but I will just jump into this here there's the same library this is a branch that hasn't been merged yet there's still some some things we're trying to figure out like what's a good way to express but let's just look at functor really quick since we were just looking at functor so this functor is a little different it's a little more to it so first it takes an object of some kind right so the actual parameter you may pass here might be type or it might be type to type things like that right so we now have kind variables and then we have an arrow oops you know from which takes two of those two of those objects and returns a type and now we have another so this this forms a category basically right although we don't have the constraint of the category type class here but we have objects we have arrows are people familiar with the the notion of a category or not who's not familiar anyone okay so so I mean a category is is basically this is a very hand wavy way of saying it but in abstraction over functions where the common category we deal with has objects that are types and the arrows are functions from you know say from int to string or from bool to int or whatever things like that and so this lets us abstract over that in some way saying instead of just having like types and functions we can have like this the the objects in the category be functors like list or option or maybe or whatever and and then the arrows between them would be a natural transformation like from which in cats is called function K which you know takes changes in F of a to a G of a so you can transform that like that constructor as opposed to the underlying proper types and so in this we have this so now that we can deal with kinds in dal we can define you know for some for some objects we can have an arrow again which is like a function in that category and then we define another category here so we have category C and category D and so this has some objects of some kind and then you know arrow functions between things of that kind basically and now we have our functor this is the same one we saw on the other place but now more generic where instead of just being a function from type to type is a function from objects in in category C to objects category D so this is this has changed things in two ways right so like one we can now write not just a regular functor but we can write like func turkey or something which is a functor and the the category of endo functors sorry i didn't mean to say that but but it's a functor so now we can do like yeah so we can do it we can do functors like one level up basically but also we can differ what the input and the output categories are which those are two different things that we couldn't do with the original definition of functor and the generalized version of map looks basically the same but instead of having like just a function from A to B we now say it's some arrow from A to B and then the result is some arrow from F of A to F of B in a different category so let's look at like a definition of this trying to think what a good one is oh actually we'll look at one thing first which is like so the regular function we see in in Scala and Haskell on everything the things called functor is really an endo functor which means it's a functor where the result category is the same as the source category so here that just happens by being so this is referring to the general functor type that we were just looking at the dot dot means the director level up not my favorite thing but this is just the way imports and files work but i but this should give a single object in the single arrow so one category and you're saying here that like the functor has both the same source and destination category so this is just like a type alias saying an endo functor is a functor where both categories are the same right and so let's see other fun let's let's get let's look at actually let's look at categories a little bit since we're kind of talking about that so categories we have simple categories that are just so the simple point is that usually isn't that in there which is just function this category is just it's just a function it something that takes two types and returns a function between those two types or not doesn't return function but the result type is a function between those two types so this is just like carrying the function thing because you can't actually operators are not carry and dull otherwise you could just write this is like just the arrow or something but we have to make it carried but we have other categories that we can play with common categories often called cly's Lee I didn't use those names I still wish you washy about what the right name is I called it star here which is not great because it's not a star category but but the thing is that it's actually broader than just cly's Lee you don't necessarily need mana instance which is what cly's Lee says it's like for something to be truly cly's Lee it needs to be out of mana but anyway this is another category where again we're abstracting over the the category so we have objects and arrows in some category here's the the mana itself which is a you know basically a function from that you can often just think of like object as being type and arrow as being a function and then you can ignore those top parts without abstracting over the category so this could be tight to type if we had an objective a categories here then it takes say two different types and gives you a function back where the result is wrapped in that hem right so now you have a function if you have an arrow a to B but what it really means you have a function from A to M of B and so by abstracting over the category we've managed to make that mana add part of the arrow part of the function part as opposed to part of the either source or destination type that makes makes sense and so that allows us to did you abstract a bunch of things over mana adds basically that that normally would just be regular functions and actually I'll talk about that a bit tomorrow with how you know traditionally like you'll define some function like what's a good case I don't know like like fold R or fold right and they're like fold right M right you end up with like these these duplicate definitions where that the variation is just like oh and I'll do it in a monad when really those aren't actually different things if you can abstract over the category you can define that once and if you specialize it to the category of types you just get fold right and if you specialize it to a class the category you get basically fold right m and so those you know those those things unify and that's kind of the point of doing this kind of categorical abstraction is that unification of you know many disparate things you now have very fewer did you yeah no one has reviewed this this is still on a branch yeah definitely would do it dealing with the kind polymorphism stuff and all the categorical parametric stuff I just was like oh wonder what happens if I do this I wonder if it works if I do this oh this is wearing school and they committed this like so yeah it's very it's very fast and loose on this branch exactly exactly no we'll see this in yeah yeah and so there's there's a bunch of other categories not to go any implementations of all of them but there are the opposite category which so is an act where an arrow from A to B is actually the function from B to a so it reverses so if you're like contravariant functors is a functor from an opposite category to the original category so you get you know if you have a function of meat ax a you can go from F of A to F of B and so it just reverses that and so you can end the way that this works is that I mean this works for any category so it takes an input category and reverses that input category so it's not specialized to functions right it actually takes the category that should take the opposite of as a parameter other categories dagger categories are basically like invariant functors where they're kind of considered categories where there's no direction to the arrows right normally you think of like a function from A to B but in the dagger category any function or any arrow from A to B there also has to be a matching arrow B to a so like isomorphisms basically a category where the arrows are isomorphisms instead of just functions so it removes the directionality from the category and that's how that's how a invariant functor works right you now have a an invariant functor is a functor where you provide it both a function from A to B and a function from B to a and that gives you a function from F of a to F of B so you need both directions and so that's a functor from it from a dagger category to whatever the underlying category is again so all these things can just you know be done in this configuration language because I mean you definitely need this stuff to write your config files but I mean this is so neat like this this language is extremely restrictive right like again it's total the language does not have recursion other than on lists like built into it and like you can't just like you know define in your normal recursive way arbitrary things and so with all this restriction you can just defined all these things and none of these things care about recursion anyway right these are all pretty flat structures well that's category I'll talk about here real quick is a monaural category which isn't actually so this is sort of the same thing it just adds extra structures so basically you know given some objects you have arrows between those objects as we've already been seeing but it adds in a very mano a mano I do you have you know to given two things how do I combine them and and also how do I get a thing out of nothing right like here's some identity object and that's why this is called a minor in my nodal category because you can see here here's a identity which is some object and and there's a product which takes two objects and combines them to give you a new object in that category the most common case of a monoidal category is the cartesian category or on onset where your product is just a tuple and your identity is is the unit type and and so this is a very useful category we'll see in a minute there's also cohesion much less useful but the product is either the product is either right this is very abstract the things and then the identity is void which so this is the empty Union type right all the alternatives this is your alternative so you can ever create a value of that type so now that we know about money our monoidal categories we can look at let's say look at him on oyd so I'm gonna this isn't going to be the most precise description is this big enough for everybody like 3/4 of the way through here so in a monoidal category sorry for a mono I'd this is this is a very abstract mono I'd right this is like given an object in some category which has to be monoidal so it needs that structure of products and identity in the cat Gouri right so this is saying for someone a little category where the objects are you know whatever this object is you have an object which has identity which your this is doing is extracting the identity and arrow things out of the out of that model category structure I'd shown before right so now you have an add an arrow from the identity thing which is say in the case of set unit 2 and M so basically looks like give me the default or you know identity M you know empty lists or yeah empty lists or or 0 for you know addition stuff like that and then it combines it with semigroup this is this is a type this is the record combiner the type record type combiner really this double double triangle sort of thing and so this takes this field or this record and combines it with whatever record comes out of this which is the you know combat combined or append operation inside me group but I won't get into that but but anyway you can see that you can define a mono a if you have if you have this this monoidal in a monoidal category and so using that we can do all the usual fun things like here is a may be familiar with this one a mono mono ad is a mono I'd in the category of endo functors right so so this is Aman ad you can kind of ignore the first part this F is really you know that's that is your Montague so might be like list or whatever and here you're just specializing mono a here's a mono but you're specializing it to a category where the objects are functors and the arrows between functors are natural transformations and the product is is composition so like F of F of a and the identity is just you know pure basically and so that's you know this this is just implementing rate Amanat is just a mono I'd in the category of endo functors that that incomprehensible statement and it turns out that there's also let's get to it right here this is an applicative is also a mono eight in the category of endo functors the only thing that's different really is that instead of using composition as its product type it uses what's called a convolution which basically looks like what's it called in Scala like lyft - is that that what people call it I don't know so like lyft - where you take like an F of a and F of B and a function from a you know takes a and B and returns you with C that's what they convolution is just like as a abstracted structure is that that thing and so so when you have the convolution of your product you have an applicative instead of a Monahan so again both just mono aids in the category of endo functors and again this is like weird stuff just kind of showing off like what you can do in such a restrictive language other things you get free like like rank n types just fall out of the simplicity of Dahl and it which it has been very helpful for things because you need you don't have existential so if you don't do anything with existential is you need to take advantage of rank end types to be able to kind of emulate I don't know if that's right where existential is using Universal types like for all and so so weak so we can fake existential basically and we do that in a bunch of places actually day convolution might do it let's see uh it's way too deep so day convolution isn't implemented as a left con extension one of those basic types that you know let's see if we can see it in here yeah yeah here so this is an existential so that what this is doing ignoring all that everything else around it is basically this is declaring B as an existential type and the you have to do that right kind of like wrapping it in an additional function that takes some result type that given a function that takes a be like you can like fill this up so this basically inverts the the for all into an exists but it's super ugly right like this whole thing should be like this very tiny not very tiny I guess it should just be like this this part pretty much but like with an exists or something but we can't do that that doesn't exist in doll so you get very ugly stuff dealing with existential x' but yeah so this is one of the two libraries we use and again it gives you like like everything you see and you know in cats and stuff like that and just and in very abstract ways right where you actual get kind polymorphism on like everything and indifferent you know category power Metro City which has been I mean it's been really cool to be able to like to find things like my dad's in such a you know like an abstract way and just say I get to mana wait didn't this in this way we use another library I mentioned that doll doesn't have any recursion thankfully that is like a specialty of mine so we've heard another library called Dada kind of referring to the Dadaist art movement because it is just insane that you would need to do this but there's no recursion so you can still define recursive data types using fixed point operator recursion schemes is anybody familiar with recursion schemes who's here but what they allow you to do is basically encode recursion as long as you have higher-order functions basically you can encode recursion without actually having recursion provided to you and and the nice thing though is the recursion you get out of this is total right like if you use this particular type mu which we don't really have to read about what it is but if you use this to give you your recursion your guarantee that your recursive structures are always finite you know like in Haskell you have this possibility of things can always be infinite because of laziness and but this guarantees that everything will be finite that you deal with and you can still deal with infinite values in a way which this other type which is existential so is ugly it has that same same existential pattern on the bottom line there but but this allows you to create potentially infinite structures by basically just building it as a delayed function that here's the delayed function and then here's like what you would apply to that function and so you can like step through the structure but you can never fully evaluate you can never get dolla to say like just run it to the end cuz that wouldn't be total that would like potentially run forever but you could step through it for some you know fixed number of things or you can just like evaluate to this the final result of your thing and have the interpreter say Haskell if you're using this from Haskell actually do the evaluation but you would know from the type that this is potentially an infinite value and so you now have that that notion of you know partiality of like maybe non termination existing of the type level and it has to exist the type Levellers no way within dahl to erase that so you always have that that promise like we know this will terminate or we can't evaluate it but we can say that this thing might not terminate and this this to has has branched the same way as the other one there's now this whole kind poly category poly metric our parametric version of recursion schemes here where here's your cata morphism given an a which is an object in the category you take an arrow from this is the pattern functor of a if and for people who are familiar with recursion schemes and it gives you an arrow back that folds the whole structure down and again category parametric so now this collapses for people who are familiar with recursion schemes there's like I would say what are called or what I would say is simple recursion schemes and then like there are ones they where they carry type information around that allow you to restrict what types can be used at each step in the recursion and so this collapse is both of those into one into one implementation basically and allows you to again eliminate a lot of codes so we actually use this at work not the kind pile not the kind polymorphic stuff but we do build recursive structures in dal using this to allow us to express some of our configs although most of the complexity is not exposed to the people who are ready Nadella configs yep no-no-no let's see anything is there a particular example or particular thing that yeah yeah okay let's see here so one of the things we use it for and I'm trying to think of a good thing so basically the way that we use is we kind of build up a library of these expressions of these functions so that the the end users just use that library in the end like they're not really using a lot of the stuff they're using things that are like you know more complicated functions that encapsulate a lot information but they don't see those details so I'm trying to think of something that is is a small but see I wonder if we have let's go back to this yeah I don't have a good example for that but there is I'll totally is this the right one I think there's two and one of them is yeah this is the right one so this is this doll kubernetes might have some good examples of things yeah so here here is basically a this is the doll config and it outputs that kubernetes config right so so it already is is wrapping up a bunch of stuff and in a smaller thing right so this is C and this is refer referring to external expressions here like this default and default container here that take these parameters and expand into some you know basically larger thing where it basically just has a bunch of default values for different fields in the communities thing so you can use that repeatedly there's other let's see this one and this uses a lot of let binding right importing lots of different things you can refer to names that one seems like counterproductive right like that's the full kubernetes and the doll is a little bit bigger but anyway it's really good for like when you have kind of many services with a lot of similar configs between them to the once with maybe like a name parameter something like that and just like apply that same function over and over again but this this kubernetes use case is is really useful for because kubernetes can fix can be super hairy and big and it allows you to like pull those into small functions so I definitely recommend like this library I don't recommend the libraries I've been showing you this whole time those are totally just fun and experimental and like see what crazy stuff we can do in a language that is intended to be super restrictive right and that like really you need so little stuff in order to be able to do everything it's kind of crazy that like you can actually you know I mean that's kind of the point is like it's crazy you can do all that stuff in a language that's designed to like you're so restrictive but it but it the restrictions do give you extra promises right if you have this proof this is this promise of totality through the whole thing and it does mean that some things become more complicated to implement or whatever but but in the end you have you have some guarantees that come out of that yeah I'm trying to think of something that I have that like anything that I would show you from what we use it for at work is kind of either exposes some things that I probably shouldn't expose or or has enough layers of indirection in it that like seeing the things that come out of it is not particularly helpful but but I do recommend all in general as a configuration language I also recommend it as a very fun thing for experimenting with like language features like the language implementation is so small I implemented kind polymorphism which you know sounds like crazy thing I don't know I've looked at the kind polymorphism implementation in Scala see and and it's super complicated like I couldn't understand it I couldn't do anything but I could implement it myself in Dahl in about half an hour because the language is just so small so simple that like the places that have to change you know you make one change basically and everything else just falls out of compiler errors and be like oh I need to update this to handle this I need to update that to handle that and you just like it's like everything is very clear everything is very straightforward so it's definitely a great language for experimenting both within and around but yeah that's sort of crazy things you can do with all the end you