Functor实例是唯一的吗？ [英] Are Functor instances unique?

问题描述

我想知道Haskell中的 Functor 实例在多大程度上由函子法则确定（唯一）。 >由于 ghc 至少可以派生 Functor 实例用于至少普通数据类型，它似乎至少在各种各样的情况下它们必须是唯一的。

为方便起见， Functor 定义和函子法律是：

  class Functor f其中
 fmap ::（a  - > b） - > f a  - > f b 
 
 fmap id = id 
 fmap（g。h）=（fmap g）。 （fmap h）
  

问题：

• 可以从假定它是 Functor 的定义从 map c> 数据的实例List a = Nil |缺点（列表a）？如果是这样，为了做到这一点必须做出什么假设？
  

• 是否有Haskell数据类型有多个 Functor 符合函数法则的实例吗？

ghc 一个 functor 实例和什么时候不可以？



• 所有这些都取决于我们如何定义相等？ Functor 定律是以值相等的形式表达的，但我们并不要求 Functors 具有 Eq 实例。那么在这里有一些选择吗？
  
  
  

  关于相等性，当然有一个我称之为构造函数相等的概念，这允许我们推断 [a，a，a] 与 [a，a，a] 任何类型的 a ，即使 a 没有（== ）为其定义。所有其他（有用的）平等概念可能比这个等价关系更粗糙。但我怀疑 Functor 定律中的相等性更像是推理平等关系，并且可能是特定于应用程序的。对此有何看法？

请参阅Brent Yorgey的 Typeclassopedia ：

与我们遇到的其他类型类不同，给定类型最多只有一个有效的实例函子。这个可以通过 free theorem 的fmap类型。实际上， GHC可以自动派生 Functor实例对于许多数据类型。




I was wondering to what extent Functor instances in Haskell are determined (uniquely) by the functor laws.

Since ghc can derive Functor instances for at least "run-of-the-mill" data types, it seems that they must be unique at least in a wide variety of cases.

For convenience, the Functor definition and functor laws are:

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

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

Questions:

• Can one derive the definition of map starting from the assumption that it is a Functor instance for data List a = Nil | Cons a (List a)? If so, what assumptions have to be made in order to do this?

• Are there any Haskell data types which have more than one Functor instances which satisfy the functor laws?

• When can ghc derive a functor instance and when can't it?

• Does all of this depend how we define equality? The Functor laws are expressed in terms of an equality of values, yet we don't require Functors to have Eq instances. So is there some choice here?

Regarding equality, there is certainly a notion of what I call "constructor equality" which allows us to reason that [a,a,a] is "equal" to [a,a,a] for any value of a of any type even if a does not have (==) defined for it. All other (useful) notions of equality are probably coarser that this equivalence relationship. But I suspect that the equality in the Functor laws are more of an "reasoning equality" relationship and can be application specific. Any thoughts on this?

解决方案

See Brent Yorgey's 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.

这篇关于Functor实例是唯一的吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！