✳flâneur — a map of the web's best reading

a very occasional diary @ Nikita Danilov | What is cosh(List(Bool))? Or beyond algebra: analysis of data types.

cofault.com · 3,302 words · saved by 1 readers

There is that curious idea that you can think of a type in a programming language as a kind of algebraic object. Take (homogeneous) lists for example. A list of integers is either an empty list (i.e., nil) or a pair of an integer (the head of the list) and another list (the tail of the list). You can symbolically write this as Here 1 is the unit type with one element, it does not matter what this element is exactly. 𝐴 + 𝐵 is a disjoint sum of 𝐴 and 𝐵 . It is a tagged union type, whose values are values of 𝐴 or 𝐵 marked as such. 𝐴 ⋅ 𝐵 is the product type. Its values are pairs of values of 𝐴 and 𝐵 . The underlying mathematical machinery includes "polynomial functors", "monads", "Lambek's theorem", etc. You can stop digging when you reach "Knaster-Tarski theorem" and "Beck's tripleability condition". In general, we have In Haskell this is written as Similarly, a binary tree with values of type 𝑥 at the nodes can be written as That is, a binary tree is either e

a very occasional diary @ Nikita Danilov | What is cosh(List(Bool))? Or beyond algebra: analysis of data types. \( \def\List{\operatorname{List}} \) \( \def\integer{\operatorname{integer}} \) \( \def\nat{\operatorname{nat}} \) \( \def\Bool{\operatorname{Bool}} \) \( \def\Punct{\operatorname{Punct}} \) \( \def\BT{\operatorname{BT}} \) \( \def\B{\operatorname{B}} \) \( \def\T{\operatorname{T}} \) \( \def\R{\operatorname{R}} \) \( \def\Set{\operatorname{Set}} \) \( \def\Bag{\operatorname{Bag}} \) \( \def\Ring{\operatorname{Ring}} \) \( \def\plug{\operatorname{plug}} \) \( \def\Zipper{\operatornam

Explore this link on the map →

related reading