megrxu

Haskell 几题

Dec 12, 2019  「PL」  #Haskell #Formal Proofs #Functional Programming 

这几天在看 Concrete Semantics 的类型理论部分，于是想做一下之前没有做下去的 Codewars 上的几道 Haskell 题。

有空写写感想。现在忙着继续看 CS（

几个证明

前几个都是证明题，所以相对都很简单，尤其是已经在 Coq 中做过相同的证明之后。如果有 Coq 的源代码的话，就是一个翻译问题。

不过也因此更加深刻地理解了程序即证明。构造一个给定类型的函数，就是在写出这个类型对应的证明，即柯里-霍华德同构（Curry–Howard Isomorphism）。

由于 Haskell 本身不是专门用来做证明的，因此一些常见的关系都需要自己实现。例如需要实现 Equal：

1
2
3
4
5

-- Preload
-- | Predicate describing equality of natural numbers.
data Equal :: * -> * -> * where
    EqlZ :: Equal Z Z
    EqlS :: Equal n m -> Equal (S n) (S m)

而例如利用 Equal 关系进行的替代，Coq 中只需要写 simpl，但是 Haskell 中也需要自己定义一个函数，以便把该类型/命题转化到另一个「等价」类型/命题上。Equal 这个二元关系是个等价关系，具有对称性，传递性和自反性三个性质：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

-- | For any n, n = n.
reflexive :: Natural n -> Equal n n
reflexive NumZ = EqlZ
reflexive (NumS n) = EqlS $ reflexive n

-- | if a = b, then b = a.
symmetric :: Equal a b -> Equal b a
symmetric EqlZ = EqlZ
symmetric (EqlS eq) = (EqlS $ symmetric eq)

-- | if a = b and b = c, then a = c.
transitive :: Equal a b -> Equal b c -> Equal a c
transitive EqlZ EqlZ = EqlZ
transitive (EqlS eq1) (EqlS eq2) = (EqlS $ (transitive eq1 eq2))

定义了这些之后，后面的证明就简单了。当真就是把 Coq 翻译到 Haskell。

例如 Coq：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

Lemma plus_n_O : forall n : nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Lemma plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m. 
  induction n as [| n' sn']. (* by induction on n *)
  - reflexivity.
  - simpl. rewrite -> sn'. reflexivity. Qed.

翻译过来就是：

1
2
3
4
5
6
7

plus_n_Z :: Natural n -> Equal (n :+: Z) (n)
plus_n_Z NumZ = EqlZ
plus_n_Z (NumS n) = EqlS (plus_n_Z n) -- by induction on n

plus_n_Sm :: Natural n -> Natural m -> Equal (S (n :+: m)) (n :+: (S m))
plus_n_Sm NumZ m = reflexive (NumS m)
plus_n_Sm (NumS n) m = EqlS (plus_n_Sm n m) -- by induction on n

如果是好几个的等价关系转换，只要手写下来当前的证明状态/中间类型，然后连续使用 transitive 就可以了。也可以写成中缀表达式的形式方便描述。

Scott Encoding

Scott encoding 可以使用 lambda 演算来表述数据结构，甚至是递归的数据结构，例如 List ，Nat等。题目中是已经给出了 Encoding 的构造，相对来说比较简单。但是对于之前没有接触过 Haskell 语法的我还是有点难度。（之前只知道 Haskell 可以方便地作 sum type 和 composition）

一开始读懂这个就费了很大劲：

1

newtype SMaybe a = SMaybe { runMaybe :: forall b. b -> (a -> b) -> b }

后来查阅资料发现，Haskell 的 newtype 构造的类型中，只能允许一个构造子。原因是这样的话，构造子和该类型实际上是同构的，在编译之后完全可以当作一个东西进行处理。即在 type-checker 的时候是一个抽象，但是在 runtime 的时候是相同的。

例如：

1

newtype State s a = State { runState :: s -> (s, a) }

意思是

1
2

State :: (s -> (s, a)) -> State s a
runState :: State s a -> (s -> (s, a))

意味着这两个类型可以相互转换。定义 newtype 实际上也是在定义一个转换函数转换到这个新定义的类型。这里的同构在后面的习题中也会遇到。

理解了 SMaybe 等函数的类型以后，之后的工作就相对较为简单了。粗暴一点来说就是作类型演算，找到对应的那个函数。当然，除了瞎猜以外也是有规律可循的。这个规律就是 Patten Matching。

以 List 数据结构为例，它的 Scott Encoding 是：

1
2
3

newtype SList a = SList { 
  runList :: forall b. b -> (a -> SList a -> b) -> b 
}

构造子接受两个参数，一个是任意类型 b，一个是函数，该函数将接受一个 a 和一个 SList a 再转换到 b 类型，最终转换到 b。对于 List 数据结构来说，它要么是空的（[]），要么是一个元素加一个列表（[x:xs]）。所以显而易见，这个模式匹配就是从这两种情况来进行的。如果是空的话，则返回第一个元素，如果不是空的，则将 x 和 xs 应用给第二个函数就可以了。

对于 List 的操作的核心想法就是这样了，具体的实现例如：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

toList :: SList a -> [a]
toList (SList l) = l [] (\x xs -> (x: toList xs))

nils = SList (\n _ -> n)
fromList :: [a] -> SList a
fromList [] = nils
fromList (x:xs) = SList (\_ c -> c x $ fromList xs)

concat :: SList a -> SList a -> SList a
concat (SList l1) sl2 = l1 sl2 (\x xs -> cons x (concat xs sl2))

map :: (a -> b) -> SList a -> SList b
map f (SList l) = l nils (\x xs -> cons (f x) (map f xs))

foldl :: (b -> a -> b) -> b -> SList a -> b
foldl fl i (SList l) = l i (\x xs -> (foldl fl (fl i x) xs))
foldr :: (a -> b -> b) -> b -> SList a -> b
foldr fr i (SList l) = l i (\x xs -> fr x (foldr fr i xs))

可见，肆无忌惮地递归就是了！

然而在实现 zip 的时候，遇到了一点问题。因为 zip 总是丑陋一点，相对于其他高阶函数，因为要比较两个列表的长度：

1
2
3
4
5

zip :: SList a -> SList b -> SList (SPair a b)
zip sl1@(SList l1) sl2@(SList l2) = (case (null sl1) || (null sl2) of
  True -> nils
  False -> cons (SPair a b) (zip t1 t2) )
    where (Just a, Just b, t1, t2) = (heads sl1, heads sl2, tails sl1, tails sl2)

Isomorphism!

然后就是两道同构题。上一节提到了，newtype 关键字实际上就是在建立一个类型抽象到它的构造的同构。这两道题将对这个概念更深入地了解。

对于 ISO 的定义：

1

type ISO a b = (a -> b, b -> a)

可以看到，就是一个函数对，表示两个类型相互之间可以进行推导。在此基础上，可以对类型的计算结果进行构造同构了。然而，走到这里，发现和第一部分的证明又有异曲同工之妙了。同构本身也是一个等价关系，因此也是 reflexive，symmetric 和 transitive 的。除此之外，只要没有信息损失，相应的类型组合都是可以构造同构出来的。例如：

1
2
3
4
5
6

isoTuple :: ISO a b -> ISO c d -> ISO (a, c) (b, d)
isoTuple (ab, ba) (cd, dc) = 
  (\(a, c) -> (ab a, cd c), \(b, d) -> (ba b, dc d))

isoFunc :: ISO a b -> ISO c d -> ISO (a -> c) (b -> d)
isoFunc (ab, ba) (cd, dc) = (\f -> (cd . f . ba), \f -> (dc . f . ab))

但是，从另一个方向是不可行的，虽然我们可以实现它，但是有些情况下会报错：

1
2
3
4
5
6
7
8

isoUnMaybe :: ISO (Maybe a) (Maybe b) -> ISO a b
isoUnMaybe (mab, mba) = (ab, ba) where
    ab a = case mab (Just a) of 
                 Just b -> b
                 _ -> fromJust $ mab Nothing
    ba b = case mba (Just b) of
                 Just a -> a
                 _ -> fromJust $ mba Nothing

fromJust 函数应用 Nothing 的时候会产生 error 。因为某个方向上（从 ISO a b 到 ISO (Maybe a) ((Maybe b))）产生了信息损失。

代数同构部分的题目将同构扩展到了（或者说解释到了）代数域上。例如乘法（类型做一个 Tuple），加法（给类型包一个 Either），幂次（把类型组合成函数）等。之后就如同前面证明题一样，证明一些乘法交换律，加法结合律等等就好了。因为同构本身就是个等价关系，与之前定义的 Equal 是一样的。

然而神奇的一点就在这里产生了，我们在证明/构造这些定理/函数的时候，有两种方法：一种是从同构的定义的角度进行编写，例如：

1
2
3

-- a * b * c = a * (b * c)
multAssoc :: ISO ((a, b), c) (a, (b, c))
multAssoc = (\((a, b), c) -> (a, (b, c)), \(a, (b, c)) -> ((a, b), c))

一种是组合之前的定理/函数，并应用在输入上：

1
2
3
4
5
6
7
8

-- 1 * b = b
multSO :: ISO ((), b) b
multSO =
  isoProd one refl `trans`
  multS `trans`
  isoPlus refl multO `trans`
  plusComm `trans`
  plusO

这两个在类型演算上是等价的，但是在表述上的意义却有所不同！第二种更类似于我们的正常证明，就如同前几道题中所作的那样。

Peano and Church

类似地，同一个代数概念也可以有很多种表示方法。比如自然数。这道题里使用四种不同的构造来构造一个 Nat 类。不同的是，有些通用的计算模型亦被抽象出来了，例如 induction。在前文中，我们都直接使用递归来实现，但是在这个小节中，加法，乘法等具体实现都可以使用 induction 来直接构造。这个思想也可以应用到之前的证明上，即在 Haskell 中实现一个类似 Coq 中的 induction 的 tactic！

Algebraic Data Type(ADT):

1

data Peano = O | S Peano deriving (Show, Eq, Ord)

相应的，有

1
2
3
4
5
6
7

instance Nat Peano where
-- ... omitted
  iter a _ O = a
  iter a f (S n) = iter (f a) f n
  plus n = iter n successor
  mult x = iter zero (plus x)
  pow x = iter (successor zero) (mult x)

[()]

[()] 方面和第一种几乎是一样的。因为 [()] 和 Peano 是同构的：

1
2
3
4
5
6

list_peano :: ISO [()] Peano
list_peano = (f, g) where
  f [] = O
  f [_:xs] = S (f xs)
  g O = []
  g (S n) = [():(g n)]

Scott Encoding 和 Church Encoding

Scott 的核心思想是通过 Pattern Matching，Church 则是通过 induction。后面有一些文献可以用来辅助作这个。

一些辅助函数

liftISO2 同构我是构造了很久才猜出来。虽然一个 lift 是很好构造的。

1
2
3
4
5
6
7
8
9

liftISO :: ISO a b -> ISO (a -> a) (b -> b)
liftISO (ab, ba) = (f, g) where
  f = \h -> ab . (. ba) h
  g = \h -> ba . (. ab) h

liftISO2 :: ISO a b -> ISO (a -> a -> a) (b -> b -> b)
liftISO2 (ab, ba) = (f, g) where
  f = \h -> (ab .) . (. ba) . (. ba) h
  g = \h -> (ba .) . (. ab) . (. ab) h

现在终于理解了，其实 composition 也是一个简单函数而已。同样可以偏应用。

一些感想

  • 递归真爽，induction 真爽。
  • 某些时候，在 haskell 里面 pattern matching 可以悄悄不必是 exhaustive 的。

Scott/Church Encoding 部分的参考