Algebra of ADTs – Constantine Ter-Matevosian

In this video we discuss the algebra of algebraic datatypes and their algebraic representations, touch on the type-theoretic similarities of the set-theoretic definitions of isomorphism and equinumerosity, and learn to construct derivatives and zippers of datatypes.

Sources:
Joel Burget, "The algebra (and calculus!) of algebraic data types": https://codewords.recurse.com/issues/...
Derivative of a type: https://en.wikipedia.org/wiki/General...
Differences between type theory and set theory: https://en.wikipedia.org/wiki/Type_th...
Zippers & differentiation of datatypes: https://en.wikibooks.org/wiki/Haskell...
Conor McBride, "The Derivative of a Regular Type is its Type of One-Hole Contexts": http://strictlypositive.org/diff.pdf

Get FP merch that doesn't suck. 👇
https://shop.serokell.io/

Follow us on social media:
  / serokell  

Learn more about us:
https://serokell.io/
https://github.com/serokell

Contact us:
[email protected]

0:00 Intro
0:40 Set cardinality
1:53 Cardinality of simple non-parameterized datatypes: Void, (), Bool, Ordering
2:18 Cardinality of parameterized datatypes: Identity, Pair, Either, Maybe, Arrow
4:53 Datatype isomorphism
6:27 Isomorphism of 'Either a a' and '(Bool, a)'
6:39 Isomorphism of 'Maybe ()' and 'Bool'
6:50 Mathematical representations of recursive datatypes: List
7:50 Isomorphism of '[()]' and the Peano naturals
8:05 Poking "holes" in datatypes: the algorithm
8:51 Poking "holes" in the product types
10:02 Poking "holes" in the sum types
10:59 Poking "holes" in the 'Ordering' datatype
11:13 Poking "holes" in the pair of 'Either's
11:54 Derivative of a datatype
12:19 Zipper
12:40 Homogeneous pair zipper
14:09 List zipper
15:40 Binary tree zipper
17:48 Conclusion
19:35 Outro