It is a paradox. I was Googling for explanations of why should I use discrminated unions instead of if else logic in my programming. Then I stumbled on this lecture. I already knew Bartosz from watching some of his videos on category theory. So I had high hopes of getting an answer. Then I watched one of the most fascinating videos I have ever seen. But my question remains unanswered.
The slide called "Systematic type theory" is a little misleading: the Hindley-Miller type inference only works for a limited type system (called, unsurprisingly, the Hindley-Miller type system), not corresponding to the full theories mentioned above it.
std::variant can be constructed by positional tags. Using std::in_place_index_t is not as pleasant to read and write than Left, Right, but it possible in C++. Additionally Providing he Left/Right syntax is also possible (for a cost of possible performance drawback though). Good talk otherwise!
One note to sums: the sum types or disjoint unions, have very little to do with set-theoretic unions. As far as I can understand, true set-theoretic unions would correspond to non-constructive proofs in logic and break the whole thing.
The way I like to think of is in terms of how algebra of types changes the cardinality. Cardinality is just a fancy way of saying how many elements are in a set. The cardinality of a Bool is 2, {true, or false}. Suppose there's another type "Tristate" which can be {0, 1, or 2}. The cardinality is 3. When we do operations against two types it results in an arithmetic change in cardinality. Adding two types Bool + Tristate means that the new type can be in one of (2 + 3) = 5 states {True, False, 0, 1, or 2}. Multiplying two types Bool * Tristate means the new type can be in one of (2 * 3) = 6 states { (True, 0), (True, 1), (True, 2), (False, 0), (False, 1), (False, 2) }. Exponentiating two types Tristate ^ Bool means the new type can be in one of (3 ^ 2) = 9 states { ((True, 0), (False, 0)), ((True, 0), (False, 1)), ((True, 0), (False, 2)), ((True, 1), (False, 0)), ((True, 1), (False, 1)), ((True, 1), (False, 2)), ((True, 2), (False, 0)), ((True, 2), (False, 1)), ((True, 2), (False, 2)), }. Notice that each entry is a possible mapping of Bool -> Tristate. This is why sometimes you will see Tristate ^ Bool as Bool -> Tristate which is just the left associative version of type exponentiation.
@@saxpy how are you deriving that exponential result? How are you conjoining the pairs? My interpretation of the exponential types is that given the set of all functions a->b, in this case Bool -> Tristate which results in 6 possible functions, you can do only 2 things with a function type like that. You can either return the function itself which is fine since a function is also a type, OR you can call that function with a boolean, in which case you will get a tristate type with a maximum of 3 possible values. So that gives you 6 + 3 = 9 possible values with a function as a type argument. Doing the opposite of tristate -> bool will give you 6 + 2 (true or false) = 8 values which is also 2^3. Let me know your reasoning.
It is a paradox. I was Googling for explanations of why should I use discrminated unions instead of if else logic in my programming. Then I stumbled on this lecture. I already knew Bartosz from watching some of his videos on category theory. So I had high hopes of getting an answer. Then I watched one of the most fascinating videos I have ever seen. But my question remains unanswered.
Oh my word, I need the rest of this talk!
arghh i wish Bartosz Milewski could have finished! what a gripping talk
I mentioned algebraic datatypes in an interview, thank you, google, for listening!
The slide called "Systematic type theory" is a little misleading: the Hindley-Miller type inference only works for a limited type system (called, unsurprisingly, the Hindley-Miller type system), not corresponding to the full theories mentioned above it.
std::variant can be constructed by positional tags. Using std::in_place_index_t is not as pleasant to read and write than Left, Right, but it possible in C++. Additionally Providing he Left/Right syntax is also possible (for a cost of possible performance drawback though). Good talk otherwise!
One note to sums: the sum types or disjoint unions, have very little to do with set-theoretic unions. As far as I can understand, true set-theoretic unions would correspond to non-constructive proofs in logic and break the whole thing.
Thank you. Cool exposition
What a shame. Just when he got to the part justifying the title, he ran out of time ...
I just rediscovered math.
I don't really get it on how exponential mapped to function type.
Anyone has a different perspective to explain it?
The way I like to think of is in terms of how algebra of types changes the cardinality. Cardinality is just a fancy way of saying how many elements are in a set. The cardinality of a Bool is 2, {true, or false}.
Suppose there's another type "Tristate" which can be {0, 1, or 2}. The cardinality is 3.
When we do operations against two types it results in an arithmetic change in cardinality.
Adding two types Bool + Tristate means that the new type can be in one of (2 + 3) = 5 states {True, False, 0, 1, or 2}.
Multiplying two types Bool * Tristate means the new type can be in one of (2 * 3) = 6 states { (True, 0), (True, 1), (True, 2), (False, 0), (False, 1), (False, 2) }.
Exponentiating two types Tristate ^ Bool means the new type can be in one of (3 ^ 2) = 9 states {
((True, 0), (False, 0)),
((True, 0), (False, 1)),
((True, 0), (False, 2)),
((True, 1), (False, 0)),
((True, 1), (False, 1)),
((True, 1), (False, 2)),
((True, 2), (False, 0)),
((True, 2), (False, 1)),
((True, 2), (False, 2)),
}.
Notice that each entry is a possible mapping of Bool -> Tristate. This is why sometimes you will see Tristate ^ Bool as Bool -> Tristate which is just the left associative version of type exponentiation.
@@saxpy Awesome.. thanks, you make it so clear just in some paragraph
@@saxpy how are you deriving that exponential result? How are you conjoining the pairs? My interpretation of the exponential types is that given the set of all functions a->b, in this case Bool -> Tristate which results in 6 possible functions, you can do only 2 things with a function type like that.
You can either return the function itself which is fine since a function is also a type, OR you can call that function with a boolean, in which case you will get a tristate type with a maximum of 3 possible values. So that gives you 6 + 3 = 9 possible values with a function as a type argument.
Doing the opposite of tristate -> bool will give you 6 + 2 (true or false) = 8 values which is also 2^3. Let me know your reasoning.
@@ritwik5774 this is not valid c++, but i think you will get the point.
enum tristate { a = 0, b = 1, c = 2};
std::function firstFunk = [](bool flag){ return flag ? 0 : 0 ;};
std::function secondFunk = [](bool flag){ return flag ? 0 : 1 ;};
std::function thirdFunk = [](bool flag){ return flag ? 0 : 2 ;};
std::function fourthFunk = [](bool flag){ return flag ? 1 : 0 ;};
std::function fifthFunk = [](bool flag){ return flag ? 1 : 1 ;};
std::function sixthFunk = [](bool flag){ return flag ? 1 : 2 ;};
std::function seventhFunk = [](bool flag){ return flag ? 2 : 0 ;};
std::function eighthFunk = [](bool flag){ return flag ? 2 : 1 ;};
std::function ninethFunk = [](bool flag){ return flag ? 2 : 0 ;};
@@saxpy Awesome explanation.
Watch at 1.25x
Very good advice. Thanks
More like 2x tbh