haskell - Functor 实例是唯一的吗？

Question

我想知道到什么程度Functor Haskell 中的实例由仿函数定律(唯一)确定。

自 ghc可以得出Functor至少对于“普通”数据类型的实例，它们似乎至少在各种情况下必须是唯一的。

为方便起见，Functor定义和仿函数定律是:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

fmap id = id
fmap (g . h) = (fmap g) . (fmap h)

问题:

• 能否推导出 map 的定义从假设它是Functor开始data List a = Nil | Cons a (List a) 的实例？如果是这样，必须做出哪些假设才能做到这一点？

• 是否有任何 Haskell 数据类型具有多个 Functor满足仿函数定律的实例？

• 什么时候可以ghc得出 functor例如，什么时候不能？

• 所有这些都取决于我们如何定义平等吗？ Functor法律以值(value)平等的形式表达，但我们不要求 Functors有Eq实例。那么这里有什么选择吗？

关于平等，肯定有一个我称之为“构造函数平等”的概念，它使我们能够推断 [a,a,a] “等于”[a,a,a]对于 a 的任何值任何类型，即使 a没有(==)为其定义的。所有其他(有用的)平等概念可能都比这种等价关系更粗糙。但我怀疑 Functor 中的平等法律更多地是一种“推理平等”关系，并且可以针对具体应用。对此有什么想法吗？

Answer 1

参见 Brent Yorgey 的 Typeclassopedia :

Unlike some other type classes we will encounter, a given type has at most one valid instance of Functor. This can be proven via the free theorem for the type of fmap. In fact, GHC can automatically derive Functor instances for many data types.