Alt`类型类的函子分布定律是平凡的吗?

问题描述 投票:5回答:2

我正在查看the Alt typeclass的定律,看起来像这样:

Alt

其中一项法律是这样的:

class Functor f => Alt f
  where
  (<!>) :: f a -> f a -> f a

更详细地说,这是:

<$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

假设我们不使用fmap f $ (<!>) a b = (<!>) (fmap f a) (fmap f b) 操作,即我们假设该类是这样编写的:

<!>

我们可以这样编写一个组合器:

class Functor f => Alt f
  where
  alt :: (f a, f a) -> f a

[表示具有给定函子mapBoth :: Functor f => (a -> b) -> (f a, f a) -> (f b, f b) mapBoth f = bimap (fmap f) (fmap f) type Pair a = (a, a)函子的组成。因此它本身就是函子的态射映射。

现在可以将这样的法律写成(不改变其含义):

f

请注意,fmap f . alt = alt . mapBoth f 只是将mapBoth f应用于fmap f的两个自变量,就像法律的原始陈述中一样。

类似于要求alt是从函子alt到函子(f -, f -)的自然转变。

但是,实际上f -类型的函数[[not不可能自然转换吗?如何编写alt的“错误”实现进行类型检查,但会被法律拒绝?

haskell functor free-theorem
2个回答
1
投票
是,根据参数法,该法律免费适用。

即使那样,这些法律仍然有价值。

  1. 它使人们无需精通编程语言理论即可意识到它们。
  2. 如果将这些接口移植到类型系统较弱的语言,则需要遵循这些规则。
  3. 直到Haskell实际上被赋予形式语义,从技术上讲,我们不知道那些自由定理成立。通过足够高的形式标准,仅假装Haskell是纯多态lambda微积分是不够的。因此,我们也可以添加并检查这些“免费”法律,以防万一。

1
投票
虽然不是其他答案和评论的共识,但这是

不是“现实世界” Haskell的自然属性。

对编写非参数代码的开发人员来说,知道何时应该添加约束以与需要参数化的代码保持兼容是很有帮助的。

举止不佳的例子

alt

© www.soinside.com 2019 - 2024. All rights reserved.