Type theory and the algebra of types

[@MsSlash89]

This is undoubtedly the best introduction to Type Theory on KZbin. My compliments! ❤

[@hemerythrin]

5:15 "please note that this is very different from returning a pair, which would always contain a number *and* an error" If only someone had shown this to the inventors of the Go language

[@DeathSugar]

considering they just made generics recently it's pretty descent way to return errors as values.

[@EvanMildenberger]

*Rust's Result type has entered the chat*

[@DeathSugar]

@ in go

[@NStripleseven]

@@EvanMildenbergerreal and based

[@APaleDot]

I never knew you could do algebra with types. This is amazing!

[@05degrees]

You can even do some black magic with solving equations about inductive types, like trees or lists, for example “seven trees in one” allows packaging any binary tree into seven and vice versa, any 7-tuple of binary trees of the same type into a single one, uniformly; but you can’t do that with e.g. five trees! due to an equation the type satisfies. But it’s early for that yet. And later it appears that wasn’t magic but it surely feels like one anyway. Simple algebra is useful too, for example for automatically deriving generic recursion schemas on any inductive type that uses just sums and products (though some form of exponentials can be carefully allowed too), for example Haskell allows writing code for doing that. Though I seem to find now usually another scheme is used, defining both the type and its associated _functor_ (which is like the type itself but with blanks in place of recursive occurrences of the same type in its definition) manually to your desires and then linking them, instead of deriving one from another and using clunky wrappers. Well, this application is probably not the clearest one, it just came to my mind first.

[@monsterhunter8595]

Lesssgoooo a type theory video!🎉

[@joeeeee8738]

This is basically set theory. I never knew algebra of types existed! I'd like to understand where they start to look different

[@Schnep]

I've actively been trying to understand these concepts for so long now, but after seeing this, it finally feels like it "clicked". Fantastic job!

[@EvanMildenberger]

15:00 The bottom two rules allows you to simplify programs: a pair of functions to the same codomain can be merged into one by getting the disjoint union of the two domains and doing some pattern matching internally. That allows you to have less functions at the tradeoff of their domain/codomains being more complicated. And a function that has a structured input can be changed to a chain of composed functions that process each field of the product type sequentially. That allows you to have more functions where each one can focus on just part of the original value.

[@nokkel6935]

I love how concise and intelligible your videos about these somewhat obscure and mysterious subjects are. Looking foreward to the category theory one :)

[@05degrees]

Yesh! Great polynomial intro into type math! 🎷🎻 Also add in one of future videos that an empty type is useful as: - a marker of a place in the code which shouldn’t be reachable, or a function that doesn’t return; - an empty error additive means no error can ever happen, if we write generic code that’s agnostic about specific error types and wish to use it with error-less functions; - a quirk to type only empty data structures: List can contain just an empty list. Likewise 1 is useful in generic data structures to add no other information where some could’ve been provided and (ideally) occupy 0 extra bytes of memory. No wonder that “trivial values” get extremely useful in generic context, as it’s the case in math overall and why they were devised, more or less, historically (but more so now when we know better why we want them to exist!).

[@MoiraLachesis]

Like with numbers, you can obtain a unit as the exponential of 0. (There is exactly one function to map from the empty type to a fixed arbitrary type). Unlike numbers, the base can also be 0.

[@AllAnglesMath]

Cool! I never looked at it like that before.

[@simeondermaats]

ahhh, the subject of my bachelor paper and (if all goes well) my master's thesis as well ❤❤ great to see you do a video on type theory!!

[@EvanMildenberger]

7:20 An interesting aside is that the exponential 2^3=8 is for all *possible* functions of the `from Fruit to Bool` type. The example shown in the top is a specific function from that general type even though it's programming type signature would also be Fruit -> Bool. The general vs specific function distinction was confusing to me in the past.

[@jamieoglethorpe]

E.W. Dijkstra used the idea of treating a two argument function as a new function with a fixed first function as currying (somebody called Curry, I presume). So currying the two argument Add function with 1 would give you the Incr function, or with -1 to give you Decr.

[@jamieoglethorpe]

I posted this comment just before you said the same thing. I left it because it could be of interest.

[@dekumarademosater2762]

Currying _is_ spicy, but it's named after a person.

[@AllAnglesMath]

I always put lots of Haskell on my chicken.

[@C3POtheDragonSlayer]

Hope to see a video on the calculus of types as a followup!

[@morgengabe1]

2:10 Sugar, Spice, everything nice, armpit hair, snails, a puppy dog tail, and chemical X.

[@jursamaj]

Chemical X is only if you want a Power Puff girl. There are other recipes for other types of people. 😁

[@morgengabe1]

@@jursamaj are the rowdy ruff boys merely a joke to you?

[@jursamaj]

@@morgengabe1 Ah, I see. Never saw those episodes.

[@enricomariadeangelis2130]

Very nice videos for newbies! ❤❤

[@m4rt_]

Sum types are also useful when making a parser: struct Token { enum { TOK_INTEGER, TOK_,FLOAT, TOK_IDENT, TOK_KEYWORD /* ... */ } kind; union { struct { uint64_t value, bool signed } _integer; double _float; char* _string; enum { KW_FUNCTION, KW_STRUCT, KW_ENUM, KW_UNION, KW_IMPORT /* ... */ } _keyword; }; };

[@kevon217]

this was super helpful. made a lot of sense

[@torb-no]

I’ve been somwhat interested in abstract algebra (and beyond)’s connection to programming but I never quite managed to grasp it, but the stuff in this video just clicked. So thanks! In which video so hou further explain monoids? I had a tiny bit of group theory at University so I understood the basic defintion at Wikipedia fine, but I’d like to know more. EDIT: found a ‘what is a monoid’ video, I assume it’s that one

[@jaorlowski]

I think there is an error in the explanation: exponential functions were with the whole set/vector (i.e. ALL values!) of properties while the combination was multiplication. Which makes sense: if you have colours and fruits and merge it with colours of vegetables you will get the sum of the elements not the product. (given they have the same colours) The exponential operation from 10:00 on is the set of 2-tuples (pairs): - relations of colours from "a" with a full vector of properties of fruits - left hand side element - the relations of a colour from "a" with a full vector of properties of vegetables - right hand side ...equals the number of combinations of colours from "a" with the complete set of properties of fruits AND that of vegetables. The same goes on later with people and properties. I believe you want a triple (person, weight, height). Otherwise we would get the function of all properties and populations. I.e we'd have a mulitverse and each element would be the set of relations like (a strawberry is green AND and Orange is Yellow AND a leek is purple...) so its more like a mux/demux kind of thing

[@DreamzAnimation]

Is there a meaningful distinction between currying and function composition? Or do they mean the same thing, just in different contexts?

[@NovemberIGSnow]

Yes. Curried functions return functions. So if Subtract(2) returns a function that subtracts the input from 2, then you can call Subtract(2)(3) and get the result -1. You can also keep the result of Subtract(2) around and invoke that function on multiple other values. This is orthogonal to function composition which is when you pass the result of another function as an input into another function. Like Increment(Square(3)) to get a result of 10. With function composition, the functions are defined independent of each other. Which means you can also swap the order they're applied, like Square(Increment(3)) = 16. You cannot swap the order of curried functions, i.e. you cannot try to get something like Subtract(_)(3) to get a function that subtracts 3 from its input. And because these concepts are orthogonal, you can combine them together: Increment(Subtract(2)(3)) = 0

[@matchamitminze]

@@NovemberIGSnow At least re: Subtract(_)(3), you can do some silly shenanigans with something like `flipsub = ($ 3) . flip $ flip subtract`, so that `flipsub 5` yields 2, but I don‘t think I‘d recommend it in a serious context. :)

[@RobotProctor]

I dont get the difference between the unit type and the empty type in your description :/

[@drdca8263]

It is possible to have a value of type the unit type. There is exactly one such value. It is impossible to have a value with type the empty type.

[@NovemberIGSnow]

In addition to what drdca8263 said, you can only ever have a single empty type, but you can have infinitely many unit types. It's just that each unit type only has a single value (hence the name "singleton"). You can have two singletons and use them for different things. If you somehow had multiple empty types, they would all be identical to each other and act the same as each other.

[@jeejeejee2837]

This is same as concepts of additive and multiplicative identities in abstract algebra. It basically means that result of any binary operation e*a where e is identity, is always a. For example; 0(empty type) is an additive identity in integers because 0+n is always n for all integers n.Similarly 1(or unit type, in context of this video) is multiplicative identity because 1×n is always n(for all integers n). You can extend this to type theory and clearly see that empty type and unit type are identity types that do not modify other types(and/or their values) under specified operations. Hope this clarifies it a little.

[@MaxPicAxe]

1:42 Cartesian* :P

[@AllAnglesMath]

Yeah, you're right, I don't know why I keep spelling that incorrectly.

[@MaxPicAxe]

Love this video!!!

[@foobargorch]

wait but a pear is a fruit so how can it contain a fruit

[@AllAnglesMath]

😆

[@DeathSugar]

i wonder if we will wonder in the proof assistant world with that

[@mistylight3521]

I think i just don't get it. Like so what? What does it bring to the table? How does it corellate with the real world? I know about the sum types and currying (never used it or have seen somebody use it), but what about the stuff at the end, what's the real world example of that?

[@dekumarademosater2762]

anything written in Haskell, Ocaml or any ml variant. Haxe, maybe? They're there, you just have to turn over the right rocks

[@mistylight3521]

My bad, I thought we were talking about the real world problems and their solutions

[@SimGunther]

The opening note is overly simple. Types wouldn't make _all_ of software development easier. It prevents some bugs, but you still need proper mathematics on the business requirements, which **SURPRISE** isn't all written down in a master compendium that rivals Les Miserables.

[@m4rt_]

Do note that type theory ignores real world scenarios like when a function only can return 2 out of 3 possible values. In the real world you have to keep the real world in mind, rather than only following what a theoretical world can do. Also, using those constraints you get from a real world scenario, you can often end up with better code, than if you forced yourself to handle impossible scenarios, or scenarios that shouldn't happen.

[@AllAnglesMath]

The thing is, type theory can only operate on the theoretical level. It doesn't know anything about the actual inputs to the program (i.e. the "real world" you refer to). This is the distinction between static typing and runtime errors.

[@drdca8263]

Can you give a specific example that dependent types can’t properly address? If you just have products, sums, and exponents, then yeah, definitely there are things such as type system can’t handle. But, dependent types seem like they should be able to handle pretty much anything?

[@AllAnglesMath]

@@drdca8263 I'm not familiar with dependent types. The only 2 cents I can contribute, is that a static type system can never handle "everything". That would make type checking undecidable, which is not very useful.

[@drdca8263]

@@AllAnglesMath If you know how your program is supposed to behave, you should (usually, unless not knowing is kind of the point) know whether each part halts, and be able to prove it. The type checking with dependent types, at least if you include like, equality types etc., should allow checking a proof that whatever parts should halt, do. I believe such a type system (which is equivalent to some fairly powerful axiom system, though of course incompleteness does apply as Gödel showed) should be able to check any well-defined property that one would reasonably hope for it to check, provided that you are willing to make your program effectively include the proof.

[@atreidesson]

No, zero isn't a natural number.

[@NovemberIGSnow]

Depends on which mathematician you're talking to. A lot of mathematicians treat 0 as a natural number and if they want to exclude 0 they'll say "the positive natural numbers." Ultimately it doesn't matter, it's all a matter of convention.

[@atreidesson]

@NovemberIGSnow well, I just said there is the convention because most mathematicians do not consider 0 a natural number

[@simeondermaats]

@@atreidesson In Belgium we tend to consider zero a natural number. It's taught this way in most if not all schools.

[@lietpi]

​@atreidesson look up 100 Questions: A Mathematical Conventions Survey

[@drdca8263]

@@atreidessonEh? I haven’t checked any surveys, but I find it hard to believe that a substantial majority are on the side of not including it. For the set theorists, I would expect they would use the finite von Neumann ordinals as their standard implementation of the natural numbers. For the algebraists, I would expect they would include zero so that it is a monoid (or a rig if you include the multiplication) not just a semigroup. Only group I would expect might exclude it is the number theorists *maybe*?