2011-12-15 6 views
12

Nuevo en Haskell lo siento si esto es muy básicodeterminar el comportamiento de la función del tipo de la función

Este ejemplo está tomado de "Real World Haskell" -

ghci> :type fst 
fst :: (a, b) -> a 

Ellos muestran el tipo de fst función y luego seguir con este párrafo ...

"el tipo de resultado de fst es a. ya hemos mencionado que el polimorfismo paramétrico hace que el r Tipo eal inaccesibles: fst no tiene suficiente información para construir un valor de tipo a, ni puede convertir una a en un b. Entonces, el único comportamiento válido posible (omitir bucles infinitos o bloqueos) que puede tener es devolver el primer elemento del par. "

Siento que me falta el punto fundamental del párrafo, y tal vez algo importante sobre Haskell . ¿Por qué no la fst función de tipo de retorno b? ¿Por qué no podía tomar la tupla como un parámetro, sino simplemente devolver un Int (o cualquier otro tipo que no es a)? no entiendo por qué DEBE devolver el tipo a?

Gracias

Respuesta

24

Si lo hizo ninguna de esas cosas, su tipo cambiaría. Lo que dice la cita es que, dado que sabemos que fst es del tipo (a, b) -> a, podemos hacer esas deducciones al respecto. Si tuviera un tipo diferente, no podríamos hacerlo.

Por ejemplo, vemos que

snd :: (a, b) -> a 
snd (x, y) = y 

no escribe-comprobación, y así que sabemos un valor de tipo (a, b) -> a no puede comportarse como snd.

Parametricity es básicamente el hecho de que una función polimórfica de un cierto tipo debe obedecer ciertas leyes por la construcción - es decir, no hay ninguna expresión bien escrito de ese tipo que no obedece a ellos. Entonces, para que sea posible probar cosas sobre fst con él, primero debemos saber el tipo de fst.

Nota especialmente la palabra polimorfismo allí: no podemos hacer el mismo tipo de deducciones sobre los tipos no polimórficos. Por ejemplo,

myFst :: (Int, String) -> Int 
myFst (a, b) = a 

tipo controles, pero también lo hace

myFst :: (Int, String) -> Int 
myFst (a, b) = 42 

e incluso

myFst :: (Int, String) -> Int 
myFst (a, b) = length b 

Parametricity se basa fundamentalmente en el hecho de que una función polimórfica no puede "mirar" los tipos con los que se llama.Por lo tanto, el único valor del tipo a que conoce fst es el que se le da: el primer elemento de la tupla.

2

El punto aquí es que a y b son variables de tipo (que pueden ser iguales, pero eso no es necesario). De todos modos, dado que para una tupla dada de dos elementos, fst devuelve siempre el primer elemento, el tipo devuelto debe ser siempre el mismo que el tipo para el primer elemento.

5

El punto es que una vez que tiene ese tipo, las opciones de implementación son muy limitadas. Si devolvió Int, su tipo sería (a,b) -> Int. Dado que a podría ser cualquier cosa, no podemos desmotarlo de la nada en la implementación sin recurrir a undefined, por lo que debemos devolver el que nos ha proporcionado la persona que llama.

4

Debe leer el artículo Theorems for Free.

+11

Antes de terminar el capítulo 2 de RWH? – ehird

+1

Es un artículo gratuito, jajaja –

+1

@ehird que quería una explicación en profundidad, así que aquí está. La explicación básica de agitar la mano ya ha sido dada por otras personas – nponeccop

3

Tratemos de agregar algo más de agitar la mano a la que ya dio Real World Haskell. Vamos a tratar de convencernos de que dado que tenemos una función fst con el tipo (a,b) -> a la única función totales que puede ser es la siguiente:

fst (x,y) = x 

En primer lugar, no podemos devolver algo que no sea un valor de tipo a , eso es en la premisa de que fst tiene el tipo (a,b) -> a, entonces no podemos tener fst (x,y) = y o fst (x,y) = 1 porque eso no tiene el tipo correcto.

Ahora, como dice captación de aguas pluviales, si me dan un fst(Int,Int), fst no conoce estos se intercepciones, además, a o b no están obligados a pertenecer a cualquier clase de tipo de modo fst no tiene valores o funciones disponibles asociadas con a o b.

Así fst sólo conoce el valor y el valor ab que le doy y no puedo convertir en un ba (No se puede hacer una función b -> a) por lo que debe devolver el a valor dado.

Esto no es en realidad simplemente agitando la mano mágicamente, uno puede de hecho deducir qué expresiones posibles hay de un tipo polimórfico dado. De hecho, hay un programa llamado djinn que hace exactamente eso.

+0

gracias por el seguimiento. Otra gran respuesta. – user772110

2

Lo fundamental es probable que se está perdiendo es la siguiente:

  • En la mayoría de los lenguajes de programación, si usted dice "esta función devuelve cualquier tipo", significa que la función puede decidir qué tipo de valor que realmente devuelve.

  • En Haskell, si dices "esta función devuelve cualquier tipo", significa que la persona que llama puede decidir qué tipo debería ser. (!)

Así que si te escribo foo :: Int -> x, no puede simplemente devolver un String, porque puede ser que no pregunte por un String.Podría pedir un Customer, o un ThreadId, o cualquier cosa.

Obviamente, no hay manera de que foo sepa cómo crear un valor de todos los tipos posibles, incluso los que aún no existen. En resumen, es imposible escribir foo. Todo lo que intente le dará errores de tipo y no compilará.

(Advertencia: No es una manera hacerlo foo podía bucle infinito, o lanzar una excepción Pero no puede retorno un valor válido...)

No hay manera para que una función sea capaz de crear valores de cualquier tipo posible. Pero es perfectamente posible para una función para mover datos sin importar de qué tipo es. Por lo tanto, si ve una función que acepta cualquier tipo de datos, lo único que puede hacer con ella es moverla.

Alternativamente, si el tipo tiene que pertenecer a una clase específica, entonces la función puede usar los métodos de esa clase en él. (Podría . No tiene por qué, pero puede si quiere.)

Fundamentalmente, esto es por lo que en realidad se puede decir lo que hace una función con sólo mirar su firma Tipo. La firma tipo te dice qué función "sabe" la función sobre los datos que se le darán y, por lo tanto, qué posibles operaciones podría realizar. Esta es la razón por la cual la búsqueda de una función Haskell por su tipo de firma es muy útil.

Has escuchado la expresión "en Haskell, si se compila, por lo general funciona bien"? Bueno, esta es la razón por la cual ;-)

+0

¡Esta es una excelente explicación de las ideas detrás de la parametricidad! Ahora solo necesitamos una traducción igualmente comprensible de las pruebas de Wadler en "Teoremas gratis". – dfeuer

+0

@dfeuer ¡Si encuentra uno, hágamelo saber! Sigo viendo esa frase, pero no tengo ni idea de lo que significa ... – MathematicalOrchid

Cuestiones relacionadas