【问题标题】：Example of violating the Functor rules in HaskellHaskell 中违反 Functor 规则的例子
【发布时间】：2020-02-02 20:51:50
【问题描述】：

我有一个二叉树的数据结构和一个 Functor

data BST a = Empty | Node (BST a) a (BST a)
instance Functor BST  where
  fmap f Empty = Empty
  fmap f (Node l val r) = (Node (fmap f l) (f val  ) (fmap f r))

我需要找到一些 BST 实例和函数 f 的示例，其中 Functor(Identity,composition) 的规则违反

有人能指出正确的方向吗？

谢谢！

【问题讨论】：

这个实现对我来说看起来是正确的，我的意思是，它应该遵守这两个法律。
没有。你确定你从你得到它的地方正确地复制了这个练习吗？
定义一个新的 Functor 实例是你的练习吗？
另一种可能性，尽管我认为这不太可能：尽管此实现是 Hask 上的函子，但名称“BST”表明您正在处理二叉搜索树，其中存在数据类型不变量。这个实现不一定保留那些不变量，也许这可以通过指出它不是Ordered 类型和单调函数的子类别的函子来表达。但这是一个相当严重的延伸——你需要阅读相当高级的文章才能成为讨论这个问题的明智方式。
@GilShafriri 如果你还控制Functor 实例，那么编写一个不同的、错误的实例。

标签： haskell functor

【解决方案1】：

你找不到任何例子，因为你的定义符合函子定律。您可以通过对树的深度进行归纳来证明它。基本情况是 0 深度树（即Empty），然后是Node 情况的证明。证明很长但很简单。

编辑：

重新阅读您的问题，也许您正在寻找fmap 的定义，该类型检查但不符合函子定律。只需使用

data BST a = Empty | Node (BST a) a (BST a)
instance Functor BST  where
  fmap f Empty = Empty
  fmap f (Node l val r) = (Node (fmap f r) (f val  ) (fmap f l))
--                                      |- notice            |- notice

为什么它不遵守法律？那是你的。以下是您的定义确实成立的证据。尝试建立自己的证据来证明为什么我的定义没有

第一定律

fmap id == id

基本情况

fmap id Empty = Empty    -- by definition of fmap
              = id Empty -- by definition of id
=> fmap id = id          -- by eta-reducing both sides of the equation

递归案例

假设假设对于给定深度D（或更小）的所有树都为真。树一深度的证明(D + 1)

fmap id (Node l val r) = Node (fmap id l) (id val) (fmap id r) -- by definition of fmap
                       = Node (fmap id l) val      (fmap id r) -- by applying id to val
                       = Node l val r                          -- by induction hyp. fmap id l == l
                       = id (Node l val r)                     -- by definition of id
=> fmap id             = id                                    -- by eta-reducing both sides of the equation

第二定律

 fmap g . fmap f == fmap (g . f)

基本情况

-- Eq 1
(fmap g . fmap f) Empty = fmap g (fmap f Empty)  -- by definition of .
                        = fmap g Empty           -- by definition of fmap
                        = Empty                  -- by definition of fmap
-- Eq 2
fmap (g . f) Empty      = Empty                  -- by definition of fmap

-- Therefore
(fmap g . fmap f) Empty = fmap (g . f) Empty     -- By transition of equality on Eq1 and Eq2
fmap g . fmap f         = fmap (g . f)           -- by eta-reducing both sides of the equation

递归案例

假设假设对于给定深度D（或更小）的所有树都为真。树一深度的证明(D + 1)

-- Eq 1
fmap (g . f) (Node l val r) = Node (fmap (g . f) l) 
                                   ((g . f) val) 
                                   (fmap (g . f) r) -- by definition of fmap

                            = Node ((fmap g . fmap f) l) 
                                   ((g . f) val) 
                                   ((fmap g . fmap f) r) -- by induction hyp.

-- Eq 2
(fmap g . fmap f) (Node l val r) = fmap g (fmap f (Node l val r)) -- dy definition of .
                                 = fmap g $ Node (fmap f l) 
                                                 (f val) 
                                                 (fmap f r)       -- by definition of fmap
                                 = Node (fmap g (fmap f l))
                                        (g (f val))
                                        (fmap g (fmap f r))       -- by definition of fmap
                                 = Node ((fmap g . fmap f) l) 
                                        ((g . f) val) 
                                        ((fmap g . fmap f) r)     -- by induction hyp.

fmap (g . f) (Node l val r) = (fmap g . fmap f) (Node l val r)    -- By transition of equality on Eq1 and Eq2
fmap (g . f)                = (fmap g . fmap f)                   -- by eta-reducing both sides of the equation

【讨论】：

最后我得到确认函子不应该违反任何函子定律，但他声称实现是“错误的”。为什么？因为在向函子提供某些函数 f （例如 (\x -> (-x) ）后，BST 可以变成非 BST。我无法接受这个“错误”术语，因为任何违反函子中的某些不变量的行为都可能是被认为是“越野车”。
如果您参考@danielWagner 评论。他声称您可以实现一个仿函数实例，因此它变得有问题，而不是 _this_implementation 是有问题的。错误实例的一个示例是我的答案编辑中的实例
变成“buggy”是什么意思 - Functor 可以改变它所操作的数据的一些不变量。我觉得“越野车”这个词不适合这个现实。
当然我可以写一个违反法律的Functor，但我觉得这不是很有趣。教授声称 BST 上的每个 Functor 都是“错误的”。我有一个问题要同意。
对不起，我迷路了。您的问题是“我能否找到一个针对这种特定类型和实例违反函子定律的示例”。答案是否定的，你不能。所有这些“错误”问题与您的问题有什么关系？