catamorphism

いい加減、Monadic Semanticsの勉強を真面目にしようと思って、
An Implementation of Modular Monadic Semantics using Folds and Monadic Folds
などを読んだら、Haskellが更にexoticなことができると知った

newtype Fix f = In (f (Fix f))
data NatF t = Zero | Suc t

instance Functor NatF where
 fmap f Zero = Zero
 fmap f (Suc n) = Suc(f(n))

type Nat = Fix NatF

Inは型構成子の一種、だと思う。多分。で、これが

data Nat = Zero | Suc Nat

と同等。というか、dataとtypeとnewtypeの使い分けが実はよく分かってない。typeは単なるaliasだと思うけど。まあいいや。

普通の不動点コンビネータは、

fix f = f (fix f)

で定義できて、Fixは型に対する不動点を定義する。自然数型Natは、型に関する方程式X=1+Xの解(1は()型で、+は型の直和)なので、NatF(X)=1+Xの不動点として、自然数型を定義できるとか、そういうイメージ。で、Fix使って、型を作っておくと、一般的な形でfoldが定義できるので、嬉しい(何が?)。foldはcatamorphismとか呼ばれて、圏論的バックグラウンドを持つらしい

type Algebra f a = f a -> a

fold::(Functor f) => (Algebra f a) -> Fix f -> a
fold g = g . fmap (fold g) . out
 where
  out (In x) = x

foldは、ここらへんで怪しいことを少し書いたことが。リストの場合は対応するのがfoldrで、ifも多分、Bool型に対するfoldと見なしていいんだと思う。大抵の言語では、ifを関数として扱うことはできないけれど、Haskellなどでは遅延評価のために、問題ない。

cond t f = (\p -> case p of {True->t;False->f;})
fact = (\n -> (cond 1 (n*fact(n-1))) (n==0))

これだと使いづらいので、

newtype Fix f = In (f (Fix f))
data NatF t = Zero | Suc t
type Nat = Fix NatF
type Algebra f a = f a -> a

zero = In Zero
suc::Nat -> Nat
suc = In . Suc
--out::Nat -> NatF Nat (実際のoutの型はもっと一般的)
out (In x) = x

instance Functor NatF where
 fmap f Zero = Zero
 fmap f (Suc n) = Suc(f(n))

nat_to_int::Nat->Integer
nat_to_int (In Zero) = 0
nat_to_int (In (Suc p)) = 1 + nat_to_int(p)

fold::(Functor f) => (Algebra f a) -> Fix f -> a
fold g = g . fmap (fold g) . out

とかやる。けど、NatをShowのinstanceにしようとすると、エラーになる。むー。とりあえず、fold使って足し算が定義できる

plus x y = fold (cata (out y) Suc) x
 where
  cata f1 f2 =
   (\m -> 
     case m of
       Zero -> In(f1)
       (Suc p) -> In(f2(p)))

テスト。

> nat_to_int(plus (suc(suc(suc(zero)))) (suc(suc(zero))))
5

足し算定義するだけで、大変過ぎる･･･。掛け算その他諸々も自由自在。いや、これだけだと、何の役に立つんだという話なんだけど。foldについては、何か色々等式が成り立つはずで、自明なのは、
fold (cata Zero Suc) = id
とか。一般的なfoldに対して、融合変換とかが働くので、最適化に役立つ(かもしれない)という話らしい。Natの場合は、そもそも上のように定義して計算すること自体効率が悪いけれども、リストとか二分木とか、その他、「プログラム言語の項」とか、そういう場合にはいいのかも。ところで、上のcataを自動的に生成できないものか。引数の数が不定だから無理か

それと、自然数の足し算とか、リスト操作関数(appendとか)の多くは、foldと型構成子とflipとか(.)みたいな基本的なコンビネータの組み合わせで書けるので、それらのコンビネータの間で成り立つ等式の変形のみで、結合法則とか証明できたりしないのかなー、とか思った

data Nat = Zero | Suc Nat
fold_nat :: a -> (Nat -> a) -> Nat -> a
fold_nat init f x = case x of
  Zero -> -> init
  (Suc n) -> (f (fold_nat init f n))

fix f = f (fix f)

--plus x y = fold_nat y Suc x
plus  = flip (flip fold_nat Suc)

とか定義して、以下はただのインチキだけど

plus x Zero = (flip fold_nat Suc) Zero x = fold_nat Zero Suc x = x

plus Zero = 
(\x -> fold_nat x Suc Zero)
= fold_nat (fold_nat Zero Suc Zero) (\n -> (fold_nat (Suc n) Suc Zero))
= fold_nat Zero (\n -> Suc (fold_nat n Suc Zero))
= fix (\f -> fold_nat Zero (Suc . f))
= id

基本的には、普通に、定理証明器でやってる帰納法を、そのままやるだけなんだけど

あと、部分型みたいなのは、欲しいと思ってたけど、

{-# OPTIONS -fglasgow-exts #-}
import Maybe
data Nat = Zero | Suc Nat

nat_to_int n = case n of
  Zero -> 0
  (Suc n) -> 1+(nat_to_int n)

class SubType sub sup where
 inj::sub -> sup -- injection
 prj::sup -> Maybe sub -- projection

instance SubType Nat Integer where
 inj = nat_to_int
 prj n |(n<0) = Nothing
       |n==0 = Just Zero
       |otherwise = Just (Suc ( fromJust (prj(n-1))))

とかやるといいらしい。余り使いやすいとはいえないけど

>(inj::Nat->Integer) (Suc Zero)
1