22

我想知道FunctorHaskell 中的实例在多大程度上（唯一地）由函子定律确定。

由于至少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的假设推导出开始的定义吗？如果是这样，为了做到这一点，必须做出哪些假设？Functordata List a = Nil | Cons a (List a)

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

  • 什么时候可以ghc派生一个functor实例，什么时候不能？

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

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

4

2 回答 2

25

请参阅 Brent Yorgey 的Typeclassopedia：

与我们将遇到的其他类型类不同，给定类型最多有一个 Functor 的有效实例。这可以通过fmap 类型的自由定理来证明。事实上，GHC 可以自动为许多数据类型派生 Functor 实例。

于 2013-11-04T19:06:21.180 回答
2

"When can GHC derive a functor instance and when can't it?"

When we have intentional circular data structures. The type system does not allow us to express our intent of a forced circularity. So, ghc can derive an instance, similar to that which we want, but not the same.

Circular data structures are probably the only case where the Functor should be implemented a different way. But then again, it would have the same semantic.

data HalfEdge a = HalfEdge { label :: a , companion :: HalfEdge a }

instance Functor HalfEdge where
    fmap f (HalfEdge a (HalfEdge b _)) = fix $ HalfEdge (f a) . HalfEdge (f b)

EDIT:

HalfEdges are structures (known in computer graphics, 3d meshes...) that represent undirected Edges in a graph, where you can have a reference to either end. Usually they store more references to neighbour HalfEdges, Nodes and Faces.

newEdge :: a -> a -> HalfEdge a
newEdge a b = fix $ HalfEdge a . HalfEdge b

Semantically, there is no fix $ HalfEdge 0 . HalfEdge 1 . HalfEdge 2, because edges are always composed out of exactly two half edges.

EDIT 2:

In the haskell community, the quote "Tying the Knot" is known for this kind of data structure. It is about data structures that are semantically infinite because they cycle. They consume only finite memory. Example: given ones = 1:ones, we will have these semantically equivalent implementations of twos:

twos = fmap (+1) ones
twos = fix ((+1)(head ones) :)

If we traverse (first n elements of) twos and still have a reference to the begin of that list, these implementations differ in speed (evaluate 1+1 each time vs only once) and memory consumption (O(n) vs O(1)).

于 2013-11-13T10:14:04.990 回答