光阴冢

We make choices and life has a way of making us pay for them.

Haskell 几题

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

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

几个证明

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

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

由于 Haskell 本身不是专门用来做证明的,因此一些常见的关系都需要自己实现。例如需要实现构造上的 Equal(在 Coq 中它是自动实现的):

-- 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 这个二元关系是个等价关系,具有对称性,传递性和自反性三个性质:

-- | 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:

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. 

翻译过来就是:

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)

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

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

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

例如:

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

意思是

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

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

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

以 List 数据结构为例,它的 Scott Encoding 是:

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

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

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

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 总是丑陋一点,相对于其他高阶函数,因为要比较两个列表的长度:

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 的定义:

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

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

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))

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

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 是一样的。

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

-- 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 * 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):

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

相应的,有

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 是同构的:

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 是很好构造的。

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