En la teoría de categorías se puede demostrar que la función de identidad es única. También se dice que, razonando con parametricidad, que el tipo forall a. a -> a tiene solo un habitante. Sin embargo, en Haskell puedo pensar en más implementaciones de la función de identidad:

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

¿Cómo puedo entender la afirmación "la función de identidad es única" y "cualquier función con el tipo forall a. a -> a tiene un solo habitante" cuando hay implementaciones múltiples?

12
Labbekak 29 abr. 2020 a las 11:46

2 respuestas

La mejor respuesta

Todos me parecen el mismo habitante. Para mostrar que son diferentes, intente construir una entrada para la que se comporten de manera diferente. Si no puede, de hecho deben ser la misma función implementada de manera diferente.

Considere un análogo de una disciplina diferente. En teoría de números, se puede demostrar que hay un primo único más pequeño, a saber, 2. ¿Pero cómo puede ser esto? 10/5 también es el primo más pequeño, al igual que 1 + 1. Es posible que todas estas afirmaciones sean verdaderas a la vez porque 10/5 es, de hecho, lo mismo que 2, al igual que todas las expresiones que ha escrito son lo mismo que la función de identidad.

13
amalloy 29 abr. 2020 a las 10:39

Esas son diferentes implementaciones de la misma función . Por lo tanto, no hay más de un habitante aquí, ya que esto se refiere a la función, no a su implementación.

5
michid 29 abr. 2020 a las 09:38