Haskell 类型代数的运算 (内有熊和物理学圣剑)

luikore · 发布于 2013年1月09日 · 最后由 mizuhashi 回复于 2016年12月21日 · 6363 次阅读
2880
本帖已被设为精华帖!

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


在 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)

zipLeftzipRight 可以大致看出 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 发现了代数数据类型的 "带洞形式" 都可以通过类似求导的方式算出来 (当然证明过程并不是这里写的那种 "工程师数学"...), 这就是我对类型代数运算所知道的全部.

共收到 20 条回复
60

这个对数学要求略高啊

165

每次看LZ的文章,总有一股自卑感。

96

难道粉丝刘德华也要自卑吗……high就够了……

1723

你好haskll的那篇中文入门的网址您能给发一下吗?

96

插入的物理学圣剑和lambda有什么关系

2880

#9楼 @WolfLee 这是... 为了丰富文章内容, 避免过于枯燥而插入的无关内容...

96

只明白前1/3的梗,和其他人一起自卑...

96

艾,自卑的人都不知道 @luikore 永远都是高高在上的……

2880

#12楼 @keating 你够了... 至于吗

96

#13楼 @luikore 晕,看来我卖萌了…sorry

198

完全没看懂。。

239

楼主篇幅太长了。

23529

Zipper的类型可以通过List求导得来,所以得出Zipper的数据也可以由List的数据以类似求导的方法取得吗? 类型吻合但是数据不吻合的情况应该很多,感觉Zipper更像一种巧合,或者说只是知道类型信息的话其实推导不出什么...

2880

#17楼 @mizuhashi 其实和求导形式如此相似是必然的而不是偶然的, 证明在链接的论文中...

23529

#18楼 @luikore 对啊,因为对数据内容的操作就是求导,所以类型必然是求导,等于说类型变换是数据变换的必要条件

23529

熊没了....

需要 登录 后方可回复, 如果你还没有账号请点击这里 注册