F-algebra と catamorphism を Haskell で理解する(2)
前回の続き。
wikipedia の F-algebra のページ http://en.wikipedia.org/wiki/F-algebra 参照。
上記ページに F(X) = 1 + X という関手の F-algebra の例で (N,[zero,succ]) が出てくる。Haskell で書くと
type N = Int a :: Maybe N -> N a Nothing = 0 a (Just x) = x + 1
本当は N は自然数なので負の数も入っている Int とは違うけれどここでは Int でごまかしておく。
a Nothing = 0 の部分が zero に、a (Just x) = x + 1 の部分が succ に対応する。
さて F-algebra (N,a) から別の F-algebra (B,b)
b :: Maybe B -> B
に対する射 f はどんなものになるだろう。
a は全単射なので逆写像 inv_a をとることができる。
inv_a :: N -> Maybe N inv_a 0 = Nothing inv_a x = Just (x-1)
逆写像なので
a・inv_a == id
F-algebra の射 f が満たすべき性質
f・a == b・F(f)
に右から inv_a をつなぐと
f・a・inv_a == b・F(f)・inv_a
a・inv_a == id だから
f = b・F(f)・inv_a これと Maybe の fmap f の性質 fmap f Nothing == Nothing fmap f (Just x) == Just (f x)
を使って
f 0 == b $ fmap f $ inv_a 0 == b $ fmap f Nothing == b Nothing f x == b $ fmap f $ inv_a x == b $ fmap f (Just (x-1)) == b (Just (f (x-1))) == (b.Just) (f (x-1)) つまり f :: N -> B f 0 = b Nothing f x = (b.Just) (f (x-1))
具体的にみていくと
f 1 == (b.Just) (f 0) == (b.Just)$b Nothing f 2 == (b.Just) (f 1) == (b.Just)$(b.Just)$b Nothing f 3 == (b.Just) (f 2) == (b.Just)$(b.Just)$(b.Just)$b Nothing ... なので f x は b Nothing に (b.Just) をx回適用した値、 つまり iterate を使って書くと f :: N -> B f x = (!!x) $ iterate (b.Just) $ b Nothing
例えば B として Int、b として
b :: Mabye Int -> Int b Nothing = 1 b (Just x) = 2 * x
とすると F-algebar (N,a) から F-algebra (Int,b) への射 f は
f :: N -> Int f x = (!!x) $ iterate (2*) 1
と一意に定まる。(実際には f x = 2^x である)
この F-algebra (N,[zero,succ]) ように任意の F-algebra に対して射が必ず存在して一意であるときこの F-algebra は initial algebra と呼ばれる。initial algebra は F-algebra のなす圏での始対象(initial object) であることと同じ意味である。
また initial algebra からの射(必ず存在して一意)を catamorphism と呼ぶ。
上の例でいえば
f :: N -> Int f x = (!!x) $ iterate (2*) 1
は F-algebra (Int,b) への catamorphism である。
ところで F-algebra の射 f が満たすべき性質
f・a == b・F(f)
の両辺を Just x に作用させると
f (a (Just x)) == b (Just (f x))
Just は空気のような存在だと思えば大体
f・a == b・f
である。この式や「x回適用」という方法どこかで見たことがあると思ったら圏論勉強会 でやった Conceptual Mathematics の session 11 1 S○圏(実際はSの右上にくるっとした矢印)圏の定義や session 15 3 Naming arbitrary elements にでてきていた。
Conceptual Mathematics 深いなあ。
多分また続く。