布尔类型

一个布尔类型的值可以为真或假，在Haskell可以这样定义：

data True
data False

data关键字用于定义数据类型。我们用True表示真，用False表示假。

自然数

我们可以这样定义自然数：

0 是自然数
如果x是自然数，x的后继也是自然数

根据这个定义，我们在Haskell可以这样：

data Zero
data Succ a

Zero表示0, Succ a表示a的后继，这里a是个变量，表示任意值。有了这两个定义，我们就可以表示所有的自然数：

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Three
...

相等？

首先我们定义相等比较：

class IEqual a b where
    type Equal a b :: *

这里用class定义了一个接口IEqual，这个接口只有一个方法Equal，Equal接受两个参数（a和b），并返回一个值。

我们可以比较两个自然数是否相等：

0和0相等
0和任意x的后继不相等
x的后继和y的后继相等，当且仅当x和y相等

我们可以通过instance实现这个一个接口，把上面比较方法翻译到Haskell：

-- 0和0相等
instance IEqual Zero Zero where
    type Equal Zero Zero = True

-- 任意x的后继和0不相等
instance IEqual (Succ x) Zero where
    type Equal (Succ x) Zero = False

-- 0和任意x的后继不相等
instance IEqual Zero (Succ x) where
    type Equal Zero (Succ x) = False

-- x的后继和y的后继相等，当且仅当x和y相等
instance IEqual (Succ x) (Succ y) where
    type Equal (Succ x) (Succ y) = Equal x y

我们可以在ghci测试一下：

ghci> :t undefined:: Equal Three Three
undefined:: Equal Three Three :: True

ghci> :t undefined:: Equal Three Two
undefined:: Equal Three Two :: False

:t表示求值，undefined ::后跟要取值的表达式。上面是说对Equal Three Three求值得到True，对Equak Three Two求值得到False。

Haskell还会阻止你定义矛盾的实例。

假设你定义了Zero和任意数相等（当然这是不对的），然后再定义Zeero和任意Succ a不相等:

instance IEqual Zero a where
    type Equal Zero a = True

instance IEqual a Zero where
    type Equal a Zero = True

instance IEqual Zero (Succ a) where
    type Equal Zero (Succ a) = False

instance IEqual (Succ a) Zero where
    type Equal (Succ a) Zero = False

Haskell会提示你实例1、3是矛盾的，实例2、4是矛盾的。

练习：

定义小于、大于操作（可以向IEqual接口添加方法，或者定义新的接口）
定义加法、乘法、减法运算

答案之一小于关系（因为还后面用到）：

class ILessThen a b where
    type LessThen a b :: *

instance ILessThen Zero Zero where
    type LessThen Zero Zero = False

instance ILessThen Zero (Succ a) where
    type LessThen Zero (Succ a) = True

instance ILessThen (Succ a) Zero where
    type LessThen (Succ a) Zero = False

instance ILessThen (Succ a) (Succ b) where
    type LessThen (Succ a) (Succ b) = LessThen a b

列表

我们这样定义列表：

空列表是列表
一个列表前加上一个元素得到的也是个列表

翻译到Haskell：

-- 空列表
data Nil

-- 一个元素h和另一个列表t的组合
data Cons h t

例子：

-- [1, 2, 3]
type List1 = Cons (One (Cons Two (Cons Three Nil)))

-- [1, 1, 2, 3]
type List2 = Cons Three List1

插入

下面要把一个元素插入到有序列表：

class IInsert a b where
    type Insert a b :: *

把一个元素插入到空列表：

instance IInsert x Nil where
    type Insert x Nil = Cons x Nil

处理非空列表时要根据大小比较选择相应的操作，我们可以增加一个布尔值作为参数，定义对非空列表的插入：

class IInsertCons b x y ys where
    type InsertCons b x y ys :: *

x表示新元素，y表示原列表的头节点，ys表示原列表的尾，b是表示x是否小于y的布尔值。根据这个我们就可以实现对非空列表的插入：

instance IInsertCons True x y ys where
    type InsertCons True x y ys = Cons x (Cons y ys)

instance IInsertCons False x y ys where
    type InsertCons False x y ys = Cons y (Insert x ys)

instance IInsert x (Cons y ys) where
    type Insert x (Cons y ys) = InsertCons (LessThen x y) x y ys

赶紧到ghci中测试一下：

ghci> :t undefined :: Insert One Nil
undefined :: Insert One Nil :: Cons (Succ Zero) Nil

ghci> :t undefined :: Insert Two (Cons One (Cons Three Nil))
undefined :: Insert Two (Cons One (Cons Three Nil))
  :: Cons (Succ Zero) (Cons (Succ One) (Cons (Succ Two) Nil))

完结

把type-level programming当Haskell入门想法是从外国一个牛人得到的，时间久了，没找着他。出于入门和完全隐藏value-level的目的，上面很多地方都比较含糊, 到后面就没编下去了。

例子来自Fun with functional dependencies，我只是改用Type Family实现，没太大差别。Fun with functional dependencies最后的例子插入排序，你可以试一下用TF实现。

我本来想在愚人节写的，那几天在忙其他事，拖到现在。愚人节写的不一定是假的，上面的例子都是测试过的，所以你大可放心。