## 几个证明

 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) 

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

 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!

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

 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))）产生了信息损失。

 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

 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 

## 一些感想

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