非平凡函子的示例

Question

在Haskell中，函子几乎总是可以派生的，是否存在类型为函子且满足函子定律（例如fmap id == id）但不能根据一组简单规则派生的情况？

那可折叠，可遍历，半群等呢？有没有重要的案例？

Answer 1

我偶然发现了一个有趣的论点。（很晚了，所以我想知道明天是否会有意义）

我们可以构造的证据种类SK还原为GADT：

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

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

（有，我觉得相当优雅，但也许更少示范替代的表述：如果你删除的RedK构造函数，然后Red t是Functor当且仅当该类型的系统可以表达的减少t 发散 -有时它发散，但你可以”不能证明这一点，而我的脑子在这种情况下是否真的是仿函数感到困惑）

Answer 2

从这个意义上说，没有非平凡的函子。所有函子可以机械地推导为款项（Either）和产品（Tuple的）Identity和Const仿函数。有关此构造的详细信息，请参见关于函数代数数据类型的部分。

在更高的抽象层次上，这是可行的，因为Haskell的类型形成了笛卡尔封闭类别，其中存在终端对象，所有乘积和所有指数。

Answer 3

可以将空参数类型明确地自动创建为函子：

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)

可以说是法律实例。

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