Scale By The Bay 2021 : Vlad Patryshev, Algebraic Data Types, Categorically

Scale By The Bay 2021 : Vlad Patryshev, Algebraic Data Types, Categorically

Recording: Scale By The Bay 2021 : Vlad Patryshev, Algebraic Data Types, Categorically

hi there i'm really thankful to the organizers uh like they're all my friends so it's been for a while so so we are back again at scale by the way the topic is algebraic data types categorically i'm a categories more or less by education but i'm a programmer so when i encountered those algebraic data types i started thinking so what's that exactly why are the algebraic and there was a lot of misconception about this and that so about like last year i eventually like put all those things together and well i'm like uh like you're uh you're so it didn't explode but it exploded in my head so i know now what it is and i'll try to share with you my knowledge so but first when when we are in computer science there's a lot of like kind of thinking uh like an argument like for example i was teaching in santa clara university for eight years and when the students come over there like computer science students i ask them can you prove in piano arithmetic uh the commutativity of addition yes for example two plus three uh two plus three three plus two and here's a proof like i'm starting this this is an expression for i believe number three and so on and then i was patiently training them not to use proof by example you can have a like counter example that's a different story so the same happens when you're trying to learn adt algebraic data types some people's there are abstract data types like you you open a book you open like a text and you see for example two plus plus three and then like a syntax tree and so on so what is it i don't know so i i was really curious about what is it about so let's let me like walk over the things and explain to you what i understood so first the terms notation right so if we have x and y a cartesian well it could be types it could be objects in a category it could be sets e and set theory so a cartesian product of them is like in sets it's just it consists of pairs x y where x is from x and y is from y for example a type x y so it's a type of pairs in scala i'll be giving a lot of scala example all those colors not like what i'm going to talk about x to the power of n is a cartesian product of x with itself and times for example array of x in scala so if you have a raise of the same size so we have a cartesian product of x it is itself the power of x one is a special cartesian product x to the power of zero is a terminal object also known in such a singleton set and this is what it is x to the power of zero and for example in scala one the terminal object is uh type unit so in scala you in the category of types of scala so unit is a terminal object in that category x plus one it's a union of objects or a sum it is a disjoint sum of objects x with objects x a union of object x with object r y inserts is just a disjoint union in scala you can model it by using either zero is annotation for an initial object empty set e set theory in scala it's nothing you can also use a null for that but no okay zero initial object so one notation f is an arrow from x to y in scala they're all called functions or method and they denote it the same way in case of sets we are talking about functions and you're pretty much familiar with it i guess arity of a function it's the number of functions parameters so if we have a function f from x y z to t so this function in scala uh well this is annotation in scala this function has rt3 if we have a function f column t so in a sense it's a function it has arity 0 it always returns a value of t and it doesn't need any parameter so this is more or less color notation for parameterized types and people don't use it frequently in category theory but i use it in category theory all the time this means that we apply a p p maybe a functor to a type object or set x so what is p could be anything any mapping of objects like for example listings color so list the functor x is the type and we apply list to type x and we produce another type so it's list is another factor in this case and this notation is pronounced in latin as a quad era demands random and it's also called tombstone halmos end of proof so that's where proofs are ended in math theorems so and this is it's notation it's okay done with notation so what is the theory let's start with algebraic theory without actions by the way there are two kinds of theories algebraic and geometric i'm not going to talk about geometric theories just keep in mind geometric theories are also there out there and they're very different from algebraic theories so we're not granted an algebraic theory currently also known as levier theory lover is a great mathematician in someone like albany new york i believe so an algebraic theory t consists of one just one data type and a collection of operation symbols of finite error definite is important so here's an example numbers with addition and multiplication so we have zero uh zero additive symbols zero and one and for example an expression in that algebraic theory is like this one plus one whatever we in insert parenthesis although they're not parts of the language but they're like i would say part of parts of meta language we probably have to change the word method to something less proprietary these days starting today so another example sets algebraic theory of cells we have algebraic theory meaning like it's not the full set theory we have union intersection singleton uh set like given a set produce a single concept with uh just that element and zero energy uh operation this is used for empty sets here's an expression in that theory so we take like singleton single time united with this and intersect with this with this if you know what it is the result would be a singleton concept containing a singleton containing empty set we don't care about results this is the theory this is not a calculation so we don't say that this is equal to something we didn't we cannot say that something is equal to something if we don't have axioms and we don't know how to transform something from them to something else and there's a word for for a theory algebraical node without axiom the word is language so because this is a language of expressions that's all we can do produce expressions any well-formed expression well-formed means like we use operation symbols properly we use the correct arity and we just build a correct expression and we can use bnf anybody knows what bnf is becca's nor a form to specify the theory because it's just expressions so but again no axioms right a more complicated kind of theory algebraic theory the theory with axioms so algebraic theory consists of one data type and collection operation operational operation symbols and axioms and what are axioms in algebraic theory in geometric theory they look different axioms look like this we have an expression on the left expression on the right and equality symbol this means that one expression can be replaced in another if we are doing something with like bigger expressions here's an example of algebraic theory of numbers we have numbers like we don't know what numbers are but we have operations plus multiplication we have zero we have one and have uh all these things like commutativity neutral element for addition neutral element for multiplication and so on i'm not going deep into numbers we'll get there a little bit later with monolines so another algebraic theory uh with axioms for sets so we say that oh a union b intersection c is equal to a union b intersection a union c so this equality of these axioms allow us to transform one expression into another and back so here are examples of algebraic theories piano theory we have one mallory operation which is number zero like it's a symbol zero and unrepetition s so the early expressions we can build this here parenthesis is missing right okay anyway you see that the parenthesis is missing uh it should be ss0 we could as well uh ignore the parenthesis so that's all the uh correct expression we can have in piano except that this one is not correct so magma with root magma is basically like a tree or like a manoid but what does it have it has another operation called root and it's denoted like this bottom and binary operation let's call it m and here's an example of correct expression in magna so m takes two parameters so one parameter is bottom the other one is this big expression this big expression is m and it takes two parameters like m bottom bottom and then bottom so here's an example of correct expression in magma obviously this one is correct this one is not okay but see no axioms so we don't transform anything to anything here's a nicer example of an algebraic theory monoid i believe there are at least two talks that mentioned monoliths today maybe more so gene no not the bill definitely mentioned monois and somebody else too so what what we have in minority we have a single type we have another operation let's call it zero and we have a binary operation let's call it op so and two axioms one is zero is a neutral uh element for operation so zero operated with any a it gives us a and vice versa so a operated with zero will be a and op is also associative not every operation is associated but this one is uh if we are talking about minorities it should be associative so a of b of c is a of b of c so that's ammonoid that's an algebraic theory of monoid it's not a monoid it's a theory we don't have any monoids yet we don't know what zero is we don't know what op is so we don't have more noise all we have is the theory now how can we have any monoids we need models so here i'll be talking mostly about models in sets but actually you can take like any category where we have creation product and union so a model of a theory is just a representation of a theory like given theory t in sets or maybe like in a category that we choose so what do we need for this we need an object x so that object x could be a set could be a type in a programming language and for that set we need these things for every operation called m of arity n we need a function that is an arrow well an arrow is a function in set theory it's just an arrow in types in programming languages maybe it's also called method whatever but so fm is from x to the power of n to x so it's an energy operation m and given an operation m we produce a function so that's that's it you cannot have uh any axioms but if you have axioms those those axioms should hold i show you the like examples later so instead well see we have like a collection of axioms and again did they say that there should be a finite number of operation symbols definitely a finite number because arity is finite you cannot have an infinite number of operations with a finite attitude no we can but again it's finite finitory theory that's what i'm talking about so if the theory has axioms so actions should be there but if not then okay instead of individual functions like from x to the power of n to x we can build the union for all operations of additive k we take x to the power of k and take the union because for every such x to the power of k there is an arrow to x there is there will be an arrow from the union p to the power of t to x so why do i denote uh it like this because it's basically a function it's a factor that produces these expressions like primitive expressions of type x and the whole collection of arrows gives us a function an error from p to the power of t or x to x so we could either have a collection of these or just build a thing and talk about this thing that's it here are examples piano numbers what do we have in piano we have uh zero operation now array and we have human reparation s so do we need for this uh x to the power of zero which is one and x to the power of one which is x so this factor p t of p t it's just a union of two possible uh powers power of uh zero and power one so one plus x this is the factor for piano numbers a little bit looks a little bit like uh option function right so magma with root so magma has what magma has zero arity uh symbol and uh symbol m m of uh like 82 so we'll need 1 plus x to the power of 1 plus x square so this is how this well i would call it factor uh that this is how the functor looks like but we don't know if it's a function we can prove it separately later monoid we have one plus x square y we have a knowledge operation and binary operation but we also need axioms so this p should satisfy some actions because these functions should should be satisfying the axioms so here's how it looks in scala because it's one plus x square in scala we can model it like this either of unit and xx so that that's how this algebraic expression is can be written in scala and we will need this operation from p to the power of x to one plus x uh two x right this operation consists of two operations one is defined on one one operation is called u and the other operation is defined on x square i denote it like this because it's kind of it reminds the operations of matrices and vectors and so on and we have a union so that's how it is so we have an operation that on the first component it's u and the second component is its m and that's not enough because we need axioms right so here are the axioms written in severely categorical style so one this is the simpler version of the action unit so we have we have x map it to x cross x so we apply u on the left side the left component would be u the component would be u the right component would be the same x so identity so it's u cross x and then apply composition apply this merge operation yeah but sorry we've got a little problem here we are offline now we need a couple of minutes to solve it so should i go back i don't hear you okay i can hear him can you hear me cloud admin i i can hear you here i think they are offline so i don't know where they are so do you remember where we stopped i think only they know we i could see you uh he's trying to send me a note and let me see what i get back okay you're alive when now he need to go back a few slides or does he [Music] go back to a few slides so like this one algebraic theory somebody should tell me like where i should uh restart claude admin do you know how far he should go back he's somebody else yeah i'm afraid we do not know exactly what slide was he doesn't know for sure vlad uh so let's just go back one or two slides and continue okay so now a model of theory of a theory so given a theory we can model it in sets or in any category with cartesian products in addition so what is a model it's just a representation of theory t in like in sets or in a category that we choose so what do we need for a representation of a theory a theory as we know consists of just operational symbols right so we have one types because we have one type we represent it as an arbitrary object a set or a type in programming language for every operation we need the function if the operation is called m so we call the function fm and if the operation is of rat the function is from x to the power of n to x and if there are axioms the action should be followed i will show you an illustration instead of individual functions we can just take a union of all those x to the power of n for different uh ends for different case for all operations and define the operation component wise on this union let's let me show you the examples like one example piano numbers which has a nullary operation and a unary operation s so we'll need x to the power of zero and x to the power of one and take uh take the sum so one plus six that's the factor for piano numbers and a model would be an operation that maps one plus a function that takes one plus x and maps it to x so magma with root if you remember what magma is we have a root and we have a binary operation for gluing together parts of magma so we have x square for this binary operation and we have x to the power of 0 for for for the root for bottom so that's that's the factor for magma based root and monoid is like magma with roots but also it needs axioms and i'll show you how we do it specifically for monoids so ammonoid is again one plus x square that the type the factor right so it can be modeled in scala as either of unit and cartesian product of x plus x and x and we'll need an operation from p of x to x and that operation consists of two components u that is defined on one and m that is defined on x defined on x square and so denote it like this as if we are dealing with matrices and we will need axioms associativity axiom and union axiom associativity goes like this take x cross x cross six and apply m to the second and third component and keep the first one uh intact so we'll have like from x y z will have x the pair x and m of y z and then apply m so it will be m of x of m of y z so this way and this should be the same as this and this would be apply operation to x and y and keep the intact and then apply operation to the result of that to z so we'll have m of m of m of x y comma z that's what we'll have and the result should be the same and the same with identity like either we take an x then take a pair x uh x and unit and do a composition or we take unit and x so uh unit then x and take a composition it will be the same identity on x so that's how uh categorically we can express these actions so just an illustration so now to be like more abstract go back a little bit here p is built out of powers of x uh and there can be can exist more than one operation of arity k so there could be can be a union of several x's to the power of k so this could be like a quotient like 2 x square and 3 3x cube and so on so it looks like a polynomial and here's a general definition of a polynomial functor it's another factor because like it goes from the same category from a category to itself like for instance from sets to sets so a polynomial functor is the functor p that takes an object x and maps it to a polynomial object which is the sum or union of c n which is a just integer number no natural number multiplied by x m so what's a natural number just one plus one plus one so this is how polynomials look like polynomials well we don't use any negatives here in this specific cases that's how polynomial functions look like here are examples of polynomial functions 1 plus x 1 plus x square and anything so if you don't see that it's a factor you can it can be just an exercise but it has a map natural transformation that preserve identity identity and composition so it's up to you to check so an algebraic theory any algebraic theory with without actions when it's modeled by object x in a category c or like uh by uh by a set x gives us a polynomial functor and then error from p of x to uh 3x so it's just an algebra over the functor pt and that's how alg algebras over frontal are defined like for any factor it's an arrow from p x to x so here here the definition of algebra so given a factor an algebra over f is an error from f x terms right so the category of all such algebras is denoted as c to the power of f these arrows in this category are known as structures morphism in haskell so that's how it's written like in a mixture of scala or haskell and categories so if we have an algebra from f on x and algebra on y the correct morphem the structured movement would be an arrow from x to y such that this diagram can use okay so what's the fixed point of a factor a fighter a fixed point level factor is any such object x that f x is isomorphic to x and a fixed point doesn't have to be unique right suppose f is an identity function so anything is a fixed point so the smallest fixed point of a functor is an initial object in the category of algebras here's an example like given an object a type a list is a functor that is denoted as one plus a cross x and the operation would be nullery and unary operation that multiplied by x so this functor is an initial algebra because it's an initial object in the category of algebras there's also the biggest possible fixed point but it's like it's a tricky thing it's a terminal object in the category of coal chips and it's denoted like this and in in the case of the category of the functor that multiplies by a the uh the terminal object is an infinite list like in what well stream streaming scala right so why is this initial object the fixed point well that's easy right so look how these algebras can be mapped to each other so of course we can map this to this because f of y f of i maps to i and so f of f of y i must have i but because it's initial there are also a unique standard error from this to this so this this would be the same so yeah flood we are at time unfortunately and we have one more session after this but this is beautiful stuff i need like a couple of minutes okay so this arrow is called the catamorphism and i'll skip like existence of initial algebra but it could be built multi-sorted algebraic theories you can view the slides it's complicated and models models simplified model so these are the topics worth studying further like roles of terminal uh algebra's class uh categories parametric types and libraries theory in original formulation by olivier encounter examples like non-infinity monad doesn't have initial algebra so this is the book where one chapter is dedicated to model theory and this this is the collection of links one is basics like jdt and so on basically by people that invented uh generalized algebraic data types andrey bauer writes it uh pretty nicely and sergey vinsky also write that stuff well and this is a deep foundation so algebraic theories book the big book all of years publications and so on and you can also write the uh read that stuff in mclean and murder and you can try to read uh and catalog junior chain also like has a nice stock on that and so that's it uh i also wish to config and this is the link okay thank you