Haskell 中的身份函数有多个居民吗？

Question

在范畴论中可以证明恒等函数是唯一的。也有人说，用参数推理，该类型forall a. a -> a只有一个居民。在 Haskell 中，虽然我可以想到更多的身份函数实现：

id x = x
id x = fst (x, "useless")
id x = head [x]
id x = (\x -> x) x
id x = (\x -> (\x -> x) x) x

forall a. a -> a当有多个实现时，如何理解“标识函数是唯一的”和“任何具有类型的函数只有一个居民”这句话？

Answer 1

对我来说，这些人都像同一位居民。为了表明它们是不同的，尝试构建一个它们表现不同的输入。如果不能，它们实际上必须是相同的功能，但实现方式不同。

考虑来自不同学科的类似物。在数论中，可以证明存在一个唯一的最小素数，即2。但这怎么可能呢？10/5 也是最小的素数，1+1 也是。所有这些语句都可能同时为真，因为 10/5 实际上与 2 相同，就像您编写的所有表达式与恒等函数相同。

Answer 2

这些都是不同 的实现中的相同的 功能。因此，这里不再有一个居民，因为这里指的是功能，而不是其实现。