Hylomorphism

ここ数日で学習したこと

・私ごときが思いつく程度の疑問は、単なる勘違いか、とっくに解決されてるか、みんな疑問に思ってるけど難しいので敢えて口にしない、のどれかというオチ。しかし、別にプロの研究者ではないので、どうでもいいのだった。

というわけで、
http://www.ipl.t.u-tokyo.ac.jp/~onoue/pub/drthesis02.pdf
に色々書いてあった。

・fold/unfoldとかってどれくらい強力なんだろう？→(foldやunfoldの一般化である)Hylomorphismなら、普通使われる大抵の再帰関数を表現できるくらい強力らしい。algebraic type上の原始帰納的関数は、全てあるalgebraic type上のhylomorphismとして表現可能であるらしい(証明みてないが)

・普通に再帰的に書かれた関数から、foldやらbuildやら使った形式に変換できないんだろうか?→なんか色々アルゴリズムあるらしいです(アバウト)。十年近く前から

hylomorphismは、自然変換を恒等変換にとれば

hylo::(Functor f) => (f a -> a) -> (b -> f b) ->  b -> a
hylo phi  psi = phi .  (fmap $ hylo phi psi) . psi

自然変換も込みでやるなら

{-# OPTIONS -fglasgow-exts #-}
type NT f g = forall x. (f x) -> (g x) --関手fから関手gへの自然変換のつもり

hylo::(Functor f　、Functor g) => (g b -> b)  -> (NT f g) -> (a -> f a) -> a -> b
hylo phi eta psi = phi .  eta . (fmap $ hylo phi eta psi) . psi

-- hylo psi id phi :: (f a -> a) -> (b -> f b) ->  b -> a

とか？

NT f gは多分全然自然変換になってないと思うけど、いい方法が思いつかない(前のdinaturalityみたく、なんか"good model"取れば、上の定義で、ちゃんと自然変換になったりするのかな。まあよく分からんが、上の定義で実用上は困らなそうな。いやでも自然変換じゃないと融合変換が成立しなくなるのか)。

hylomorphismは、F余代数とG代数とFからGへの自然変換の3つ組を受け取って、F余代数のcarrierからG代数のcarrierへの射を作るけど、foldやunfoldと違って圏論的には余り面白いものではないような。何か普遍性を使った特徴づけがあるとよいんだけど(あるかもしれないけど。定義からして、ありそうな感じだし。そのうち考えるor調べる)。

{-# OPTIONS -fglasgow-exts #-}
newtype Fix f = In (f (Fix f))
out (In x) = x

type NT f g = forall x. (f x) -> (g x) 
hylo::(Functor f , Functor g) => (g b -> b)  -> (NT f g) -> (a -> f a) -> a -> b
hylo phi eta psi = phi .  eta . (fmap $ hylo phi eta psi) . psi

--Nat型定義
data NatF t = ZeroF | SucF t

instance Functor NatF where
 fmap f ZeroF = ZeroF
 fmap f (SucF n) = SucF(f(n))

type Nat = Fix NatF
zero = In ZeroF
suc = In . SucF

nat_to_int::Nat->Integer
nat_to_int (In ZeroF) = 0
nat_to_int (In (SucF p)) = 1 + nat_to_int(p)


--List型定義
data ListF a t = NilF | ConsF a t
instance Functor (ListF a) where
 fmap f NilF = NilF
 fmap f (ConsF x y) = ConsF x (f y)

type List a = Fix (ListF a)
nil = In NilF
cons x xs = In (ConsF x xs)

ltol :: List a -> [a]
ltol (In NilF) = []
ltol (In (ConsF x xs)) = x:(ltol xs)

_map :: (a -> b) -> (List a) -> (List b)
_map f = hylo In (mapNT f) out
 where
  mapNT :: (a -> b) -> (ListF a t) -> (ListF b t)
  mapNT f NilF = NilF
  mapNT f (ConsF m x) = ConsF (f m) x

test = ltol $ _map nat_to_int  $ _map suc (cons (suc zero) (cons zero nil))

_length :: List a -> Nat
_length  = hylo In lengthNT out
 where
  lengthNT :: (ListF a t) -> (NatF t)
  lengthNT NilF = ZeroF
  lengthNT (ConsF m xs) = SucF xs

test2 = nat_to_int $ _length (cons 1 $ cons 2 $ cons 3 nil)

私も晴れて、Ph.D haskellプログラマなようです。mapNTやlengthNTが、ばりばり手で与えてる感じなので、これだと、_length . (_map f) = _lengthすら言えない。うーん、がんばってhylomorphismによる表現さえ与えられれば、RULESプラグマのみで処理できないんだろうか