Await 做些相當庸俗的夢

Haskell 幾題

這幾天在看 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 演算來表述資料結構,甚至是遞迴的資料結構,例如 ListNat等。題目中是已經給出了 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])。所以顯而易見,這個模式匹配就是從這兩種情況來進行的。如果是空的話,則返回第一個元素,如果不是空的,則將 xxs 應用給第二個函式就可以了。

對於 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 bISO (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 中的 inductiontactic

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