Unfold Fusion

一直沒辦法感受 coinduction 的直覺意義。在豁然貫通的那一個時刻來臨以前，最簡單的方式大概就是用 unfold fusion 嘍，因為 category theory 裡面的 duality 很明確很好操作，只要把 inductive datatypes 那一套的箭頭全部反過來就行了。

第一個 coinductive proof 當然是

map f . iterate f = iterate f . f        (*)

我們需要一些基本定義（in Haskell）。

-- constructor
-- Maybe (A, B) is isomorphic to 1 + A * B
alpha :: Maybe (a, [a]) -> [a]
alpha Nothing       = []
alpha (Just (a, t)) = a : t

-- deconstructor
ahpla :: [a] -> Maybe (a, [a])
ahpla []       = Nothing
ahpla (x : xs) = Just (x, xs)

-- products
split f g a = (f a, g a)
cross f g   = split (f . fst) (g . snd)

-- base functor
listrF f g Nothing       = Nothing
listrF f g (Just (a, t)) = Just (cross f g (a, t))

接著是一些 coinductive lists 的相關定義。

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
unfoldr f = alpha . listrF id (unfoldr f) . f

-- type functor
mapana :: (a -> b) -> [a] -> [b]
mapana f = unfoldr (listrF f id . ahpla)

iterate :: (a -> a) -> a -> [a]
iterate f = unfoldr (Just . split id f)

為了對稱，我們把 inductive lists 的相關定義重寫一遍。

foldr :: (Maybe (a, b) -> b) -> [a] -> b
foldr f = f . listrF id (foldr f) . ahpla

mapcata :: (a -> b) -> [a] -> [b]
mapcata f = foldr (alpha . listrF f id)

以上其實就是莊老師在 FLOLAC '07 講的一部份東西。真恐怖，FLOLAC 花了快一年時間都還沒消化完 XD。

Inductive lists 有 fusion law

h . foldr f = foldr g    <=    h . f = g . listrF id h

以及雖為特例但很好用的 type functor fusion law

foldr f . mapcata g = foldr (f . listrF g id)

現在把 function composition 的方向顛倒，就直接得到 coinductive lists 的 fusion law 和 type functor fusion law！

unfoldr f . h = unfoldr g    <=    f . h = listrF id h . g

mapana g . unfoldr f = unfoldr (listrF g id . f)

我沒預期要鋪這麼多路 XD。Anyway，(*) 式左邊可直接從 type functor fusion law 得到：

  map f . iterate f
=   { definition of iterate }
  map f . unfoldr (Just . split id f)
=   { type functor fusion }
  unfoldr (listrF f id . Just . split id f)
=   { definition of listF }
  unfoldr (Just . cross f id . split id f)
=   { product functor }
  unfoldr (Just . split f f)

右邊很自然地湊湊看 fusion condition：

  (Just . split id f) . f
=   { split fusion }
  Just . split f (f . f)
=   { product functor }
  Just . cross id f . split f f
=   { definition of listrF }
  listrF id f . Just . split f f
=   { let g = Just . split f f }
  listrF id f . g

所以依 fusion law 就得到

iterate f . f = unfoldr (Just . split f f)

於是 (*) 式兩邊都等於同一個 unfold，證畢。Coinduction 大概就先這樣弄吧 XD。

--
寫完才發現 this post should have been written in English XD。