…………………..-,,--’’’¯¯¯’’--,, ………………..,-‘’ ; ; ;-,,---,,- ; ;’’-,……………………………..-,,,---,,- ……………….,’ ; ; ;,-‘ , , , , , ‘-, ; ;’-,,,,-----’’’’’’---,,,-…..,,--’’ ; ; ; ;--;’-, ……………….| ; ; ;,’ , , , -,,--’’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ¯’’-’-,,- ,,--’’ , , ‘, ;’, ……………….’, ; ; ‘-, ,--’’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;’’-, , , , , ,’ ; | …………………’, ; ;,’’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;’-, , ,-‘ ;,-‘ ………………….,’-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;’’-‘ ;,,-‘ ………………..,’ ; ; ; ; ; ; ; ; ; ; ; ;-- ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ‘-,’ ………………,-‘ ; ; ; ; ; ; ; ; ; ;,-‘’¯: : ’’-, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; - ; ; ; ; ;’, ……………..,’ ; ; ; ; ; ; ; ; ; ; ;| : : : : : ; ; ; ; ; ; ; ; ; ; ; ; ,-‘’¯: ¯’’-, ; ; ;’, …………….,’ ; ; ; ; ; ; ; ; ; ; ; ‘-,-: : -,-‘ ; ; ; ; ; ; ; ; ; ; ; ; | : : : : : ; ; ; | ……………,’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ¯¯ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;’-,,- : :,-‘ ; ; ; ;| …………..,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ,,--’’ , , , , ,,,----, , , , - ; ; ;¯¯ ; ; ; ; ;| ..…………,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,’ , , , , , , ,( : : : : , , , ,’’-, ; ; ; ; ; ; ; ;| ……….,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;’, , , , , , , , ,’-----’’ , , , , , ,’ ; ; ; ; ; ; ; ;’, …….,-‘’ ; -, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ‘’--,,,,----’’’¯’’’--,,- , ,-,-‘ ; ; ; ; ; ; ; ; ; ‘, ….,-‘’--’’,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; | ; ; | . . . . . . ,’; ,’’¯ ; ; ; ; ; ; ; ; ; ,- ; ‘-, ……….,’ ; ;,-, ; ;, ; ; ;, ; ; ; ; ; ; ; ; ; ; ‘, ; ;’, . . . . .,’ ;,’ ; ; ; ;, ; ; ;,’-, ; ;,’ ‘’---‘’’ ………,’--’ ,-‘--’’ ‘, ,-‘ ‘, ,,- ; ; ; ; ; ; ; ; ‘, ; ; ‘--,,,-‘’ ; ,’ ; ; ; ; ‘, ;,-‘’ ; ‘, ,-‘, ……….,-‘’ ; ; ; ; ; ‘’ ; ; ;’’ ; ; ; ; ; ; ; ; ; ; ‘’-,,- ; ; ; -,-‘ ; ; ; ; ; ;’-‘’ ; ; ; ‘’ ; ;’-, ……..,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;¯¯’’¯ ; ; ; ; ; ; ; ; , ; ; ; ; ; ; ; ; ;’’-, ……,-‘ ; ; ; ; ; ; ; ,, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; |, ; ; ; ; ; ; ; ; ; ; ‘-, …..,’ ; ; ; ; ; ; ; ;,’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;|..’-,- ; ; ; , ; ; ; ; ; ‘, ….,’ ; ; ; ; ; ; ; ; | ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,’…….’’’,--’ ; ; ; ; ; ,’ …,’ ; ; ; ; ; ; ; ; ;’--,,,,,----’’’’’’--,, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,’…..,--’’ ; ; ; ; ; ; ,- …| ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ‘, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,’…,-‘ ; ; ; ; ; ; ; ;,-‘ …’, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ,-‘ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ,’….’, ; ; ; ; -,,-‘’ ….’, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ,-‘’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,’…….’’--’’¯ …..’’-, ; ; ; ; ; ; ; ; ; ; ; ; ; ;-,,-‘’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ,-‘ ………’’--,,- ; ; ; ; -,,,--’’ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,-‘ ………..| ; ; ;¯¯’’’’¯ ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,,-‘ ………..’, ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;,-‘ …………| ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;| …………’, ; ; ; ; ; ; ; ; ; --,,--- ; ; ; ; ; ; ; ; ; ; ; ; ; ;’, ………….’, ; ; ; ; ; ; ; ; ; ; ;,-‘….’’-, ; ; ; ; ; ; ; ; ; ; ; ; ‘, ………..,’ ‘- ; ; ; ; ; ; ; ; ;,-‘’……….’-, ; ; ; ; ; ; ; ; ; ; ; ‘, ……….,’ ; ;’ ; ; ; ; ; ; ,,-‘…………….’, ; ; ; ; ; ; ; ; ; ; ;’, ………,’ ; ; ; ; ; ; ; ;,-‘’…………………’’-, ; ; ; ; ; ; ; ; ; | ……..,’ ; ; ; ; ; ; ;,,-‘………………………’’, ; ; ; ; ; ; ; ; | ……..| ; ; ; ; ; ; ;,’…………………………,’ ; ; ; ; ; ; ; ;,’ ……..| ; ; ; ; ; ; ,’………………………..,-‘ ; ; ; ; ; ; ; ,’’ ……..| ; ; ; ; ; ;,’……………………….,-‘ ; ; ; ; ; ; ; ,-‘ ……..’,- , ; , ;,’……………………….,’ ; ; ; ; ; ; ; ,-‘ ………’,,’,¯,’,’’|……………………….| ; ; ; ; ; ; ; ; ‘--,, ………….¯…’’………………………..’-, ; ; ; ; ; ; ; ; ; ;’’-,, ……………………………………………’’-,, ; ; ; ; ; ; ; ; ; ;’’--,, ………………………………………………..’’-, ; ; ; ; ; ,,- ; ;’-,’’-, …………………………………………………..’, ; ; ; ; ; ; ‘-,--,--. ……………………………………………………’-, ; ; ;,,--’’’ , ,|, | ………………………………………………………’’--‘’- , , ,,’,-/--

---

在 Unix 和 Ruby 里我们考虑问题，是从问题域的 DSL 着手，例如 Unix 的很多命令都有自己的 DSL: sed, awk, ed 所以不掌握多种语言是不可能掌握 *nix 的。

在 Haskell 中考虑问题，是从问题域中对象的类型着手。假设我们要写一个 Lisp 解释器，那 Lisp 中的对象类型就是第一要解决的问题。在 Haskell 中可以定义一个统一的代数数据类型：

data LispValue = LispString String
               | LispInt Integer
               | LispDouble Double
               | LispBool Boolean
               | LispList [LispValue]
               | LispTuple2 (LispValue, LispValue)
               | LispTuple3 (LispValue, LispValue, LispValue)
               | ...

对比一般的静态语言中的做法：

• 在 C 里可以写 union, 但是你要手动判断一个 union 是哪个分支
• 在 C++ 和 Java 里，应用传统的 OO 设计思想，设计一个抽象类或者说接口 LispValue, 然后写各种具体类去继承和实现 LispValue

都比较麻烦，但是 Haskell 这么写就简单直白多了。

为什么叫代数数据类型呢？类型推导需要类型运算，类型运算中的 "对象" 就是类型。类型有两种运算：

• A | B 是加法运算，表达一个东西既可以是 A 类型，也可以是 B 类型，它的单位元 (零元) 是 Void 类型 (Void 代表了所有 Haskell 不允许的类型，包括空指针，所以 Haskell 是不可能出现空指针异常的)
• (A, B) 是乘法运算，表达一个东西是 A 和 B 的二元组，它的单位元 (一元) 是 Unit 类型。这里我们把 Constructor A B, A : B 都统一看作是 (A, B).

单位元的意思：

A | Void == A
Void | A == A
(A, Unit) == A
(A, Void) == Void -- 不可能出现这种类型的值, 所以运算的结果也是 Void.
(Unit, A) == A
(Void, A) == Void

| 满足交换律但 (,) 不满足：

A | B == B | A
(A, B) /= (B, A)

X | X 是什么意思？举个例子，我们有个算钱的程序，钱用分作单位，用整数表示，正数是盈余，负数是亏损，针对盈余和亏损我们有不同的处理，我们可以用 if 来处理：

f :: Int -> a
f x = if x >= 0
      then ...
      else ...

但使用代数数据类型和模式匹配，完全可以消灭所有 if 的存在

f :: Int -> a
f x | x >= 0 = ...
    | otherwise = ...

x 在这个模式匹配有两个 Int 的分支，可以认为 x 的类型是 Int | Int.

我们在小学学过，X + X = 2 * X, 这里我们定义 2 为一种只能取两种值的类型 (注意这和丘奇数不是一回事), 那么上面的算钱程序又可以这么写：

data Two = Positive | Negative
f :: (Two, Int) -> a
f (Positive, x) = ...
f (Negative, x) = ...

所以我们也有

X | X = (2, X)

加法和乘法还满足结合律和分配律：

(A | B) | C == A | (B | C)
((A, B), C) == (A, (B, C))
(A, B|C) == (A, B) | (A, C)
(A|B, C) == (A, C) | (B, C)

乘法运算之上还能定义幂运算：

(A, A) = A ^ 2
(A ^ n, A) = A ^ (n + 1)

类型，类型运算，和它们满足的运算定律，构成了类型代数。这个加法运算不是所有的元素都有逆元，所以不能成为群，所以类型代数也不能成为环，更不用说域了。但类型代数在很多方面和实数域有点相似，可以做一些类似实数域的运算 (下面的推导是工程师 style, 数学上其实并不严格...).

考虑 List 的类型定义：

data List x = Null | (x, (List x))

用 y(x) 代换 List x, 用 + 代换 |, 用 * 代换 (,), 那么我们有

y = 1 + x * y

解这个方程得

y = 1 / (1 - x)

再用泰勒展开得到

y = 1 + x + x^2 + x^3 + ...

这个表达式的意义就是 List 的非递归定义：

List x = Null | x | (x, x) | (x, x, x) | ...

严格点，上面 List 的标准写法是：

y = μy. 1 + x * y

μy. 标识着 "小心哦，这是一个关于 y 的递归定义!", 逐步代入展开又会是这样：

y = μy. 1 + x * (1 + x * y)
  = μy. 1 + x + x^2 * y
  = μy. 1 + x + x^2 * (1 + x * y)
  = μy. 1 + x + x^2 + x^3 * y
  = μy. 1 + x + x^2 + x^3 * (1 + x * y)
  = μy. 1 + x + x^2 + x^3 + x^4 * y
  = ...
  = μy. 1 + x + x^2 + x^3 + x^4 + ...

得到的结果和我们取巧用泰勒展开一样...

---

插入物理学圣剑一枚 (我个人最近的重大发现：其实这个词包含着 3 个梗... 这个撬棍是半条命里的物理学家 Gordon Freeman 的主要武器，也是奈亚子发挥宇宙 CQC 的道具，还和 Soul Eater 里的圣剑拿的那个杖长得神似...)

初学 Haskell 的一大难题就是各种数据类型都是不可变的，但是平时写程序已经习惯了各种可变的数据结构，要更新某个字段只能整个复制，造成效率低下？不是的，XMonad 里使用的 Zipper 就可以高效的转换可变数据结构到不可变数据结构。Zipper 类型和它名字一样，是个拉链状的东西，在 List 上的 Zipper 就像这样：

data Zipper x = (List x, x, List x)

zipLeft :: Zipper x -> Zipper x
zipLeft (left:lefts, middle, rights) = (lefts, left, middle:rights)

zipRight :: Zipper x -> Zipper x
zipRight (lefts, middle, right:rights) = (middle:lefts, right, rights)

从 zipLeft 和 zipRight 可以大致看出 Zipper 是怎么操作的：有点像纸带图灵机，纸带在上面不停的抽插移动，不同的是我们还能在纸带的停留点做插入和删除。假如我们有个文本编辑器，光标移动一两个字是常见的事情，那么用 Zipper 来记录光标的移动，在 Zipper 的洞里插入和删除字符，就很简单了，而且不需要拷贝整个链表那么蛋疼。

Zipper 代数数据类型怎么写？

z = y * x * y = (1 / (1 - x)) * x * (1 / (1 - x)) = x / (1 - x)^2

如果把 Zipper 中间的 x 掏空，我们就有

z' = 1 / (1 - x)^2

利用上面的 y 的定义，一项项检查 z' 可以取的值是什么：

• List 长度为 0 (y = 1): Zipper 不存在 -> z = 0
• List 长度为 1 (y = x): Zipper 只有 1 种：(_) -> z = 1
• List 长度为 2 (y = x^2): Zipper 可以是：(_, x) 和 (x, _) -> z = x + x = 2x
• List 长度为 3 (y = x^3): Zipper 可以是：(_, x, x), (x, _, x) 和 (x, x, _) -> z = x^2 + x^2 + x^2 = 3x^2
• List 长度为 4 (y = x^4): 照上面的类推 -> z = x^3 + x^3 + x^3 + x^3 = 4x^3
• ...

所以这个带洞的数据结构又可以写成：

z' = 0 + 1 + 2x + 3x^2 + 4x^3 + 5x^4 + ...

高数还没还给老师的朋友，可以看到这和对 y 取导数运算是一样的... 我们猜想

z' = dy / dx

我们可以用 List 的定义来推导 dy / dx, 看看是不是和 z' 一样。依上文我们有：

y = 1 / (1 - x)

取导数

dy / dx = 1 / (1 - x)^2 = z'

2001 年，Conor McBride 发现了代数数据类型的 "带洞形式" 都可以通过类似求导的方式算出来 (当然证明过程并不是这里写的那种 "工程师数学"...), 这就是我对类型代数运算所知道的全部。