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) 的实例?如果是这样，为了做到这一点，必须做出哪些假设？

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

什么时候可以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.