types - 为什么 *id* 函数只有一种可能的实现？

Question

我多次看到有人声称可以证明具有类型签名的函数

α → α

只能通过返回参数来实现，因为我们对参数的类型一无所知。

id :: α → α
id a = a

可以在http://blog.precog.com/?p=431找到该声明的示例

但是是什么阻止我们做出这样的 if 语句（伪代码）？

id :: α → α
id a = if ( a is_a_String) a + "hello"
       else a

有没有我失踪的先决条件？

Answer 1

像这样的定理只适用于具有参数属性的语言。这意味着代码不能在运行时检查类型，因此，执行永远不能依赖类型信息。大多数函数式语言都具有此属性，而 OO 语言通常需要提供向下转换和类似功能，这会破坏参数化。

参数化是一个非常强大的属性。它确保了某些抽象属性，即您提到的所谓的“自由定理” ，并且它是可以在运行时擦除类型的高效实现的推动者。

另请参阅我的答案。