7

我想理解函子不动点的抽象概念，但是，我仍在努力弄清楚它的确切实现及其在 Haskell 中的变态。

例如，如果我根据“程序员的类别理论”一书 - 第 359 页定义，则以下代数

-- (Int, LiftF e Int -> Int)

data ListF e a = NilF | ConsF e a

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) -> n + 1
lenAlg NilF = 0

根据变质的定义，可以将以下函数应用于 ListF 的不动点，即 List，以计算其长度。

cata lenAlg :: [e] -> Int
cata lenAlg = lenAlg . fmap (cata lenAlg) . unFix

我有两个困惑。首先，Haskell 编译器如何知道 List 是ListF 的不动点？我从概念上知道它是，但是编译器怎么知道，即，如果我们定义另一个与 List 相同的 List'，我敢打赌编译器不会自动推断 List' 也是 ListF 的不动点，或者确实它？（我会很惊讶）。

其次，由于 cata lenAlg 的递归性质，它总是试图 unFix 数据构造函数的外层以暴露函数的内层（顺便说一句，我的这种解释是否正确？）。但是，如果我们已经在叶子节点，我们怎么能调用这个函数呢？

fmap (cata lenAlg) Nil

例如，有人可以帮助为以下函数调用编写执行跟踪以澄清吗？

cata lenAlg Cons 1 (Cons 2 Nil)

我可能遗漏了一些明显的东西，但是我希望这个问题对于其他有类似困惑的人仍然有意义。

答案摘要

@nm 回答了我的第一个问题，指出为了让 Haskell 编译器找出 Functor A 是 Functor B 的不动点，我们需要明确。在这种情况下，它是

type List e = Fix (ListF e)

@luqui 和@Will Ness 指出，由于 fmap 的定义，在叶子上调用 fmap (cata lenAlg)，在这种情况下是 NilF，将返回 NilF。

-- f :: a -> b
fmap f (ConsF e a) = ConsF e (f b)
fmap f NilF        = NilF

我会接受@nm 的回答，因为它直接解决了我的第一个（更大的）问题，但我确实喜欢所有三个答案。非常感谢您的帮助！

4

3 回答 3

5

ListF e编译器知道和之间关系的唯一方法[e]是告诉它。您没有提供足够的上下文来准确回答，但我可以推断出unFix有类型

unFix :: [e] -> ListF e [e]

也就是说，它展开顶层。 unFix可能更通用，例如在recursion-schemes类型族中用于将数据类型与其底层函子相关联。但这就是这两种类型的联系。

至于你的第二个问题，你需要更清楚什么时候有列表，什么时候有ListF. 它们完全不同。

fmap (cata lenAlg) Nil

在这里，您要映射的函子ListF e适用于您喜欢的任何东西e。也就是说，它是这样的fmap：

fmap :: (a -> b) -> ListF e a -> ListF e b

如果你instance Functor (ListF e)自己实现（总是一个很好的练习）并让它编译，你会发现Nil必须映射到Nil，所以cata lenAlg根本不重要。

让我们看看类型Cons 1 (Cons 2 Nil)：

Nil                 :: ListF e a
Cons 2 Nil          :: ListF Int (ListF e a)
Cons 1 (Cons 2 Nil) :: ListF Int (ListF Int (ListF e a))

这里有些不对劲。问题是我们忘记了unFix将ListF备份卷入常规列表的相反操作。我会调用这个函数

roll :: ListF e [e] -> [e]

现在我们有

Nil                                      :: ListF e a
roll Nil                                 :: [e]
Cons 2 (roll Nil)                        :: ListF Int [Int]
roll (Cons 2 (roll Nil))                 :: [Int]
Cons 1 (roll (Cons 2 (roll Nil)))        :: ListF Int [Int]
roll (Cons 1 (roll (Cons 2 (roll Nil)))) :: [Int]

这些类型现在保持良好和小型，这是一个好兆头。对于执行跟踪，我们只需要注意unFix . roll = id，但是它们是有效的。重要的是要注意

fmap f (Cons a b) = Cons a (f b)
fmap f Nil        = Nil

也就是说，fmap仅ListF将函数应用于类型的“递归部分”。

我将切换Cons案例以lenAlg (ConsF e n) = 1 + n使跟踪更具可读性。还是有点乱，祝你好运。

cata lenAlg (roll (Cons 1 (roll (Cons 2 (roll Nil)))))
(lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 1 (roll (Cons 2 (roll Nil)))))
lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 1 (roll (Cons 2 (roll Nil)))))))
lenAlg (fmap (cata lenAlg) (Cons 1 (roll (Cons 2 (roll Nil)))))
lenAlg (Cons 1 (cata lenAlg (roll (Cons 2 (roll Nil)))))
1 + cata lenAlg (roll (Cons 2 (roll Nil)))
1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 2 (roll Nil)))
1 + lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 2 (roll Nil)))))
1 + lenAlg (fmap (cata lenAlg) (Cons 2 (roll Nil)))
1 + lenAlg (Cons 2 (cata lenAlg (roll Nil)))
1 + 1 + cata lenAlg (roll Nil)
1 + 1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll Nil)
1 + 1 + lenAlg (fmap (cata lenAlg) (unFix (roll Nil)))
1 + 1 + lenAlg (fmap (cata lenAlg Nil))
1 + 1 + lenAlg Nil
1 + 1 + 0
2

另请参阅我关于变质的其他答案。

于 2018-11-27T08:30:00.450 回答
4

不，unFix公开结构，然后在其上fmap f应用功能f。如果它是一个叶子，fmap f它将做它定义为叶子做的事情 - 即，什么都不做。就像在 Haskell 的基于案例的fmap定义中一样，“知道” ie 被定义为处理每种情况。

Fix (ListF e) = ListF e (Fix (ListF e)) 
              = NilF | ConsF e (Fix (ListF e))

所以重命名Fix (ListF e)为Listof e我们得到

Listof     e  = NilF | ConsF e (Listof e)

Listof e是递归类型。ListF e r是非递归类型。 Fix用它做一个递归类型。ListF e作为一个 Functor 意味着fmap作用于r“肉”，ListF e成为这个“水果”的“坚硬外壳”。

data ListF e a = NilF | ConsF e a

newtype Fix f = X { unFix    :: (f       (Fix f)) }

-- unFix ::    Fix f          -> f       (Fix f        )
-- unFix (_ :: Fix (ListF e)) :: ListF e (Fix (ListF e))

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) = n + 1
lenAlg NilF        = 0

instance Functor (ListF e) where
    -- fmap :: (a -> b) -> (ListF e a) -> (ListF e b)
    fmap f NilF        = NilF
    fmap f (ConsF e r) = ConsF e (f r)

cata :: (ListF e Int -> Int) -> Fix (ListF e) -> Int
cata lenAlg x = (lenAlg . fmap (cata lenAlg) . unFix) x
              =  lenAlg ( fmap (cata lenAlg) ( unFix  x ))
--------
        x       ::       Fix (ListF e)
        unFix x ::            ListF e (Fix (ListF e))
        fmap (cata lenAlg) :: ListF e (Fix (ListF e)) -> ListF e (Int)
              cata lenAlg  ::          Fix (ListF e)  ->          Int

        fmap (cata lenAlg)   (unFix  x              ) :: ListF e  Int 
 lenAlg (_                                            :: ListF e  Int ) :: Int

看？所有的电线都到了它们合适的地方。fmap递归地变换内部部分r，然后lenAlg 代数应用最后一个变换，这是折叠结构的最后一步，其中所有内部部分都已经折叠成递归结果。从而产生最终的结果。

作为一个具体的例子，对于两个数字1和2的列表，我们有

-- newtype Fix f  = X { unFix :: (f      (Fix f         )) }
--             _\_______       ____\____      _\________
onetwo :: Fix (ListF Int) -- ~ ListF Int (Fix (ListF Int))
onetwo = X (ConsF 1
                  (X (ConsF 2
                            (X NilF))))

cata lenAlg :: Fix (ListF e) -> Int
cata lenAlg    onetwo
  = {- definition of cata   -}
    lenAlg . fmap (cata lenAlg) . unFix  $ onetwo
  = {- definition of onetwo -}
    lenAlg . fmap (cata lenAlg) . unFix  $ 
                           X (ConsF 1 (X (ConsF 2 (X NilF))))
  = {- definition of unFix  -}
    lenAlg . fmap (cata lenAlg) $ 
                              ConsF 1 (X (ConsF 2 (X NilF)))
  = {- definition of fmap   -}
    lenAlg $ ConsF 1 (cata lenAlg     (X (ConsF 2 (X NilF))))
  = {- definition of lenAlg -}
    (+ 1)  $          cata lenAlg     (X (ConsF 2 (X NilF)))
  = {- definition of cata   -}
    (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                       X (ConsF 2 (X NilF))
  = {- definition of unFix  -}
    (+ 1) $ lenAlg . fmap (cata lenAlg) $ ConsF 2 (X NilF)
  = {- definition of fmap   -}
    (+ 1) $ lenAlg $ ConsF 2 $ cata lenAlg        (X NilF)
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $           cata lenAlg        (X NilF)
  = {- definition of cata   -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                                  (X NilF)
  = {- definition of unFix  -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) $   NilF
  = {- definition of fmap   -}
    (+ 1) $ (+ 1)  $ lenAlg $                        NilF
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $ 0
  = (+ 1) $ 1
  = 2

还，

squaringAlg :: ListF Int [Int] -> [Int]
squaringAlg (ConsF e r) = e*e : r
squaringAlg NilF        = []

filteringAlg :: (e -> Bool) -> ListF e [e] -> [e]
filteringAlg p (ConsF e r) | p e       = e : r
                           | otherwise = r
filteringAlg _ NilF                    = []

等等

于 2018-11-27T08:29:43.513 回答
4

“List is the fixed point of ListF”是一种快速松散的修辞手法。虽然快速而松散的推理在道德上是正确的，但您始终需要牢记无聊的正确事物。如下：

的任何最小不动点ListF e同构于[e]。

现在“编译器”（顺便说一下，这是“Haskell 语言”的一个快速而宽松的词）不知道这种同构。你可以整天写同构类型

data []    x = []   | (:)   x ([]    x)    -- the imaginary built-in definition of []
data ListA x = NilA | ConsA x (ListA x)
data ListB x = NilB | ConsB x (ListB x)
data ListC x = NilC | ConsC x (ListC x)

并且编译器永远不会将它们视为“相同类型”。它也不会知道 的固定点ListF e与 相同[e]，或者确实是固定点。如果您想使用这些同构，您需要通过编写一些代码（例如通过定义 的实例Data.Types.Isomorphic）来教编译器了解它们，然后在每次要使用时明确指定同构！

有这个想法，让我们看看cata你已经定义了。首先映入眼帘的是定义类型签名的尝试是一个语法错误。让我们去掉它，只在 GHCi 中定义函数（为了避免混淆，我更改了参数的名称f，并修复了 ListF 定义中的一些拼写错误）

Main> data ListF e a = NilF | ConsF e a
Main> let lenAlg :: ListF e Int -> Int
Main|     lenAlg (ConsF e n) = n + 1
Main|     lenAlg NilF = 0
Main|
Main>
Main> :m + Data.Fix
Main Data.Fix> cata f = f . fmap (cata f) . unFix
Main Data.Fix> :t cata
cata :: Functor f => (f b -> b) -> Fix f -> b
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Functor (ListF e) => Fix (ListF e) -> Int

这表示为了使用lenAlg，您需要：

  • Functor定义for的一个实例ListF e
  • 显式使用Fix (ListF e)（这是ListF 的一个固定点）。希望“ListF 的固定点”存在是行不通的。没有魔法。

所以让我们这样做：

Main Data.Fix> instance Functor (ListF e) where
Main Data.Fix|     fmap f NilF = NilF
Main Data.Fix|     fmap f (ConsF e a) = ConsF e (f a)
Main Data.Fix>
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Fix (ListF e) -> Int

太好了，现在我们可以计算基于 ListF 的 Fix-wrapped 列表的长度。但是，让我们先定义一些辅助定义。

Main Data.Fix> type List e = Fix (ListF e)
Main Data.Fix> nil = Fix (NilF)
Main Data.Fix> let infixr 7 ~~                   -- using an infix operator for cons
Main Data.Fix|     h ~~ t = Fix (ConsF h t)
Main Data.Fix|
Main Data.Fix>
Main Data.Fix> myList = (1::Int) ~~ 2 ~~ 3 ~~ 4 ~~ nil
Main Data.Fix> :t myList
myList :: Fix (ListF Int)

[Int]这是我们的“列表”（准确地说是同构的类型的成员）。让我们来吧cata lenAlg：

Main Data.Fix> cata lenAlg myList
4

成功！

底线：编译器什么都不知道，你需要解释一切。

于 2018-11-27T08:52:15.070 回答