日々の流転

λ. DrHylo: A tool for deriving hylomorphisms

DrHylo is a tool for deriving hylomorphisms from a restricted Haskell syntax. It is based on the algorithm first presented in the paper Deriving Structural Hylomorphisms From Recursive Definitions at ICFP'96 by Hu, Iwasaki, and Takeichi. The generated code can be run with Pointless Haskell, allowing the visualization of the recursion trees of Haskell functions.

【2009-11-04 追記】 まず、ホームページにある以下の例を試してみる。

module Sample where

swap :: (a,b) -> (b,a) 
swap (x,y) = (y,x) 

data Nat = Zero | Succ Nat 

len :: [a] -> Nat 
len [] = Zero 
len (h:t) = Succ (len t)

これに対して、DrHylo -iSample.hs とすると、以下のような感じでhylomorphismの三つ組み表現で出てきて、「おー！」という感じ。

{-# LANGUAGE TypeFamilies #-}
module Sample where
import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.RecursionPatterns

swap :: (a, b) -> (b, a)
swap = app . (((curry ((snd . snd) /\ (fst . snd))) . bang) /\ id)

data Nat = Zero
         | Succ Nat

type instance PF Nat = (:+:) (Const One) Id

instance Mu Nat where
        inn (Left (_)) = Zero
        inn (Right (v1)) = Succ v1
        out (Zero) = Left (_L)
        out (Succ v1) = Right (v1)

len :: [a] -> Nat
len
  = hylo
      (_L :: Fix ((:+:) (Const One) Id))
      (app . (((curry (app . ((eithr . ((curry (inn . (inl . bang))) /\ (curry (inn . (inr . snd))))) /\ snd))) . bang) /\ id))
      (app . (((curry (app . ((eithr . ((curry (inl . bang)) /\ (curry (inr . (snd . snd))))) /\ (out . snd)))) . bang) /\ id))

ただ、以下のような関数

plus :: Nat -> Nat -> Nat
plus m Zero = m
plus m (Succ n) = Succ (plus m n)

に対しては、

plus :: Nat -> Nat -> Nat
plus = app . (((fix . (curry (curry (curry (app . ((eithr . ((curry (fst . (((snd . fst) . fst) /\ (snd . fst)))) /\ (curry (inn . (inr . (app . ((app . ((((snd . fst) . fst) . fst) /\ (fst . (((snd . fst) . fst) /\ (snd . fst))))) /\ snd))))))) /\ (out . (snd . ((snd . fst) /\ snd))))))))) . bang) /\ id)

となってしまって、hylomorphismを導出できない。 他にも色々試してみたが、思ったほどにはhylomorphismを導出できない感じ。