11

我想我在hackage 文章中Control.Applicative发现了一个缺陷。作为对应用函子定律的描述，它说：

class Functor f => Applicative f where

一个带有应用程序的函子，提供嵌入纯表达式 ( pure) 的操作，以及对计算进行排序并组合它们的结果 ( <*>)。

一个最小的完整定义必须包括满足以下定律的这些函数的实现：

身份

pure id <*> v = v

作品

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

同态

pure f <*> pure x = pure (f x)

互换

u <*> pure y = pure ($ y) <*> u

（请注意，这并没有说明 fmap 的任何内容）并且它指出这些法律决定了Functor实例：

作为这些定律的结果，Functorf 的实例将满足

fmap f x = pure f <*> x

起初我认为这显然是错误的。也就是说，我猜肯定存在t满足以下两个条件的类型构造函数：

  1. t是Applicative满足上述规则的一个实例，并且
  2. 有两种不同的实现instance (Functor t) （即有两个不同的函数fmap1, fmap2 :: (a->b) -> (t a->t b)，满足函子定律）。

如果（且仅当）上述正确，则必须将上述语句重写为

f 的 Functor 实例必须满足

fmap f x = pure f <*> x

作为这些法律的结果，这符合Functor法律。

这显然是正确的，无论我的猜测是否正确。

我的问题是：我的猜测正确吗？有没有t符合要求的条件？

以下是我在尝试自己回答这个问题时的想法的解释。

如果我们只是对实际 Haskell 编程不感兴趣的数学家，我们可以很容易地肯定地回答这个问题。实际上，

t = Identity
newtype Identity a = Identity {runIdentity :: a}

满足上面的要求 1 和 2（事实上，几乎任何事情都可以）。事实上，是和Identity的一个简单的实例，如 中所定义。（这满足了。）要定义另一个“实现” ，为每种类型采取两个函数FunctorApplicativeData.Functor.Identityfmap f = (pure f <*>)instance (Functor f)a

transf_a, tinv_a :: a -> a

这样

tinv_a . transf_a = id

（从理论上讲，这很容易）。现在定义

instance (Functor Identity) where
 fmap (f :: a->b) = Identity . transf_b . f . tinv_a . runIdentity

这符合Functor法律，如果有

x :: a
f :: a -> b

这样

f x /= transf_b $ f $ tinv_a x

但是我们是否可以在 Haskell 中做到这一点并不明显。是这样的：

class (Isom a) where
 transf, tinv :: a -> a

instance (Isom a) where
 transf = id
 tinv = id

specialized instance (Isom Bool) where
 transf = not
 tinv = not

在 Haskell 中可能吗？

编辑

我忘了写一些很重要的东西。我认为Control.Applicative它是 GHC 基础包的一部分，所以我也对我的问题的答案是否会随着我还不理解的任何 GHC 语言扩展（例如FlexibleInstancesor ）而改变感兴趣。OverlappingInstances

4

2 回答 2

14

Haskell 中的任何类型最多只能有一个 的实例Functor，因此您的猜测是不正确的：对于任何类型t（无论它是否是 的实例Applicative）都不可能存在instance (Functor t). 见：http ://article.gmane.org/gmane.comp.lang.haskell.libraries/15384

于 2015-04-15T08:59:38.030 回答
2

a -> a它是只有两个居民的类型的属性，即id :: a -> a（定义为id x = x）和bottom :: a -> a定义为bottom = error "Infinite loop."。

如果我们仅将自己限制在“合理”的第一种情况，我们就会得出一个重要的数学定理，即至多有一个fmap类型forall a. forall b. (a -> b) -> f a -> f b满足fmap id = id和的函数fmap f . fmap g = fmap (f . g)。

如果我们不这样做，那么您是对的，我们有一种情况 wherefmap = undefined和另一种情况 where fmap = (<*>) . pure。但这有点俗气。

于 2015-04-15T20:54:32.927 回答