Why algebraic data types are important - Bartosz Milewski - code::dive 2018

Strong static typing detects a lot of bugs at compile time, so why would anyone prefer to program in JavaScript or Python? The main reason is that type systems can be extremely complex, often with byzantine typing rules (C++ comes to mind). This makes generic programming a truly dark art. Interestingly, the theory behind types is relatively simple – a fact exploited by functional languages like Haskell or ML. I'll discuss elements of type theory and its connection to category theory and logic.

[fsaldan]

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.

[FastFSharp]

Oh my word, I need the rest of this talk!

[feihcsim]

arghh i wish Bartosz Milewski could have finished! what a gripping talk

[bocckoka]

I mentioned algebraic datatypes in an interview, thank you, google, for listening!

[piotrkozbial]

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.

[abels]

std::variant<int, int> 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!

[piotrkozbial]

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.

[rifaldhiaw]

I don't really get it on how exponential mapped to function type.
Anyone has a different perspective to explain it?

[brikken]

What a shame. Just when he got to the part justifying the title, he ran out of time ...