Почему существует только одна возможная реализация функции * id *?

Question

я видел несколько раз утверждаем, что один может доказать, что функция с сигнатурой типа

α → α 

может быть осуществлен только путем возвращения аргумента, потому что мы ничего о типе параметра не знаем.

id :: α → α 
id a = a 

exmample этого требования можно найти на http://blog.precog.com/?p=431

Но что мешает нам делать, если заявление, как это (псевдо-код)?

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

Есть ли предварительное условие, что мне не хватает?

Answer 1

Теоремы, подобные этому, хранятся только на языках, которые характеризуются параметрами . Это означает, что код не может проверять типы во время выполнения, и, следовательно, выполнение никогда не может опираться на информацию о типе. Большинство функциональных языков обладают этим свойством, в то время как языки OO часто видят необходимость предоставления downcasts и подобных функций, которые нарушают параметричность.

Параметричность - очень мощное свойство. Он обеспечивает определенные свойства абстракции, так называемый "free theorems", как и тот, который вы упоминаете, и это средство эффективной реализации, которое может стирать типы во время выполнения.

См. Также my answer here.