代數數據類型是什麼？

01-08

algebraic data types
只是類型的枚舉嗎？

Algebraic Data Type之所以叫這個名字是因為它可以像代數一樣做運算。

看過這個talk你就明白了-&> https://www.youtube.com/watch?v=YScIPA8RbVE

牆內可以看這個：

The Algebra of Algebraic Data Types, Part 1

The Algebra of Algebraic Data Types, Part 2

The Algebra of Algebraic Data Types, Part 3

參考A foundation for GADTs and inductive families

Every Algebraic Datatype (ADT) is characterised as the initial algebra of a polynomial functor on sets. This paper extends the characterisation to the case of more advanced datatypes: Generalised Algebraic Datatypes (GADTs) and Inductive Families. Specifically, we show that GADTs and Inductive Families are characterised as initial algebras of dependent polynomial functors. The theoretical tool we use throughout is an abstract notion of polynomial between sets together with its associated general form of polynomial functor between categories of indexed sets introduced by Gambino and Hyland.

其實最早是基於 curry-howard 同構搞出了 (+) 和 (×)，然後一發不可收拾……

比如類型 0 的意思是「程序不終止」

類型 1 就是 Lisp 里著名的 ()

函數類型給抽象成指數

而列表呢，給弄成了 $Lambda a.frac{1}{1-a}$ ，考慮到自然數的定義形式與之類似，於是 $m Nat=frac{1}{1-1}$ ，呃，自然數確實有無窮多。還可以證明「節點類型為 1 的二叉樹組成的七元組和二叉樹之間存在一一對應」這種看上去十分匪夷所思的結論。

f :: (Tree, Tree, Tree, Tree, Tree, Tree, Tree) -&> Tree f (Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) = Leaf f (t1, Node Leaf Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) = Node t1 Leaf f (Node t1 t2, Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) = Node t1 (Node t2 Leaf) f (t1, Node (Node t2 t3) Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) = Node t1 (Node t2 (Node t3 Leaf)) f (t1, Node t2 (Node t3 t4), Leaf, Leaf, Leaf, Leaf, Leaf) = Node t1 (Node t2 (Node t3 (Node t4 Leaf))) f (t1, t2, Node t3 t4, Leaf, Leaf, Leaf, Leaf) = Node t1 (Node t2 (Node t3 (Node t4 (Node Leaf Leaf)))) f (t1, t2, t3, Node t4 t5, Leaf, Leaf, Leaf) = Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 Leaf) Leaf)))) f (t1, t2, t3, t4, Node t5 t6, Leaf, Leaf) = Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 (Node t6 Leaf)) Leaf)))) f (t1, t2, t3, t4, t5, t6, Node t7 t8) = Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 (Node t6 (Node t7 t8))) Leaf)))) f (t1, t2, t3, t4, t5, Node t6 t7, Leaf) = Node t1 (Node t2 (Node t3 (Node t4 (Node t5 (Node t6 t7)))))

g :: Tree -&> (Tree, Tree, Tree, Tree, Tree, Tree, Tree) g Leaf = (Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) g (Node t1 Leaf) = (t1, Node Leaf Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) g (Node t1 (Node t2 Leaf)) = (Node t1 t2, Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 Leaf))) = (t1, Node (Node t2 t3) Leaf, Leaf, Leaf, Leaf, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 (Node t4 Leaf)))) = (t1, Node t2 (Node t3 t4), Leaf, Leaf, Leaf, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 (Node t4 (Node Leaf Leaf))))) = (t1, t2, Node t3 t4, Leaf, Leaf, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 Leaf) Leaf))))) = (t1, t2, t3, Node t4 t5, Leaf, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 (Node t6 Leaf)) Leaf))))) = (t1, t2, t3, t4, Node t5 t6, Leaf, Leaf) g (Node t1 (Node t2 (Node t3 (Node t4 (Node (Node t5 (Node t6 (Node t7 t8))) Leaf))))) = (t1, t2, t3, t4, t5, t6, Node t7 t8) g (Node t1 (Node t2 (Node t3 (Node t4 (Node t5 (Node t6 t7)))))) = (t1, t2, t3, t4, t5, Node t6 t7, Leaf)

ps. 最好玩的擴展應該是給類型求導， $frac{partial}{partial a}T$ 可以用來表示帶有一個類型為 a 的空位的 T 類型，和「真的」導數一樣揭示了數據結構的局部特徵。

推薦這篇文章：Algebraic type sizes and domain modelling

對初步了解 ADT 是什麼樣子的很有幫助，講的非常淺顯

簡單說就是struct/tuple和(tagged)union

http://www.haskell.org/haskellwiki/Algebraic_data_type

看目錄之前就可以。

函數式編程語言必須掌握的概念。

sum type、union type，maybe type，product type ，tuples，records這些都是。

模式匹配會用到代數類型。