在Haskell中，fst和snd这样的函数在什么意义上是由它们的类型特征唯一决定的？

Question

我最近又给了Haskell一次机会，主要是因为我听说了Haskell的“基本原则”(Haskell)一书，到目前为止，我正在经历一场大爆炸。我的背景是一位数学家，主要在代数领域工作，所以我通常能很好地理解范畴方面，但我不能完全理解下面的具体说法。在Haskell的第163页“第一性原理”中，有人声称这些函数

fst :: (a,b) -> a
snd :: (a,b) -> b

是由它们的类型签名唯一确定的。

现在，我觉得如果没有进一步的自然性、兼容性或普遍性要求，这是不正确的，这些要求唯一地决定了fst和snd的显式实现，给出了a和b到显式类型的绑定。

因此，我的问题是: fst和snd假定拥有哪些属性确实决定了它们的惟一性？

我觉得我对这意味着什么有了粗略的理解。如果我们想要fst和snd在某种程度上“以同样的方式”，无论我们为a和b选择哪种类型，那么我们确实别无选择，只能让(a，b)的居民返回其选民。然而，我不知道这里到底是什么意思。

乍一看，它可能会让人想起集合类别中的范畴产品之一，但该产品已经与其两个投影图一起出现了。当然，我们可以说，“如果我们想让三元组( (a，b)，fst，snd)满足范畴积的普适性质，那么fst和snd已经是唯一确定的了”，但这是一个相当微弱的主张，当然不是书中所说的那样。

另一个想法是，也许我们希望fst和snd与映射兼容，如果f :: a -> b是任何函数，那么我们可能想要像f a = fst.(f -*- id ) (a,undefined)这样的东西。(也可能是未定义的，而不是id，但这并不重要，因为我们还是放弃了它)。

任何帮助都是非常感谢的！

Answer 1

作为一个简单的例子，我们可以考虑函数id :: a -> a。对于任何类型的a，这个函数都接受一个a值并返回一个a值。然而，a不受任何类型的限制--这意味着我们不能对该类型做任何事情。我们甚至不能创造新的价值。因此，id求值为a类型值的唯一方法是返回给定的值。

id x = x

从技术上讲，还有另一种方法，因为有undefined :: a --一个具有任何类型的表达式。因此，undefined服务器是Haskell中的一种“底层实例”。但是，undefined从未实际计算值，试图计算它将导致错误。undefined表达式可以通过重言式undefined = undefined定义。因此，从技术上讲，我们可以另外定义id _ = undefined。这样的函数也可以驻留在类型a -> b中，尽管它永远无法被成功地计算出来。

同样的论点是，id :: a -> a是唯一定义的(撇开涉及undefined的退化情况不谈)，函数fst :: (a,b) -> a必须只有一个唯一的定义。它不能创建新的a值，也不能使用b值代替a，因此它必须计算为第一个元组元素。相反，fst :: (a,a) -> a没有唯一的定义，因为实现可以选择使用第一个或第二个元组元素。