非平凡函子的例子

Question

在 Haskell 中，几乎总是可以推导出函子（functor），但是否存在这样的情况：某个类型既满足函子定律（例如 fmap id == id），又不能按照简单的规则进行推导？

那么对于 Foldable、Traversable、Semigroup 等类型呢？是否存在非平凡的情况？

- Jiaming Lu

---

当你不确定是将函数应用于第一个值还是第二个值时，是否意味着类似元组的东西？ - talex

@talex 不是的，如果你把一个二元组 (a, b) 视为以 b 为函数参数的函子，那么 fmap 的结果就是 (a, c)，从中很清楚可以看出应该将函数 b -> c 应用于哪个值。 - Jiaming Lu

在Haskell中，函子总是可以派生的。Bartosz Milewski在他的书《程序员范畴论》[1]中谈到了这个问题。我需要自己查找确切的参考和细节，但这与Haskell中的函子形成某种代数有关。[1] https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ - michid

可折叠（Foldable）、可遍历（Traversable）和半群（Semigroup）都具有对称性，使它们可以在多个不同的方式下合法实例化，这是它们至少具有一种非平凡性的含义。 - luqui

@luqui，如果你使用 Atkey 风格的索引应用程序来为类型对齐集合定义一个可遍历性概念，那么你应该会恢复独特性。 - dfeuer

Answer 1

我刚刚发现了一个有趣的论点。 (由于太晚了，明天可能会更加清晰)

我们可以构建一个GADT类型来证明SK可简化性：

infixl 9 :%:
data Term = S | K | Term :%: Term

-- small step, you can get from t to t' in one step
data Red1 t t' where
    Red1S :: Red1 (S :%: x :%: y :%: z) (x :%: z :%: (y :%: z))
    ...

现在让我们创建一种类型，将其函子性隐藏在约简链的末尾。

data Red t a where
    RedStep :: Red1 t t' -> Red t' a -> Red t a
    RedK    :: a                     -> Red K a
    RedS    :: (a -> Bool)           -> Red S a

现在，如果t归一化为K，则Red t是一个Functor，但如果它归一化为S，则不是 - 这是一个无法判断的问题。因此，也许您仍然可以遵循“简单的规则集”，但如果允许GADTs，则规则必须足够强大以计算任何内容。

（还有一种我觉得相当优雅但可能不太明显的替代公式：如果去掉RedK构造函数，则当类型系统能够表达t的规约发散时，Red t才是一个Functor - 有时它会发散，但是你无法证明它，关于在这种情况下它是否真的是一个Functor，我的想法非常混乱）

- luqui

---

如果规约发散，为什么它可能不是一个函子？如果您在Red1中选择确定性规约策略，请定义data Blue t where BlueStep :: Red1 t t' -> Blue t' -> Blue t。（对于非确定性策略，情况会变得有点丑陋，因为您必须分离所有重叠的规则）。现在，您可以在Blue t旁边消耗Red t a。在每个步骤中，Blue t中的Red1 t t'证明t不是S。 - dfeuer

@dfeuer，嗯，我不确定我是否理解了。确实我们可以在每个步骤中得到t不等于S，但为了证明函子性质，我们需要在每一个步骤中都满足这一条件。 - luqui

我还没有完全做到，但是这个代码片段建立了我所勾画的框架，并且在表达一个特定示例的发散证明方面已经走了很远的路。 - dfeuer

Answer 2

明确的空参数类型可以自动转换为函子：

data T a deriving Functor

然而，隐式的空值却做不到这一点：

import Data.Void
data T a = K a (a -> Void)
    deriving Functor  -- fails
{-
error:
    • Can't make a derived instance of ‘Functor T’:
        Constructor ‘K’ must not use the type variable in a function argument
    • In the data declaration for ‘T’
-}

然而，

instance Functor T where
   fmap f (K x y) = absurd (y x)

这可能是一个合法的实例。

有人可能会争论，通过利用底部（bottoms），可以找到上述实例中函子定律的反例。但在这种情况下，我想知道即使存在底部，所有“标准”的函子实例是否实际上都是合法的。（也许它们是合法的？）

- chi

---

我认为大多数常见的“Functor”实例即使有底部值也是有效的。以下是 GHC 无法为其派生“Functor”的简单类型：data Foo a = Foo (a -> Bool) !Void。还有一种逆变性可能会阻碍它的方法：newtype Bar f a = Bar (f a -> Bool)。 GHC 无法派生完全有效的实例 instance Contravariant f => Functor (Bar f) where fmap f (Bar g) = Bar (g . contramap f)。主要问题在于将“Contravariant”添加到派生混合中会导致出现多个潜在实例（具有不兼容限制），例如 newtype Baz f g a = Baz (f (g a))。 - dfeuer

Answer 3

就问题而言，不存在非平凡的函子。所有函子都可以机械地派生为Either和Tuple的和与积，其中包括Identity和Const函子。有关此构造详细信息，请参见有关函子代数数据类型 的部分内容。

在更高的抽象层面上，这是因为 Haskell 的类型形成了一个 笛卡尔闭范畴，其中存在终端对象、所有积以及所有指数.

- michid

Answer 4

有点作弊，但我们还是试一下。 根据此文，当类型有约束时，例如： 此处，函数子不能自动导出。

data A a where
    A1 :: (Ord a) => a -> A a
deriving instance Functor A -- doesn't work

实际上，如果我们手动编写，它也不起作用。

instance Functor A where
    fmap f (A1 a) = A1 (f a) -- Can't deduce Ord for f a

然而，由于算法只是检查是否存在约束条件，因此我们可以引入一个类型类，使得每种类型都成为其成员。

class C c
instance C c

现在按照以上步骤使用C代替Ord进行操作。

data B b where
    B1 :: (C b) => b -> B b

deriving instance Functor B -- doesn't work

instance Functor B where
    fmap f (B1 b) = B1 (f b) -- does work!

- moonGoose

Answer 5

在base中有一个标准类型，叫做Compose，定义如下：

newtype Compose f g a = Compose { getCompose :: f (g a) }

派生的 Functor 实例是这样实现的：

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose v) = Compose (fmap (fmap f) v)

但是还有另一个完全合法的实例，其行为不同：

instance (Contravariant f, Contravariant g) => Functor (Compose f g) where
    fmap f (Compose v) = Compose (contramap (contramap f) v)

对我而言，Compose 有两个不同的实例可用，这表明没有一组规则可以自动适用于涵盖所有可能情况。

- Daniel Wagner

---

当两组约束条件都成立时（即当f和g都具有幻影参数时），实例具有相同的行为。因此，我认为这与不兼容的约束条件有关，而不是不同的行为。 - dfeuer