Maybe Not is an excellent video in some ways, but I just watched it a few years later and it reminded me that as much as I love almost every Rich video, I do wish he'd spend some time reading a little deeper on type systems and theory.
For example his note about "Categorical descriptions" and then the explanation about maps/and spec at 25:00[1] seems to indicate he's unfamiliar with the difference between extensional and intensional type theory.
The core difference between the two is extensional type systems decide equality on the observable behavior of the output. For example if two functions take the same input, and produce the same output extensional type systems/theories say they are the same. The problem with this is type equality is then undecidable.
Extensional type systems also struggle because there are more than one way things might be equal! For example two string might be equal if you ignore case, but unequal if you don't. So if we want our type system to check if two functions are equal under case insensitivity an extensional type system will struggle with this.[2][3]
Now in fairness to Rich, these concepts come more from the math community, especially the notion of types being equal under different paths, and in the case of Homotopy type theory are burred in unapproachable language and concepts... even by mathematicians standards.
He also talks about select from spec, and it not preventing you from passing types broader types, and the necessity of specifying deeper type.[4] But, that's just an eliminator defined on the type[5].
Now most strongly typed programming languages suffer from the issue he identifies when talking about not making brittle systems [6] and the issues you get with coupling around taking a map/struct/product type C = A X B (e.g a map C = {A: something, B: something}), and you require A so you're function should be good but you fail to compile because the function says A, and now you're passing C.
It's frankly pretty annoying in places like Java that if you have a Point = Int x Int y you can't use it in functions which take a Tuple = Int x Int y. I'd actually say that's the common observation that both Rich, the Go Inventors, and the TypeScript folks have all made. You need to care about the extensional type of your input (and output) fairly often. And carring around the intensional type causes both dependency issues and just some general PITA's.
For example his note about "Categorical descriptions" and then the explanation about maps/and spec at 25:00[1] seems to indicate he's unfamiliar with the difference between extensional and intensional type theory.
The core difference between the two is extensional type systems decide equality on the observable behavior of the output. For example if two functions take the same input, and produce the same output extensional type systems/theories say they are the same. The problem with this is type equality is then undecidable.
Extensional type systems also struggle because there are more than one way things might be equal! For example two string might be equal if you ignore case, but unequal if you don't. So if we want our type system to check if two functions are equal under case insensitivity an extensional type system will struggle with this.[2][3]
Now in fairness to Rich, these concepts come more from the math community, especially the notion of types being equal under different paths, and in the case of Homotopy type theory are burred in unapproachable language and concepts... even by mathematicians standards.
He also talks about select from spec, and it not preventing you from passing types broader types, and the necessity of specifying deeper type.[4] But, that's just an eliminator defined on the type[5].
Now most strongly typed programming languages suffer from the issue he identifies when talking about not making brittle systems [6] and the issues you get with coupling around taking a map/struct/product type C = A X B (e.g a map C = {A: something, B: something}), and you require A so you're function should be good but you fail to compile because the function says A, and now you're passing C.
It's frankly pretty annoying in places like Java that if you have a Point = Int x Int y you can't use it in functions which take a Tuple = Int x Int y. I'd actually say that's the common observation that both Rich, the Go Inventors, and the TypeScript folks have all made. You need to care about the extensional type of your input (and output) fairly often. And carring around the intensional type causes both dependency issues and just some general PITA's.
[1] https://www.youtube.com/watch?v=YR5WdGrpoug&t=1504s [2] https://math.stackexchange.com/questions/4486995/what-is-an-... [3] https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Ext... [4] https://youtu.be/YR5WdGrpoug?t=2668 [5] https://www.quora.com/In-type-theory-what-is-an-eliminator-a... [6] https://youtu.be/YR5WdGrpoug?t=2823