trimaps的快捷方式融合

Question

在 Haskell 中尝试融合中间 trimaps 时出现此问题。

考虑 Peano 自然数的 trie：

data Nat = Zero | Succ Nat

data ExpoNat a = ExpoNat (Maybe a) (ExpoNat a)
               | NoExpoNat

我们可以轻松地在ExpoNat 上定义折叠（它本质上是一个列表）并使用foldr/build（又名finally tagless）融合中间出现的ExpoNat：

{-# NOINLINE fold #-}
fold :: (Maybe a -> b -> b) -> b -> ExpoNat a -> b
fold f z (ExpoNat x y) = f x (fold f z y)
fold f z NoExpoNat = z

{-# NOINLINE build #-}
build :: (forall b. (Maybe a -> b -> b) -> b -> b) -> ExpoNat a
build f = f ExpoNat NoExpoNat

{-# RULES "fold/build" forall f n (g :: forall b. (Maybe a -> b -> b) -> b -> b). fold f n (build g) = g f n #-}

例如，我们从“Is there a way to generalize this TrieMap code?”中提取match 和appl 并将它们组合成ExpoNat 被融合掉。 （注意我们必须在appl中“强化归纳假设”。）

{-# INLINE match #-}
match :: Nat -> ExpoNat ()
match n = build $ \f z ->
  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 (\f z -> \n ->
            case n of Zero    -> f
                      Succ n' -> z n')
         (\n -> Nothing)

applmatch :: Nat -> Nat -> Maybe ()
applmatch x = appl (match x)

可以通过-ddump-simpl检查Core来验证融合。

现在我们想对 Tree 做同样的事情。

data Tree = Leaf | Node Tree Tree

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

我们遇到了麻烦：TreeMap 是一种非常规数据类型，因此如何编写其对应的折叠/构建对并不明显。

Haskell Programming with Nested Types: A Principled Approach 似乎有答案（请参阅Bush 类型），但凌晨 4:30 对我来说似乎为时已晚。一个人应该怎么写hfmap？自那以后有进一步的发展吗？

在What's the type of a catamorphism (fold) for non-regular recursive types? 中提出了这个问题的类似变体

Answer 1

我在这方面做了更多工作，现在我有了工作融合，没有使用论文中的通用小工具。

{-# 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)

我通过采用泛型构造然后内联类型定义来派生大多数专用类型，直到触底。为了便于比较，我在这里保留了通用结构。

data HExpoTree f a = HExpoTree (Maybe a) (f (f a))
                   | HNoExpoTree

type g ~> h = forall a. g a -> h a

class HFunctor f where
  ffmap :: Functor g => (a -> b) -> f g a -> f g b
  hfmap :: (Functor g, Functor h) => (g ~> h) -> (f g ~> f h)

instance HFunctor HExpoTree where
  ffmap f HNoExpoTree = HNoExpoTree
  ffmap f (HExpoTree x y) = HExpoTree (fmap f x) (fmap (fmap f) y)
  hfmap f HNoExpoTree = HNoExpoTree
  hfmap f (HExpoTree x y) = HExpoTree x (f (fmap f y))

type Alg f g = f g ~> g

newtype Mu f a = In { unIn :: f (Mu f) a }

instance HFunctor f => Functor (Mu f) where
  fmap f (In r) = In (ffmap f r)

hfold :: (HFunctor f, Functor g) => Alg f g -> (Mu f ~> g)
hfold m (In u) = m (hfmap (hfold m) u)

Alg ExpoTreeH g 可以分解为两个自然变换的乘积：

type ExpoTreeAlg g = forall a. Maybe a -> g (g a) -> g a
type NoExpoTreeAlg g = forall a. g a

{-# NOINLINE fold #-}
fold :: Functor g => ExpoTreeAlg g -> NoExpoTreeAlg g -> ExpoTree a -> g a
fold f z NoExpoTree = z
fold f z (ExpoTree x y) = f x (fold f z (fmap (fold f z) y))

c ~> x 这里的自然转换非常有趣，而且非常必要。这是构建翻译：

hbuild :: HFunctor f => (forall x. Alg f x -> (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 (x a) -> x a)
                                        -> (forall a. x a)
                                        -> (forall a. c a -> x a)
                                            )}

{-# NOINLINE build #-}
build :: ExpoTreeBuilder c -> forall a. c a -> ExpoTree a
build g = runETP g ExpoTree NoExpoTree

需要生成器函数的新类型，因为 GHC 8.0 不知道如何在没有 RULE 的情况下触发。

现在，捷径融合规则：

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

“匹配”与“构建”的实现：

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

'appl' 与 'fold' 的实现（我们需要定义一个自定义函子来定义返回类型。）

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 = \z f -> 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

把它们放在一起：

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

我们可以再次使用-ddump-simpl 检查内核。不幸的是，虽然我们成功地融合了TrieMap 数据结构，但由于match 中的fmap，我们留下了次优代码。消除这种低效率的工作留给未来的工作。

Answer 2

该论文似乎在 ExpoNat a 作为递归 Type 和 Tree 作为递归类型构造函数 (Type -> Type) 之间进行了比较。

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

Fix f表示内函子在类型和函数范畴上的最小不动点，f :: Type -> Type； HFix h 表示内函子h 在函子和自然变换类别h :: (Type -> Type) -> (Type -> Type) 上的最小不动点。

-- x ~ Fix (ExpoNatF a) ~ ExpoNat
data ExpoNatF a x = ExpoNatF (Maybe a) x | NoExpoNatF

fmap :: (x -> y) -> ExpoNatF a x -> ExpoNatF a y
fmap f (ExpoNatF u v) = ExpoNatF u (f v)
fmap _ NoExpoNatF = NoExpoNatF


-- f ~ HFix TreeMapH ~ TreeMap
data TreeMapH f a = TreeMapH (Maybe a) (f (f a)) | EmptyTreeMapH

hfmap :: (f ~> g) -> (TreeMapH f ~> TreeMapH g)
hfmap f (TreeMapH u v) = TreeMapH u ((fmap . fmap) f v)
hfmap _ EmptyTreeMapH = EmptyTreeMapH


-- (~>) is the type of natural transformations
type f ~> g = forall a. f a -> g a

• 内函子产生代数。

  type  Alg f a = f a -> a
  type HAlg h f = h f ~> f
  

• fold 或 cata 将任何代数映射到态射（函数|自然变换）。

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

• build 从其 Church 编码构造一个值。

  type  Church f = forall a.  Alg f a -> a
  type HChurch h = forall f. HAlg h f ~> f
  
   build ::  Church f ->  Fix f
  hbuild :: HChurch h -> HFix h a
  
  -- 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 fusion 用一个方程来概括。

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