Trick Shortcut Sync

Question

This problem occurred while trying to merge intermediate tricks in Haskell.

Consider a trie for Peano natural numbers:

data Nat = Zero | Succ Nat data ExpoNat a = ExpoNat (Maybe a) (ExpoNat a) | NoExpoNat 

We can easily define a fold on ExpoNat (this is essentially a list) and use foldr / build (aka finally without tags ) to prevent ExpoNat :

 {-# NOINLINE fold #-} fold :: (Maybe a -> b -> b) -> b -> ExpoNat a -> b fold fz (ExpoNat xy) = fx (fold fzy) fold fz NoExpoNat = z {-# NOINLINE build #-} build :: (forall b. (Maybe a -> b -> b) -> b -> b) -> ExpoNat a build f = f ExpoNat NoExpoNat {-# RULES "fold/build" forall fn (g :: forall b. (Maybe a -> b -> b) -> b -> b). fold fn (build g) = gfn #-} 

As an example, take match and appl from “ Is there a way to generalize this TrieMap code? ” And compose them so that ExpoNat merges. (Note that we must "strengthen the induction hypothesis" at appl .)

 {-# INLINE match #-} match :: Nat -> ExpoNat () match n = build $ \fz -> let go Zero = f (Just ()) z go (Succ n) = f Nothing (go n) in go n {-# INLINE appl #-} appl :: ExpoNat a -> (Nat -> Maybe a) appl = fold (\fz -> \n -> case n of Zero -> f Succ n' -> z n') (\n -> Nothing) applmatch :: Nat -> Nat -> Maybe () applmatch x = appl (match x) 

You can verify the merge by checking Core with -ddump-simpl .

Now we would like to do the same for Tree .

 data Tree = Leaf | Node Tree Tree data TreeMap a = TreeMap { tm_leaf :: Maybe a, tm_node :: TreeMap (TreeMap a) } | EmptyTreeMap 

We have problems: TreeMap is an irregular data type, and therefore it is not clear how to write the corresponding addition / assembly pair.

Haskell programming with nested types: The principled approach seems to have an answer (see Bush type), but 4:30 AM seems too late for me to work. How can I write hfmap ? Have there been further developments since then?

A similar version of this question is asked in What is the type of catamorphism (fold) for irregular recursive types?

Answer 1

I have worked on this yet, and now I have working fusion without using common paper gadgets.

 {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveTraversable #-} module Tree where data Tree = Leaf | Node Tree Tree deriving (Show) data ExpoTree a = ExpoTree (Maybe a) (ExpoTree (ExpoTree a)) | NoExpoTree deriving (Show, Functor) 

I deduced most of the specialized types by taking a generalized construct and then introducing type definitions until I hit the bottom. I have retained the general design here for ease of comparison.

 data HExpoTree fa = HExpoTree (Maybe a) (f (fa)) | HNoExpoTree type g ~> h = forall a. ga -> ha class HFunctor f where ffmap :: Functor g => (a -> b) -> fga -> fgb hfmap :: (Functor g, Functor h) => (g ~> h) -> (fg ~> fh) instance HFunctor HExpoTree where ffmap f HNoExpoTree = HNoExpoTree ffmap f (HExpoTree xy) = HExpoTree (fmap fx) (fmap (fmap f) y) hfmap f HNoExpoTree = HNoExpoTree hfmap f (HExpoTree xy) = HExpoTree x (f (fmap fy)) type Alg fg = fg ~> g newtype Mu fa = In { unIn :: f (Mu f) a } instance HFunctor f => Functor (Mu f) where fmap f (In r) = In (ffmap fr) hfold :: (HFunctor f, Functor g) => Alg fg -> (Mu f ~> g) hfold m (In u) = m (hfmap (hfold m) u) 

An Alg ExpoTreeH g can be decomposed into a product of two natural transformations:

 type ExpoTreeAlg g = forall a. Maybe a -> g (ga) -> ga type NoExpoTreeAlg g = forall a. ga {-# NOINLINE fold #-} fold :: Functor g => ExpoTreeAlg g -> NoExpoTreeAlg g -> ExpoTree a -> ga fold fz NoExpoTree = z fold fz (ExpoTree xy) = fx (fold fz (fmap (fold fz) y)) 

The natural transformation c ~> x very interesting and very necessary. Here's the constructed translation:

 hbuild :: HFunctor f => (forall x. Alg fx -> (c ~> x)) -> (c ~> Mu f) hbuild g = g In newtype I :: (* -> *) where I :: x -> I x deriving (Show, Eq, Functor, Foldable, Traversable) -- Needs to be a newtype, otherwise RULE firer gets bamboozled newtype ExpoTreeBuilder c = ETP {runETP :: (forall x. Functor x => (forall a. Maybe a -> x (xa) -> xa) -> (forall a. xa) -> (forall a. ca -> xa) )} {-# NOINLINE build #-} build :: ExpoTreeBuilder c -> forall a. ca -> ExpoTree a build g = runETP g ExpoTree NoExpoTree 

A new type of builder function is needed because GHC 8.0 does not know how to disable this rule.

Now the label merge rule:

 {-# RULES "ExpoTree fold/build" forall (g :: ExpoTreeBuilder c) c (f :: ExpoTreeAlg g) (n :: NoExpoTreeAlg g). fold fn (build gc) = runETP gfnc #-} 

Implementation of 'match' with 'build':

 {-# INLINE match #-} match :: Tree -> ExpoTree () match n = build (match_mk n) (I ()) where match_mk :: Tree -> ExpoTreeBuilder I match_mk Leaf = ETP $ \ fz (I c) -> f (Just c) z match_mk (Node xy) = ETP $ \ fzc -> -- NB: This fmap is bad for performance f Nothing (fmap (const (runETP (match_mk y) fzc)) (runETP (match_mk x) fzc)) 

Implement "appl" with "fold" (we need to define a custom functor to determine the return type.)

 newtype PFunTree a = PFunTree { runPFunTree :: Tree -> Maybe a } deriving (Functor) {-# INLINE appl #-} appl :: ExpoTree a -> PFunTree a appl = fold appl_expoTree appl_noExpoTree where appl_expoTree :: ExpoTreeAlg PFunTree appl_expoTree = \zf -> PFunTree $ \n -> case n of Leaf -> z Node n1 n2 -> runPFunTree f n1 >>= flip runPFunTree n2 appl_noExpoTree :: NoExpoTreeAlg PFunTree appl_noExpoTree = PFunTree $ \n -> Nothing 

Putting it all together:

 applmatch :: Tree -> Tree -> Maybe () applmatch x = runPFunTree (appl (match x)) 

We can check the kernel again with -ddump-simpl . Unfortunately, although we have successfully fused the TrieMap data TrieMap , we are left with suboptimal code due to fmap in match . Elimination of this inefficiency is left for future work.

Answer 2

It seems that the document uses the recursive Type and Tree parallel between ExpoNat a as a recursive type constructor ( Type -> Type ).

 newtype Fix f = Fix (f ( Fix f)) newtype HFix ha = HFix (h (HFix h) a) 

Fix f is the smallest fixed point of the endofund in the category of types and functions, f :: Type -> Type ; HFix h represents the smallest fixed point of endofunctor h by the category of functors and natural transformations, h :: (Type -> Type) -> (Type -> Type) .

 -- x ~ Fix (ExpoNatF a) ~ ExpoNat data ExpoNatF ax = ExpoNatF (Maybe a) x | NoExpoNatF fmap :: (x -> y) -> ExpoNatF ax -> ExpoNatF ay fmap f (ExpoNatF uv) = ExpoNatF u (fv) fmap _ NoExpoNatF = NoExpoNatF -- f ~ HFix TreeMapH ~ TreeMap data TreeMapH fa = TreeMapH (Maybe a) (f (fa)) | EmptyTreeMapH hfmap :: (f ~> g) -> (TreeMapH f ~> TreeMapH g) hfmap f (TreeMapH uv) = TreeMapH u ((fmap . fmap) fv) hfmap _ EmptyTreeMapH = EmptyTreeMapH -- (~>) is the type of natural transformations type f ~> g = forall a. fa -> ga 

• Endofentors generate algebras.

   type Alg fa = fa -> a type HAlg hf = hf ~> f 

• fold , or cata maps any algebra to morphism (a natural transformation of the function |).

    cata :: Alg fa -> Fix f -> a hcata :: HAlg hf -> (HFix h ~> h) 

• build builds value from its church coding.

   type Church f = forall a. Alg fa -> a type HChurch h = forall f. HAlg hf ~> f build :: Church f -> Fix f hbuild :: HChurch h -> HFix ha -- The paper actually has a slightly different type for Church encodings, derived from the categorical view, but I'm pretty sure they're equivalent 

• build/fold Merge is summed up by one equation.

    cata alg ( build f) = f alg hcata alg (hbuild f) = f alg