Hylomorphism(その2)

よく考えると(よく考えなくても)、Hylo-fusionをRULESプラグマのみで扱うのは無理がある。普通のプログラムをHylo3つ組形式に変換→融合変換→Hylo3つ組形式を展開、というプロセスで、2つ目と3つ目をRULESで処理しようとしても、本来融合変換できるはずのものが、展開されちゃうとか、そういうことが起きそうな気がする･･･。いや、phase-controlとか利用すればできるのかも

ま、とりあえず、そのへんは無視して、lengthNTやmapNTが泥臭いので、"basic functors and related combinators"で書かないといけないとか、そういう話だった。以下の話は基本的にここに書いてある話。

まず、NatFやListFを、Eitherとtupleの組み合わせで与える必要がある。んだけど、

type NatF t = Either () t
instance Functor NatF where
 ...

とかやっても、エラーになる・・・。Haskellつかえねー。type宣言って、本当にただのaliasとしてしか働かないんだなー。

仕方ないので、IsoTypeクラスを導入して、NatF tとEither () t 間の「同形写像」とかを自分で定義することにした。が、Haskellの型推論がアレなので、型を書かないと大抵推論に失敗するとか。Haskellつかえねー(2回目)。まあ、こんな感じで

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

--fold g = g . fmap (fold g) . out
--unfold g = In . fmap (unfold g) . g

--大人の事情で、GHCに勝手に型推論してもらうことに
{-
hylo::(Functor f , Functor g) 
       => (g b -> b)  -> (forall x.(f x)->(g x)) -> (a -> f a) -> a -> b
-}
hylo phi eta psi = phi .  eta . (fmap $ hylo phi eta psi) . psi

--簡易版
{-# RULES "hylo-shift-comp" forall p q. (hylo In p out) . (hylo In q out) = hylo In (p.q) out #-}
{-# RULES "hylo-shift"  forall p q x. hylo In p out (hylo In q out x) = hylo In (p.q) out x #-}


--型の同形
class IsoType t1 t2 where
  strip :: t1 -> t2
  equip :: t2 -> t1

{-# RULES "strip/equip" strip . equip = id #-}
{-# RULES "equip/strip" equip . strip = id #-}


--basic functors and related combinators
--cop:separated sum , cup:product
--split f g = <f,g> , junc f g = [f,g]
exl = fst 
exr = snd 
inl = Left 
inr = Right

cop :: (a -> c) -> (b -> d) -> (Either a b) -> (Either c d)
cop f g (Left x) = Left (f x)
cop f g (Right x) = Right (g x)

cup :: (a -> c) -> (b -> d) -> (a,b) -> (c,d)
cup f g (r,l) = (f r , g l)

junc :: (a -> c) -> (b -> c) -> Either a b -> c
junc f g (Left x) = (f x)
junc f g (Right x) = (g x)

split :: (a -> b) -> (a -> c) -> a -> (b,c)
split f g x = (f x , g x)

{-# RULES "hylo-redex1"  forall f g. exl . (cup f g) = f . exl #-}
{-# RULES "hylo-redex2"  forall f g. exr . (cup f g) = g . exr #-}
{-# RULES "hylo-redex3"  forall f g. exl . (split f g) = f #-}
{-# RULES "hylo-redex4"  forall f g. exr . (split f g) = g #-}
{-# RULES "hylo-redex5"  split exl exr = id #-}
{-# RULES "hylo-redex6"  forall f g h j. (cup f g) . (split h j) = (split (f . h) (g . j)) #-}
{-# RULES "hylo-redex7"  forall f g h j. (cup f g) . (cup h j) = (cup (f . h) (g . j)) #-}
{-# RULES "hylo-redex8"  forall f g h. (split f g) . h = (split (f . h) (g . h)) #-}
{-# RULES "hylo-redex9"  forall f g. (cop f g) . inl = inl . f #-}
{-# RULES "hylo-redex10" forall f g. (cop f g) . inr = inr . g #-}
{-# RULES "hylo-redex11" forall f g. (junc f g) . inl = f #-}
{-# RULES "hylo-redex12" forall  f g. (junc f g) . inr = g #-}
{-# RULES "hylo-redex13" junc inl inr = id #-}
{-# RULES "hylo-redex14" forall f g h j. (junc f g) . (cop h j) = (junc (f . h) (g . j)) #-}
{-# RULES "hylo-redex15" forall f g h j. (cop f g) . (cop h j) = cop (f . h) (g . j) #-}
{-# RULES "hylo-redex16" forall f g h. f . (junc g h) = (junc (f . h) (g . h)) #-}


--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

instance IsoType (NatF t) (Either () t) where
 strip ZeroF = Left ()
 strip (SucF p) = Right p
 equip (Left ()) = ZeroF
 equip (Right p) = (SucF p)

instance Show Nat where
 show n = show $ nat_to_int n

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)

instance IsoType (ListF a t) (Either () (a,t)) where
 strip NilF = Left ()
 strip (ConsF a x) = Right (a,x)
 equip (Left ()) = NilF
 equip (Right (a,x)) = (ConsF a x)

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 f = hylo In (mapNT f) out
mapNT :: (a -> b) -> (ListF a t) -> (ListF b t)
mapNT f = (equip::(Either () (a,t))->(ListF a t)) 
            . (cop id (cup f id)) 
            . (strip::(ListF b t) -> (Either () (b,t)))

_length = hylo In lengthNT out
lengthNT :: (ListF a t) -> (NatF t)
lengthNT = 
   equip . (cop id exr ) . (strip::(ListF a t) -> (Either () (a,t)))

ls = cons (suc zero) $ cons zero nil
main = print $ _length $ _map suc ls

で、こうしておけば

_length . (_map f) 
= {since dinition}
(hylo In (equip.(cop id exr).strip) out).(hylo In (equip.(cop id (cup f id)).strip) out)
= {since hylo shift law}
hylo In (equip.(cop id exr).(cop id (cup f id)).strip) out
= {since "hylo-redex15"}
hylo In (equip.( cop (id.id) (exr.(cup f id)) ).strip) out
= {since "hylo-redex2"}
hylo In (equip.(cop (id.id) (id.exr)).strip) out
= {since basic property of id}
hylo In (equip.(cop id exr).strip) out
= {By definition}
_length

とかなって、_length . (_map f) = _lengthくらいは、簡単に証明できる。。

というようなことを、わざわざ手で書いたのは、つまりGHCのRULESプラグマではうまくいかなかったからなんだけど

Main.lvl8 = Main.poly_hylo
              @ (Main.Fix (Main.ListF (Main.Fix Main.NatF)))
              @ (Main.ListF (Main.Fix Main.NatF) (Main.Fix (Main.ListF (Main.Fix Main.NatF))))
              @ (Main.Fix (Main.ListF (Main.Fix Main.NatF)))
              (Main.$WIn @ (Main.ListF (Main.Fix Main.NatF)))
              Main.lvl4
              (Main.out @ (Main.ListF (Main.Fix Main.NatF)))
              Main.lvl7

Main.lvl9 :: Main.Fix Main.NatF
[GlobalId]
[]
Main.lvl9 = Main.poly_hylo
              @ (Main.Fix Main.NatF)
              @ (Main.NatF (Main.Fix Main.NatF))
              @ (Main.Fix (Main.ListF (Main.Fix Main.NatF)))
              (Main.$WIn @ Main.NatF)
              Main.lvl3
              (Main.out @ (Main.ListF (Main.Fix Main.NatF)))
              Main.lvl8

ここまできておきながら〜!!Haskellつかえねー(3回目)。Conal Elliottが、どっかでGHCのsimplifierは複雑すぎて、展開されてほしいものがされなかったりして、わけわからんので、ダメぽとか書いてたけど、う〜ん(まあ、私がダメだとかいう可能性も否定できないけど)。hylo-redexはいけるようにみせかけて、実は、上で定義したRULESは関係ないとか。GHC本体の機能のみで勝手に最適化される(まあ、基本的にtrivialなルールなので、それはそれでいいんだと思う)

hylo-fusionは、fold/buildルールによるshortcut-fusionよりは、大分見通しがいいと思うけどな〜。でも、別に人間が手でやるのではなく、自動化したいので、見通しのよさは関係ないんだけど。しかし、RULESプラグマが使えないとなると、やっぱGHCに直接手を入れるしかないのか?それはしたくないよなー。どう考えても大変そうだし。あと、別の手として、-fext-coreで吐いたCoreに処理を施すという道がある。ExtCoreをRead/Writeする関数は、GHCに既にあるのでこれが一番楽かもしれない