A Taste of Type Theory: Understanding Identity Types in Programming

[00:00:08]thank you all right can you hear me yes okay uh well thank you Ed um I called you fully responsible for creating a monster that you are seeing here right now yes uh and thank you for um giving me this opportunity uh to visit uh beautiful Australia I had no idea it was a continent like this that that wonderful um I want to talk today just so this talk was listed as for beginners Okay so it's it's really funny yeah um so if you feel like at some point that you you don't understand something I'm saying you know it's like you're in the wrong place this is for beginners uh introduction to type Theory this is really really simple stuff yeah um so why why type Theory so I usually talk about category Theory right and and this time I decided to talk about type Theory which is sort of a little bit step behind or under I don't know it's like the foundations of mathematics but as always there is this weird convergence like everything is converging with with computer science with programming so type theory is also converging on the one hand being being the foundations of mathematics the new foundations of mathematics on the other hand something that we use every day in our programming right we have types and typed languages although there are some people who think that types are not important in programming JavaScript and stuff like this but ah uh well I won't talk about that um so um here's a little outline of my talk so I I'm I'm just heading towards one thing that that I found really interesting that sort of like I had like an epiphany about understanding uh these identity types um um but in order to get there you have to like find a path through uh type Theory um and um are actually sort of path from programming to type Theory and I think this is this is probably the shortest path that I could think of uh so first first I'll give you uh I'm gonna give you a little bit of motivation right so like why so identity types are are about equality what does it mean for two things to be equal it's such a trivial thing right um and but but but in order to express it in in type Theory you really have to start from from Basics from like nothing so um so these these identities first of all are recursive so I'll start by giving you an example of a recursive type but present very simple type so you will all understand but um but it's presented in a way that type theories do it and and they they have their ways right um uh then it's a dependent type so I'll give you a little bit of a refresher on what dependent types are um then I will tell you about induction okay because once we have dependent types and recursive types we can talk about induction um and uh then through propositions as types the Kerry Howard isomorphism I will explain what is so important about equality types or identity types right and finally I'll introduce identity types introduce and eliminate them at the same time and the elimination of identity types that's that's the interesting part this is what I really want to talk about and this is all uh sort of leading towards what is called homotopia type Theory although I'm not going to get into it but but it's a type Theory and it's based on it develops uh equality types okay so motivation right um so let's start by by um very simple problem 1 times a equals a okay how does one prove this thing right um so e but but in types okay so there is a type corresponding to one that's the unit type in Haskell now in other languages they kind of sneak this type under the carpet but in our schools explicitly a unit type and product times right is is a Cartesian product or a product uh um of pairs right so we create pairs so if you pair a which is an arbitrary type here right with unit type what do you get well you get something that's equivalent to this original type because pairing it with uni does not provide any additional information because there is only one unit right and it's always available available so in Haskell we would we would do this by by saying uh okay there is there is a function uh from despair to a and there is another function so this is left unit right left Lu as it works for all a so it's a polymorphic function that goes from despair to a and it just picks the second element of the pair trivial right and there is an uh the other function that goes backwards right goes from a and just slaps a unit on it pairs it with a unit a unit is always available so no problem there okay um so I'm cheating here okay so this is what what I would do normally in in programming but in mathematics uh they would slap me you know and they say uh well first of all this is this is not really equality we're talking about it's isomorphism right isomorphism means there is a function one way and there's a function the other way and they are inverse of each other okay so I showed the function one way show the function of uh the other way I haven't shown that they are actually inverse of each other right I could do some kind of equational reasoning on the side right not within the language but okay so a little bit of cheating there and I could show the isomorphism I think the second thing is it's uh like so what does the isomorphism have to do with equality what is equality to begin with right so equality is defined as uh if two things are equal you can replace one with another in any context okay and that's obviously not true because if you have a function that takes an a and you try to pass it a pair you need a the compiler will complain right so these things are not equal even though they are isomorphic so this is why equality is very important and and we are not yet treating them very seriously we are treating them as something on the side you know equational reasoning maybe uh and and replacing equalities with isomorphisms without really understanding why we can do that why is it okay to replace things like this um so there is a whole theory behind it and this is what I want to talk about or at least give you a taste I mean it's like this this would take uh a whole semester to explain but but just give you a little taste of it okay so we'll start by introducing to talk about type Theory I could start with like simple things but uh what we really need is recursion okay understanding recursion recursive types uh so um let's start with natural numbers right so um so you've probably seen the way natural numbers are introduced sometimes especially when you introduce numbers natural numbers as types when you do dependent kind of programming in Haskell um I don't know how many people did some kind of dependent programming in high school using nuts um so you Define natural numbers using uh these two Constructors zero and successor right it's called Piano arithmetic but um the the way type theories talk about types is they they uh for every type there is a way to introduce a type the introduction Rule and there is the elimination rule okay so these are the two important things so an introduction rule for us programmers means construction how do you construct it how do you create a function that will produce a natural number so there are two Constructors here Z or zero that produces a natural number from nothing so it's a Constructor takes no arguments right zero can always be constructed and and then there is the successor that says given a natural number I'll give you another natural number and sort of freely uh so that it's like a free construction because uh you assume that what you were given after this Constructor is a new number it's like freshly new minted number that's the successor of the previous number right and this is equivalent to all natural numbers because you can say okay I can produce a z i can use the Z Constructor to produce something and I will call this something zero okay arbitrarily then once I have zero as a natural number I can apply the second Constructor and I will get something new and I will say I'm going to call this one okay fine and and then I apply successor to it and I get something and I call it two and so on and I continue until I create all the natural numbers eventually right um uh so that's that's one thing so you can you can create these natural numbers but that's not really interesting until you know how to eliminate them elimination means uh I want to Define some actions that take natural numbers some functions so mappings out of natural numbers how do I map out of natural number how do I Define a function that takes a natural number well since there are two ways of creating natural numbers zero and successor then when I eliminate them I have to think of two ways of eliminating them like what do I do if when I get a zero that's what I do and what do I do and I get a successor of something so this can be formalized in saying well I have a base of type A so I'm I'm creating a function that takes a natural number and produces a value of type A sum a okay for every function this will be a different a um so I have to Define what this function does on on zero on Z right and that I call base so that's just a value of type A and then I then I have to have a function that tells me if somebody gives me a natural number [Music] um and uh and some previously created value in this sequence of creating values then I tell you how to get the next value okay and that's called a step so given base and step I can now generate a function that will work for any natural number because any natural number is obtained from zero by applying a number of steps to it right so if I know what to do for zero and I will know what to do for every step I'm done right so that's called the elimination right but there is also this part that says well once once you have created this function right uh uh you can give me any function and I won't know whether this was created from base and step or not so there is this condition and and it's usually called computation rule that says the function that I give you actually has this property that if you call it with z you will get the base and if you call it with a successor of some and you will get a step acting on F of n where F of n is defunct recursive call to the function so recursion occurs naturally as the computation rule this is where it comes in right there is also third thing that type theories often do is is the uniqueness like as is the function you we won't worry about this right so so this procedure of building a recursive function here is is uh um is written as as a higher order function rack so Rec takes a base takes a step and produces the function that we wanted from Nat to a okay that's the result this is the function and an example the simplest example is factorial right you take as your base and number one and step is n plus 1 times x so step is not the recursive function it's just a regular function right that's easy to Define but these two will produce using the computation rule will produce you the um recursive function that calculates factorials okay so this is the first part natural numbers um as an example of what a recursive type definition is right now let's do something uh more interesting let's talk about dependent types um so uh instead of interesting in general I'll give you first an example how you can work with dependent types and this is an example that's close to our hearts that's uh [Music] um that's the vectors okay counted vectors right so counted vectors are dependent types um and they they Define a family of types it's not just one type counted number a counted Vector is is a whole family of types that's indexed by natural numbers so there is a separate type for zero length Vector of a and there is a separate type for length one vector of a and length two Vector of a and so on each of them is a separate type you can't mix them and because of that you know we have this power that the compiler will tell us if we are doing something wrong with Vector sizes right it will match sizes and so on so I want to introduce some some family of types and this family of types in this case will be the family of vectors and this is this is how you construct a vector again com it's very similar to how you construct natural numbers you have two Constructors one Constructor nil creates an empty vector and then cons given an existing Vector of size n will produce a vector of size n Plus 1.

[00:18:10]and some value of type A of course that you put in front of the existing Vector so you get a vector of size n and you slap another a in front of it and you get a vector of size n plus one and the interesting thing here is that the the stuff in red tells you well so it's a function that takes n which is a value right and takes types A and then vac a n is another type and this type depends on the value that was passed before the N right and the result also depends on this n so this is this is the equation in types right it tells you what what how types are created but it has one one of the arguments there is a value and that's what dependent types are these are types that can depend on values I mean normally we have types that depend on other types you know like list of integers depends on int right right here uh it depends on on values but I really uh this I I want this type because I want I want to show you induction I want to show you uh uh a little a dependent induction is a dependent elimination so I I'm still talking about uh natural numbers right but I need these vectors to have a family of times uh so that I can define a new way of eliminating numbers okay so I want to create a function that a dependent function that would take natural numbers of arguments but for every n it would produce a different value of different type right normally a function produces a different value for different values but here it produces different values of different types for every n so that's what I want to do okay so I want to define a dependent function of natural numbers this is why I needed vectors as an example of something that I could be creating right so um and this is called induction I'll explain in a moment why it is called induction right like right now we are doing calculations so you start with a type family and the example of type family is this Vector index by n and just like before we had base and step but this time base and step is dependent so it depends on N it does not before we had base and step all producing something of type A right so it was the same type for base and step here we have something a little bit more interesting bass produces one type Vector of size zero okay an empty vector and step takes n as before but it takes a vector of size n and produces a vector of size n plus 1 or successor of n right and this is a different type before it was taking something of type A and producing something of type A here it's changing type it's producing something of a different type okay so for every step you will get the value but it's a value of a different type and then an example of a function like this is a very simple example you you have some value uh constant value of type c and you want to replicate it so you want to be able to create vectors of size n that are filled with this single value so C right so how do you do this well you define base base is supposed to produce you in this case a vector of size 0 and the Constructor for Vector of size 0 is nil that was my Constructor for Vector of size 0. so base is equal to nil uh and my step will be uh will will take a vector of size n and slap a c on it and produce a vector size n plus one so it's it changes the the type right it takes a type Vector of N and will produce type Vector of n plus one a different different type okay um so this can be um encapsulated as a recursive scheme that is dependent dependent type uh and it's it's called induction okay so we what we did is Define induction on natural numbers and in general so I I use that for generating vectors right but in general induction is is defined by uh first defining some type family which was vectors in my case so given a Thai family C and you give me a base and a dependent step and given base and dependent step I can create a function dependent function from not to c n so it's a function that takes natural numbers and produces values of different types depending on n okay so it's more General than the previous recursive function right where where all the values were of the same type A here the type changes with ends so end is is this higher order function that defines oh okay for all uh right so end is this function that takes base and and takes step so the second argument second line is step and produces this dependent function right and it has a computation rule as before uh it looks almost uh well it looks the same right it looks the same but but but this this is a computational rule now involves different types at each level okay so this is uh so why why am I calling this induction why do people call this induction okay and this has to do uh with the propositions as types Curry Howard isomorphism that every type can be thought of as a proposition which is something that can be true or false okay so what's what's a true proposition it's a type that is inhabited that has elements like we normally deal with types that have elements right like Boolean has two elements and integer has infinitely many elements and so on so like every type seems to be inhabited right except that there's this one weird type void that is not inhabited except for the bottom of course right but we'll ignore that so so what does it mean well it means that well there are some um more complex types like like function types you know it's like you give me some value and I produce some value of some other type can I always Implement a function like this if I can Implement a function like this then it's proved that this function type is inhabited because I just implemented the function of this type right but if I can't if it's impossible to implement a function like this because it doesn't have enough information or so in its argument to produce a result well then maybe uh this is an not inhabited type so a type that's inhabited is a proof is is a is a true proposition in this language and every inhabitant of this type is the proof that it's inhabited obviously right so it's a proof of this proposition so this is the summary of Curry Howard isomorphism right and then here's an example like the the proof of a proposition that A and B right consists of a proof of a and the proof of B right what does it mean it means that this proposition A and B is trans translated into pair of type A B right and the proof that it's inhabited that this type of a pair of a b is by constructing this pair and in order to construct this pair somebody has to give me a value of type A and the value of type B and the value of type A is a proof that a is inhabited and the value of type B is the proof that b is inhabited so given these two proofs I construct a proof which is a pair okay and in it inhabits the pair type and there may be many proof of the same proposition you know obviously right so how does this relate to induction okay so now we have induction was like we had this type family right so for every n we had a type CN right so now if we look at the types as propositions uh it means for every n we have a different proposition so if there's a proposition that's indexed by n and we want the proof that all these propositions are true right so we want to prove something for every n this proposition is true right and the way we do this in type theory was we had this base and step now we we interpret this base since it's a value of type c of Z right C of zero uh then it's a proof that c of zero is inhabited right so base is the proof that c of zero is inhabited and step is to prove that c of n plus 1 type is inhabited as long as the type C of n is inhabited so I'm proving that c of n plus 1 is inhabited using C of n right and this is exactly how we were taught induction in school right you have the base case and you have the step and now we understand how how this works in type Theory so this is what induction is and this function in just generates the proof for all and essentially so induction now we have a new understanding of it induction is just depending the elimination of natural numbers that's what it is right so now we have all the ingredients to talk about identity types okay so identity types is is uh is um specifies that two things are equal two values are equal okay so it's a prop sort of a proposition that says you know given an X of type A and another y of type A are these things equal right so using Curry Howard isomorphism we could say okay so we have the proof of equality should be like an inhabitant of a certain type because this is a proposition corresponding to the to equality right [Music] so that means so now you see why we need dependenties because for every X and every Y which are values of type A there is a separate statement separate proposition is x equal to y right so I have to have a different type for every pair of X and Y and this type I call ID of X Y this type is either inhabited or not depending on what value of X and Y I give it right so if I give it a x that is different from y it's not equal to Y this type will not be inhabited will be empty right if I give it something that's equal two values that are equal and then it should be inhabited right I should be able to prove that it's inhabited so now I have a type family idxy which is parameterized by X and Y by values so it's very similar to what we were doing with these dependent types right we started with the type family um now this this identity type is often uh is in the beginning it might be confusing but then you get used to it it's written in infix notation so x equals y now is a type so you put this equal between the values that you're operating on so it's a type that depends on X and Y and sometimes there is this index a uh signifying in what type we are talking about like both X and Y of ta are of type a right and now if if somebody gives you a value of this type x equals y this value is a proof that x equals y right because it means that x equals y is inhabited but they have to give you a proof for every possible pair of X and Y or not give you a proof because maybe X is not equal to Y then there is does not exist a proof like this so these a lot of these types most of them kinda are in not inhabited only the ones that um are correspond to equal values so how do we so now we have a family of types now how do we uh Define this type right I mean so the way to define a type was by uh introduction and elimination right so how do we introduce this type we have to have a Constructor something that would Constructor this Constructor would have to depend on X and Y right um and how can we construct we have you have to construct it from something that we know kind of is true and the only thing we know that it's absolutely true about equality is that a thing is equal to itself right it's a trivial statement everything is equal to itself right and that's called the reflection of the as a property of of this relation of equality it's reflect it's reflective right um so so reflection is the only way we can introduce identity in general right like we don't know anything about equality but this we know for sure right X must be equal to X so this is the only Constructor of the equality type raffle okay so this construct is called raffle from reflection right raffle takes one argument value right and produces a value of type x equals X all right so x equals x is a type and the raffle is the value of this type which serves as a proof we can then use this everywhere as a proof a x is equal to X and I have a proof of this and I can pass it in my program you know to everybody to testify that X is equal to X it might sound really crazy right it's like but it means that everywhere I have a x i can replace it with x um so I'm I'm uh here's the here's like a diagram uh drawing like you can you can think of this like X and Y uh on on a plane right these are two coordinates and they're like every point on this plane corresponds to a type uh that X is equal to Y right so if you have X and Y X is equal to Y is a type so every point on this plane corresponds to a equality type a different type right and now I know that the diagonal the types that sit on the diagonal they are all inhabited right and they are inhabited by these values called raffle different for every point on the diagonal because every point on the diagonal is a different type right but they are all inhabited and I have a proof of this okay so introduction is is really a piece of cake it's the elimination of this type that's really it's like okay so I can give you a proof of x equals to Y which probably means that X is the same as y because the only way I was able to create it is using refer what can you do with it right how do you define a function that takes a proof of equality of two things right so that's that's the elimination principle and the elimination principle is really really weird and this is why I wanted to explain it to myself and uh hopefully I'll I will give you a little bit of of intuition why uh why this works uh so first of all identity is a dependent type it's doubly dependent on X and Y um so we'll be now I introduced these natural numbers induction and so on for the purpose of giving you an analogy because the elimination of equality types is analogous in some ways to the elimination of natural numbers it just goes like way beyond that okay so when we were eliminating natural numbers we had we started with a with a type family that was parameterized by natural numbers so now we would have to start with a tight family we have to Define some kind of type families capital c that depends not on natural numbers but depends on these values X y well depends on the proofs of equality but proofs of equality it's themselves depend on X and Y right for every X and Y you would have to have a different proof of equality so it's really a function of three arguments x y and P okay X is a value of type A Y is the value of type A P is the value of type x equals y so it's a proof that X is equal to y and that produces a different type for every X Y P so there's a family C of X Y P so that's that's what there is at the bottom right so there is this family that's parameters by three parameters it's like a three-dimensional family that is our starting point so this is this corresponds in this analogy to our counted vectors they depended on one parameter n this thing depends on three parameters the the important one being P the proof of equality so we want to eliminate these proofs of equality right so going by analogy again for natural numbers we had two introduction principles Z and S zero and successor right and for each of them we defined like our starting point base and step which would move us from one natural number to another now for identity types we only have one introduction raffle that was the only thing right so our elimination uh should be a function of of one uh argument so it's instead of having base and step it just has something that's both base and step okay so what should it do well it should produce a value it should be a so this step in the previous case step and base produced a value of the particular type so here we want this to produce a value of a type that corresponds to the introduction so introduction was only introducing elements on the diagonal right using refer so elimination will will start by saying for raffles I have a proof okay give me no give me a proof for raffle to begin with and then I can extend it for every other equality like you give me a proof for natural numbers you gave me a proof of zero and you gave me a step how to proceed from one to another and then I gave you a proof for every n here give me a proof of raffle and I can extend it to approve for every equality that you can give me right so this proof for raffle will be a function little s right that it's a dependent function so it takes X as an argument right and produces a value of this type this diagonal type c of x x raffle X right C was defined on the whole three-dimensional volume kind of for for X's y's and P's uh now we are just looking at the diagonal and and saying this diagonal is inhabited okay so you give me the proof that the diagonal is inhabited and I can proceed from there so that's that's the input that you give me this is my step of induction right it's a sort of a little very very tiny step of induction because there is no movement in there like step in in the induction for natural numbers who's moving you from one place to another it's moving what you buy one right here this is a step that's not really moving you much it's just constantly sitting on this diagonal so combining this the elimination principle for for uh identity types is this by analogy Again by analogy with inductive uh procedure for creating a function of n right which took base step and produces a function of n here instead of base and step we have this function that I called little C right that was proving that there is a value for every type on the diagonal right and then it produces a proof that this C this Proposition C uh or this type c is inhabited outside of the diagonal it's inhabited for every x y and p right you see it's like the result of this C is c x y of P so it gives me a value of c x y of P but it only gives me a value if I can give it arguments okay so I mean I can give it X and I can give it y but it also requires this P okay and P is a proof that X is equal to y okay so if I can't provide this argument meaning X is not equal to Y I can't produce this value okay so automatically like if these two things are equal I will produce a value for you okay if these two things are not equal I can't produce a value sorry you have to provide me the the proof that X is equal to y and there is a corresponding computation rule that you can figure out it's like this the function that's obtained through induction right if you substitute the original Little C into it you should get what you expect right if you substitute the raffle right yes what what was it oh oh the computation rule uh okay so what was the computation rule for for natural numbers it means that if you substituted Z right you would get the base and if you substituted step you would get um the next value from the previous value so here the only thing that you can substitute is you can substitute the raffle right so so end will give you this function from X Y P to C of x y p right so take this function call it with x X again instead of Y and raffle which proves that X is equal to X and you should get a value this value better be the same as your input which was the little function C right okay uh-huh right yeah yeah I get typos okay accurate oh okay well it's renaming I did some renaming on the fly yeah yeah and and for all yeah okay okay first oh that works now need to shout in the first one I think you need a for all in front of the just after the first Arrow yeah of your end of now because the scope of the ends on those two lines are different yes that's true that's true this is a different end right right yeah sorry I was kind of sloppy yes okay last slide ah perfect timing um Okay so so this is the uh these are the formulas that you can like read in in this book uh on homotopic type Theory or on any type theory that deals with dependent types and identity types right uh but what I wanted to do is is give you a little bit of intuition how this relates to something that we already know which is which is induction principles right and dependent types um and it's uh it's it's really a kind of mind-blowing generalization of the induction principle because normally induction principle uh tells you well I proved something uh for the starting point and then you know you make a step and I give you a proof that if if you were able to get here that you can make another step and you'll get to the next point right so if you prove something for for this place you know you started from Z you got here you know all happy uh I'll tell you how to make the next step and and that's enough for you to cover all the distance to any end right but the thing is that this step is kind of discreet for natural numbers it goes from n to n plus one so there is like a size of one between your steps and that that's what makes it easy with identity types there is no step really because you're dealing with arbitrary types you don't know you don't have a distance there you can say you can make a step like this right but before you get there right you you have to cover half of the distance right so maybe my induction should be for half of a distance but before you get to half of the distance you have to get half of the half of the distance right you see where I'm getting like it's it's kind of xenos paradox there before you get fro before you make a a journey from one place to another you know you have to make a little step and the sizes of these steps there is no lower bound there is no like with integers you have one and you cannot go below one here there is no limit so every path from one place to another and by the way these equality uh types are called paths in homotopia type Theory because they have they they have a model for this in actual hamotabi where these things correspond to paths so the proofs of equality are paths from one place to another and what I'm saying is that I have the proof of equality on the diagonal right which has to serve me both as a starting value and as a step but what's the size of this step the size of the step is zero so it's like moving an infinite decimal distance and shrinking this infinitesimal distance to zero and you get a path of size 0 which leads you from X to X right and the fact that this works is it's just really truly miraculous you know it's like you know you you get you get this path you shrink it shrink it shrink it and because there is no granularity there you shrink it to zero and it still works so shrinking this path to zero and getting raffle edges gives you enough information to extend it to the whole path so I'm going to end with this like wisdom I guess you know it's like every Journey Begins with reflection which makes sense in this case of extending paths starting from the proof of the minimum proof which is reflection okay thank you [Applause]