3

考虑以下包装器：

newtype F a = Wrap { unwrap :: Int }

我想反驳（作为围绕这个有趣帖子的练习）存在一个合法Functor F实例，它允许我们将Int -> Int类型函数应用于实际内容并〜忽略〜所有其他函数（即fmap nonIntInt = id）。

我相信这应该用一个自由定理来完成（我在这里fmap读到）： 对于给定的 ,和,这样: ,给定构造函数的自然映射在哪里。fghkg . f = k . h$map g . fmap f = fmap k . $map h$map

什么定义了自然地图？我是否正确地假设它是一个简单flip const的 for F？

据我所知：$map f是我们Ff在范畴论中所指的。因此，从分类的意义上说，我们只是想要下图中的一些东西来通勤： 在此处输入图像描述

然而，我不知道用什么代替???s （也就是说，我们应用什么函子来得到这样的图，我们如何表示这个几乎fmap-？）。

那么，一般来说，什么是自然地图F？的自由定理的正确图是什么fmap？

我要去哪里？

考虑：

f = const 42
g = id

h    = const ()
k () = 42

很容易看出f . g是h . k。然而，不存在的fmap只会执行，而f不是k，给出不同的结果。如果我对自然性的直觉是正确的，那么这样的证明就会奏效。这就是我想要弄清楚的。

@leftaroundabout提出了一个更简单的证明：fmap show . fmap (+1)改变内容，不像fmap $ show . (+1). 这是一个很好的证明，但我仍然想将自由定理作为练习。

4

1 回答 1

2

所以我们正在娱乐一个功能m :: forall a b . (a->b) -> F a -> F b，这样（除其他外）

m (1 +)    (Wrap x) = (Wrap (1+x))
m (show)   (Wrap x) = (Wrap x)

这里有两个有点相关的问题。

  1. 一个乖巧的人能fmap做到吗？
  2. 参数函数可以做到这一点吗？

这两个问题的答案都是“不”。

一个行为端正的人fmap不能这样做，因为fmap必须遵守 的公理Functor。我们的环境是否是参数化的无关紧要。的公理Functor说，对于所有函数a和b，必须成立，而对于和fmap (a . b) = fmap a . fmap b则失败。所以不能成为一个乖巧的人。a = showb = (1 +)mfmap

参数函数不能做到这一点，因为这就是参数定理所说的。当将类型视为术语之间的关系时，相关函数将相关参数用于相关结果。很容易看出m参数化失败了，但看起来稍微容易一些m': forall a b. (a -> b) -> (Int -> Int)（两者可以简单地相互转换）。(1 +)是相关的，show因为m'它的参数是多态的，所以参数的不同值可以通过任何关系相关。函数是关系，并且存在发送(1 +)到的函数show。但是，结果类型是m'没有类型变量的，所以它对应的是常量关系（它的值只和自己有关）。由于每个值包括m'与自身相关，因此所有参数函数都m :: forall a b. (a -> b) -> (Int -> Int)必须服从m f = m g，即它们必须忽略它们的第一个参数。这在直觉上是显而易见的，因为没有什么可以应用的。

fmap事实上，人们可以通过观察行为良好的行为必须是参数来从第二个陈述中推断出第一个陈述。因此，即使该语言允许非参数性，fmap也不能对其进行任何重要的使用。

于 2021-04-25T13:53:32.807 回答