日記 (2019 年 11 月 28 日)

11 月 16 日では、 下方射と上方射の数学的な定式化を行った。 今回は、 これらを Haskell でどう定義できるかを見ていきたいと思う。

実装を見る前に、 始代数の重要な性質を 1 つ証明する。

命題 3.1.

󰒚 上の自己関手 F:󰒚󰒚 をとる。 F-代数 (S,σ) が始代数ならば、 σ は同型射である。

証明.

(S,σ)F-始代数であるとする。 (FS,Fσ)F-代数であるから、 図式 FSFFSSFSFffσFσ を可換にする射 f が一意に存在する。 すると、 FSFSSSF(σf)σfσσ が可換になるから、 σf:SS は代数の射である。 一方、 id:SS も明らかに代数の射である。 このような射は一意でなければならないので、 σf=id が成り立つ。 また、 最初の図式の可換性により、 fσ=F(σf)=id も成り立つ。 以上により、 fσ の逆射になるから、 σ は同型射である。

つまり、 F-始代数 (S,σ)SFS を満たすということなので、 F の不動点であると見なすことができる。 さらに、 別の F-代数があるとそれに向かって射が伸びることから、 F-始代数は F の不動点の中でも最小不動点であると言うことができる。 双対的に、 F-終余代数は F の最大不動点である。

では、 これをもとに Haskell で実装していこう。 以下では GHC 拡張の MultiParamTypeClasses と FlexibleInstances あたりの機能を利用するので、 実行したい場合はこれらを有効にしておくこと。

まず、 型情報を読みやすくするため、 代数の型 f a -> aAlgebra f a という別名を付けておく。

type Algebra f a = f a -> a

関手 f に対する始代数は、 以下のように定義できる。

class Functor f => Fix f s where
inF :: f s -> s
outF :: s -> f s

既存の型を始代数と見なせるように、 ここでは型クラスとして定義することにした。 この実装は、 先程述べた始代数 (や終余代数) が関手の不動点になっているという観察から来ている。 sinF のペアが始代数であり、 outFinF の逆射を与えているわけである。 ただし、 実際に逆射になっているかどうかを Haskell の型で確認させることはできないので、 この点は実装者に委ねられていることには注意すること。

下方射の実装は以下のようになる。

cata :: Fix f s => Algebra f a -> s -> a
cata alg = alg . fmap (cata alg) . outF

この式はまさに、 下方射が満たすべき可換図式 f sf asafmap (cata alg)cata alginFoutFalg そのものである。 定義式の右辺に cata alg が出てきてしまっているが、 Haskell では遅延評価が採用されているので、 これで定義が可能なのである。

では、 この下方射の実装を実際に使ってみよう。 11 月 16 日と同じく、 ある V を固定して、 FV: A 1+V×A という形の関手を考えることにする。 この関手は以下のように実装できる。

data FList v a = Nil | Cons v a
instance Functor (FList v) where
-- fmap :: (a -> b) -> FList v a -> FList v b
fmap func Nil = Nil
fmap func (Cons val rest) = Cons val (func rest)

FV-始代数とは V の要素から成るリストであった。 実際、 以下のようにリスト型を Fix のインスタンスにすることができる。

instance Fix (FList v) [v] where
-- inF :: FList v [v] -> [v]
inF Nil = []
inF (Cons val rest) = val : rest
-- outF :: [v] -> FList v [v]
outF [] = Nil
outF (val : rest) = Cons val rest

下方射を得るためには、 別の FV-代数が必要である。 ここでは、 VInt とし、 0 を初期値とした加算を行う代数を考えてみる。

algPlus :: Algebra (FList Int) Int
algPlus Nil = 0
algPlus (Cons val rest) = val + rest

では、 algPlus による下方射に適当なリストを渡して実行してみよう。

cata algPlus ([8, 7, 4, 6, 9] :: [Int])
cata algPlus ([128, 580, 401, 952, 757] :: [Int])
34 2818

この通り、 リストに含まれる数値の和が得られた。

さらに、 特に V がユニット型の場合は、 FV-始代数は自然数全体になる。 実際、 以下のように Fix のインスタンスを定義することが可能だある。 なお、 Haskell には自然数型が存在しないので Int で代用し、 負数が渡された場合の挙動は考えないことにする。

instance Fix (FList ()) Int where
-- inF :: FList () Int -> Int
inF Nil = 0
inF (Cons _ num) = num + 1
-- outF :: Int -> FList () Int
outF 0 = Nil
outF num = Cons () (num - 1)

代数としては、 何らかの関数を固定した上で、 1 を初期値としてその関数を適用するようなものを考えてみる。

algRep :: (Int -> Int) -> Algebra (FList ()) Int
algRep func Nil = 1
algRep func (Cons _ num) = func num

実行する。

cata (algRep (* 2)) (10 :: Int)
cata (algRep (+ 4)) (1000 :: Int)
1024 4001

このように cata (algRep func) は引数に渡された回数分だけ 1 に func を適用する関数になる。

さて、 終余代数と上方射もほとんど同様に実装できる。 Haskell では、 上で定義した Fix f t のインスタンスが始代数としても終余代数としても振る舞うという性質があるため、 以下のようにすれば良い。

type Coalgebra f c = c -> f c
ana :: Fix f t => Coalgebra f c -> c -> t
ana coalg = inF . fmap (ana coalg) . coalg

Fix f t が始代数にも終余代数にもなるという事実は、 更なる 「何とか morpshism」 であるところの hylomorphism や metamorphism を定義するのに重要になってくる。 これについては次の機会で触れたいと思う。