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 部分的參考