這幾天在看 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 部分的參考