Introducing Product, Sum and Equality Types: Spilling the HotT

[00:02] was talking about the links between logic and programming. The wonderful relationship that is the Curry Howard correspondent where every logical proposition has a corresponding type and every constructive proof corresponds to

[00:17] a computer program that implements that type. In this video, I'm going to cover type. In this video, I'm going to cover the logical operations of and and or as the logical operations of and and or as well as the predicate equals. I'll show

[00:30] how they have equivalences in type theory. I hope you'll be able to experience some of the wonder and joy that I felt when I learned all of

[00:46] and. It's the logical operator that is true if and only if both of its arguments are true. In classical logic, it has this truth table. And we can also

[00:58] represent and with these rules of inference from A and B, we can infer that A is true. We can also infer from A and B that B is true. If we have both A

[01:13] and B that B is true. If we have both A along with B, then we can infer that A and B is true. So what is the type equivalent to this? Well, in natural language, we often use and to create pairs of things like Tio and Tia, spy

[01:29] pairs of things like Tio and Tia, spy and family, homes and Watson. If we have and family, homes and Watson. If we have a type that is a pair of items of different types, would this work as our and equivalent? Yes. If we have a type

[01:43] that is populated with pairs with one item from the first type and the other side of the pair with an item of the second type, in order for it to be populated, we would need an item from both types to exist. in order to create

[02:00] one of these pairs. Now, if any type involved is uninhabited, then it is impossible for this pair type to be inhabited because there is nothing to populate that item slot in the structure. The only way a pair type can

[02:16] be populated is if we have items from both of the constituent types. There was a brilliant comment on the previous video from Mahai Nati that function

[02:28] types acted like exponentiation. Well, pairing in this exponentiation. Well, pairing in this way very much acts like multiplication which leads to the name of product type and this is why we are justified using

[02:43] the multiplication symbol to represent it. The three inference rules for and it. The three inference rules for and also have three corresponding functions. also have three corresponding functions. The projection functions PR1 which is a

[02:58] The projection functions PR1 which is a cross B to A and the projection function cross B to A and the projection function P R2 which is A cross B to B. These projection functions allow you to extract a witness from the first or

[03:13] second elements of a pair. If you are familiar with functional programming, these are often called f and this inference law corresponds to the inference law corresponds to the constructor pair a to b to a cross b

[03:28] constructor pair a to b to a cross b which in most places including is just written as this which I'm not going to attempt to

[03:41] about that other key part of logic, the humble ore? Oes are true if at least one of the arguments to them are true. And or is also true if both sides are true, as in this classical truth table. A few of you with backgrounds in classical

[03:57] of you with backgrounds in classical logic, digital electrical engineering, or Minecraft redstone might have already thought, we already have and and not. Could we just make an or out of them? Congratulations because in classical

[04:11] logic that's exactly what we would do. However, this doesn't work in However, this doesn't work in constructivist logic. So, let's dig a little bit more into computer science to find a working solution. Let's use an

[04:26] example of a rather common problem you'll often run into programming in the real world. Say you are writing some sort of weather statistical system and

[04:38] your job is to write the program that downloads the temperature recordings from the sensors all over the country and store them. Another team will write the program that will do the processing of this stored information and make the

[04:52] results. However, you have a slight problem. Not all the temperature sensors are made by the same company. So they present the data in slightly different ways. Some of the sensors give the output as an integer whole number

[05:08] values. The other sensors are made by a completely different company and output the values as floating points. So decimal values. These are represented

[05:20] differently inside computer memory. Although in most cases they might take up about the same amount of space. At some point you'll want to convert these values to be in the same form. However, the program that collects the raw values

[05:36] from the sensors might not be the program that does the conversion and management has given you the requirement that the raw values have to be stored before any processing is done. They explain this because if there's a bug in

[05:50] the processing, they want to be able to go back and rerun the processing on the archival values. Well, we know about product types. Could we use one of them

[06:02] here? Well, we could make a type that looks like this with a sensor ID, a temperature in float form, a temperature in integer form. That allows us to store both types of temperatures. Oh, and the field names are that just there for

[06:17] readability. They're not really a part of the type itself. There is a problem though. While we're able to store both types of values, there's no way to know which value should we should use. So, let's add an extra format field for

[06:32] let's add an extra format field for that. This format field contains a tag which tells us to use a float or an integer. Then, we know which of the two fields to use. However, this is rather inefficient. There's always going to be

[06:46] a field that isn't used. If we were gathering a lot of data, that's a very large amount of wasted space. But in a computer, a float and an integer take up about the same amount of space in

[07:01] memory. It's just how the computer interprets these bits in memory that determines what they are. So if we had a way to tell the computer how to interpretate them interpret the memory location and if we had it treat the

[07:15] memory location differently depending on that then that would give us a clean solution and we already have this format field. So we could restructure it like this. In computing, types like this are often called tagged union types because

[07:32] they contain a union of two possible types and a tag to tell you what type to use. Other names for this kind of type are co-product type or the name that I

[07:44] are co-product type or the name that I will be using some types. And some types will work perfectly well in our types and propositions world as well. In type theory, some types are notated like this, a + b and are populated with a tag

[08:04] this, a + b and are populated with a tag and elements from either a or b. Some types are populated with as many elements as the elements in the left

[08:16] side plus the right side. Just like with product types, the inference laws have product types, the inference laws have corresponding functions. in L or in left

[08:28] corresponding functions. in L or in left which is A to A + B in R or in right which is A to A + B in R or in right which is B to A + B and wreck A + B which is B to A + B and wreck A + B which is this. I'll explain why this is

[08:42] called wreck and what the pi is doing here in our next uh hot tea video. But here in our next uh hot tea video. But for now I'll explain it as being you can

[08:54] for now I'll explain it as being you can take create a witness for c from a + b take create a witness for c from a + b if you have a witness of a to c and a witness from of b to c. I think this makes sense. You have to have a function

[09:10] makes sense. You have to have a function to be able to handle each of the potential types that could be in our sum type. In functional programming type. In functional programming language, this function is often called

[09:23] [Music] either. We have reached the point where we have a system of logic and propositions. However, at this moment, we don't have a way of getting information from the element level up

[09:38] into the proposition level. For that, we are going to need predicates, a way to ask information questions about the quality of the entries that inhabit

[09:50] these types. And one of the most fundamental properties of an entity is fundamental properties of an entity is equality. Are these two things equal? is equality. Are these two things equal? is a pretty important question. It is the

[10:04] a pretty important question. It is the basic question that all of primary and basic question that all of primary and much of secondary school education is constantly being asked of you. In type theory, everything that is a

[10:17] proposition, everything that we could have a yes answer to is represented by a have a yes answer to is represented by a type. Equality is no different. When a type. Equality is no different. When a type is defined, it also defines a whole

[10:30] type is defined, it also defines a whole family of equality types. One or every family of equality types. One or every combination of two entities within that type. If the two entities are equal, then that type is inhabited by a

[10:45] witness. The simplest way two things can be equal is if they are the same entity. In this case, the equality type gets a witness called riffle, short for reflect. This is called judgmental or

[11:02] definitional equality. But two things can be equal without being exactly the same thing. Let's have an example. Say you want to represent the rational

[11:15] numbers, the numbers that can be expressed as a fraction. One of the ways expressed as a fraction. One of the ways you can do this is as pairs of whole you can do this is as pairs of whole numbers, a numerator and a denominator.

[11:27] And yes, I haven't defined how we're going to do whole numbers yet, but let's just assume that whole numbers just work the way you expect whole numbers to. We good with this? Excellent. Now, clearly in the case of 1 2 1 2, both numerators

[11:42] match and both denominators match. They are both equal to a half. So clearly are both equal to a half. So clearly equal. But what about 24? Two quarters is also a half. If we want to have a system that works like rationals, we

[11:57] need some way to say that these two things are equal. This is done by adding to the type a uniqueness principle. A uniqueness principle basically allows

[12:11] multiple entities in a type to be different names for the same thingy. Technically the proper name for this is a referant but thingy works just as well. This uniqueness principle requires that any function that interacts with

[12:28] these entities as a domain to treat these entities exactly the same. So the function should always give you the same output if the these entries are put in.

[12:41] This type of equality is called propositional equality. So for a rational type we say rationals are equal when they're the same value or a value that you get after multiplying the numerator and the denominator by some

[12:57] whole number. So long as the whole number has an absolute value of one or number has an absolute value of one or more. Uh why did I use such a roundabout way of saying nonzero in constructivist logic? It is often easier to talk about

[13:12] logic? It is often easier to talk about positive statements rather than negative statements just because of the way that we don't have the law of the excluded

[13:29] We have the ability to combine propositions together so long as we are dealing with a fixed finite count of propositions. But in order to express

[13:41] things like the rational numbers uniqueness principle, we are going to have to have propositions that operate on an unknown possibly infinite count of propositions. For that we are going to need the tools which will be provided in

[13:57] the next video in this series. Pi types and sigma types. So, please subscribe to learn about them when the next video in this series comes