Hylomorphism(その3)

結局、ダメなのは私だったという話。コメントで教えていただいた通りやったらできた。

{-# OPTIONS -fglasgow-exts #-}
newtype Fix f = In (f (Fix f))
out (In x) = x
{-# NOINLINE out #-} --必要ないけど、Core出力見るときに便利とか

--確認用
{-
fold :: forall f.(Functor f) => (forall x.(f x -> x) -> (Fix f) -> x)
fold g = g . fmap (fold g) . out
unfold :: forall f.(Functor f) => (forall x.(x -> f x) -> x -> (Fix f))
unfold g = In . fmap (unfold g) . g
fold f  = hylo f id out
unfold f = hylo In id f
-}

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

--簡易版
{-# RULES "hylo-shift" 
    forall (p :: forall x. g x -> h x) (q :: forall x. f x -> g x) a. 
      hylo In p out (hylo In q out a) = hylo In (p.q) out a #-}


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

--{-# RULES "strip/equip" forall x . strip  (equip x) = x #-}
--{-# RULES "equip/strip" forall x . equip  (strip x) = x #-}


--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 x. exl (cup f g x) = f (exl x) #-}
{-# RULES "hylo-redex2"  forall f g x. exr (cup f g x) = g (exr x) #-}
{-# RULES "hylo-redex3"  forall f g x. exl (split f g x) = f x #-}
{-# RULES "hylo-redex4"  forall f g x. exr (split f g x) = g x #-}
{-# RULES "hylo-redex5"  split exl exr  = id #-}
{-# RULES "hylo-redex6"  forall f g h j x. cup f g (split h j x) = (split (f . h) (g . j) x) #-}
{-# RULES "hylo-redex7"  forall f g h j x. cup f g (cup h j x) = (cup (f . h) (g . j) x) #-}
{-# RULES "hylo-redex8"  forall f g h x. split f g (h x) = split (f . h) (g . h) x #-}
{-# RULES "hylo-redex9"  forall f g x. cop f g (inl x) = inl (f x) #-}
{-# RULES "hylo-redex10" forall f g x. cop f g (inr x) = inr (g x) #-}
{-# RULES "hylo-redex11" forall f g x. junc f g (inl x) = f x #-}
{-# RULES "hylo-redex12" forall f g x. junc f g (inr x) = g x #-}
{-# RULES "hylo-redex13" junc inl inr = id #-}
{-# RULES "hylo-redex14" forall f g h j x. junc f g (cop h j x) = junc (f . h) (g . j) x #-}
{-# RULES "hylo-redex15" forall f g h j x. cop f g (cop h j x) = cop (f . h) (g . j) x #-}
--hylo-redex16はhがstrictでないと成立しないので、コメントアウトしておく
--{-# RULES "hylo-redex16" forall f g h. h .(junc f g) = junc (h.f) (h.g) #-}

{-# NOINLINE [1] exl #-}
{-# NOINLINE [1] exr #-}
{-# NOINLINE [1] cop #-}
{-# NOINLINE [1] cup #-}
{-# NOINLINE [1] junc #-}
{-# NOINLINE [1] split #-}
{-# NOINLINE [1] inl #-}
{-# NOINLINE [1] inr #-}

--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 = stripList
 equip = equipList

stripList NilF = Left ()
stripList (ConsF a x) = Right (a,x)
equipList (Left ()) = NilF
equipList (Right (a,x)) = ConsF a x


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

_map f = hylo In (mapNT f) out
 where
  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
 where
  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)
--main = print $ _length $ _map suc ls 
--main = print $ _length . (_map suc) $ ls

Coreが

Main.lvl3 :: forall x_a2jv.
             Main.ListF (Main.Fix Main.NatF) x_a2jv -> Main.NatF x_a2jv
[GlobalId]
[Arity 1
 NoCafRefs]
Main.lvl3 = \ (@ x_a2jv) (x_a2TY :: Main.ListF (Main.Fix Main.NatF) x_a2jv) ->
              case (Main.NatF x_a2jv) x_a2TY of wild_X1v {
                Main.NilF -> Main.ZeroF @ x_a2jv;
                Main.ConsF a_a1d9 x1_a1da -> Main.SucF @ x_a2jv x1_a1da
              }

------------------------------------

Main.lvl7 :: Main.Fix Main.NatF
[GlobalId]
[]
Main.lvl7 = Main.hylo1
              (Main.$WIn @ Main.NatF)
              Main.lvl3
              (Main.out @ (Main.ListF (Main.Fix Main.NatF)))
              Main.lvl6

こんな感じに。勝った！第三部完!

hylo shiftさえうまく発動すれば、strip/equipの消去くらいは、GHCが頑張ってやってくれるような気もする。確信はないが(それでいいのか)。問題は、"_length $ _map suc ls"や"_length . (_map suc) $ ls"だとうまくいかないっぽい。Simplifier phase 2で、($)や(.)が展開されると同時に、hyloが引数に応じてpoly_hylo_s2RWとpoly_hylo_s2s0に特殊化(?と呼ぶのかなんと言えばいいのか)されて、RULESが適用されなくなってる感じっぽい。う〜ん、RULESプラグマは面白いと思うんだけど、使いこなすの大変だなー。length/mapくらいはうまくいったけど、もっと複雑になったらどうなるやら。結局合流性が保証されない限りは、ユーザの意図と違う変換が起こるのは避けられない。まあ、この手の悩みは、OnoueのD論にもグチグチ書いてあって、ある最適化の前に、別の最適化を挿入すると、本来最適化されるはずのものが最適化されなくなったりetc...単純な項書換え系なら、合流性を保証することもできるかもしれないけど(完備化が停止するかどうかはわからんけど)、最適化には、多分項書換えで書けない類の大域的な変換(strictness analysisとか)も含まれてるだろうし。このへんは、ad hocにやってたのでは、どうにもならんかもわからんね

よいニュース。RULESプラグマのforallで束縛した変数に型が指定できるというのは、僥倖。これによって、(practical)Acid Rain Theorem(つまり、cata-hylo fusionlawとhylo-ana fusion law)が自然に書ける

{-# RULES "cata/hylo" 
  forall (tau::forall a.(f a -> a)->f' a -> a) 
         (eta1::forall a.g a->f a) (eta2::forall a.f' a -> h a) phi psi x.
          hylo phi eta1 out (hylo (tau In) eta2 psi x) = hylo (tau (phi.eta1)) eta2 psi x #-}

{-# RULES "ana/hylo"
  forall (sigma::forall a.(a -> f a)-> a ->f' a) 
         (eta1::forall a.g a->f a) (eta2::forall a.f' a -> h a) phi psi x.
          hylo phi eta1 (sigma out) (hylo In eta2 psi x) = hylo phi eta1 (sigma (eta2.psi)) x #-}

ながいよ！ちゃんと機能するのかい、これ･･･。まあ、tauとかsigmaの型が指定できてよかったという話。尤も、それできないと、fold/buildルール書けないじゃん！って話で

{-# RULES
"fold/build" 	forall k z (g::forall b. (a->b->b) -> b -> b) . 
		foldr k z (build g) = g k z

"foldr/augment" forall k z xs (g::forall b. (a->b->b) -> b -> b) . 
		foldr k z (augment g xs) = g k (foldr k z xs)

........

"augment/build" forall (g::forall b. (a->b->b) -> b -> b)
		       (h::forall b. (a->b->b) -> b -> b) .
		       augment g (build h) = build (\c n -> g c (h c n))
"augment/nil"   forall (g::forall b. (a->b->b) -> b -> b) .
			augment g [] = build g
 #-}

これ何回も見てるのに、気付いてなかったわたしがアホ

ようやく、parametricity theoremというのが理解できてきた(今まで理解せず何を書いてたんだ?)けど、Acid Rain theoremの証明には、parametricity theoremが使われてるので、seqとかが絡んでくると、Acid Rain theoremは破れることになるのか?自信ないけど、例は少し考えれば構成できるはず(参考)