pattern - multiplicar haskell

¿Cómo funciona ''indefinido'' en Haskell?

Question

Tengo curiosidad por el valor "indefinido" en Haskell. Es interesante porque puedes ponerlo en cualquier lugar, y Haskell será feliz. Los siguientes son todos a-ok

[1.0, 2.0, 3.0 , undefined]  ::[Float]
[1, 2 ,3 undefined, 102312] :: [Int]
("CATS!", undefined)  :: (String, String)
....and many more

¿Cómo funciona indefinido bajo el capó? ¿Qué hace posible tener datos de todos los tipos de datos? ¿Me sería posible definir un valor como este que pueda poner en cualquier lugar, o es este un caso especial?

Answer 1

¿Cómo funciona undefined ? Bueno, la mejor respuesta, en mi humilde opinión, es que no funciona . Pero para entender esa respuesta, tenemos que trabajar con sus consecuencias, que no son obvias para un recién llegado.

Básicamente, si tenemos undefined :: a , lo que eso significa para el sistema de tipos es que undefined puede aparecer en cualquier lugar. ¿Por qué? Porque en Haskell, siempre que vea una expresión que tenga algún tipo, puede especializar el tipo sustituyendo de manera consistente todas las instancias de cualquiera de sus variables de tipo por cualquier otro tipo. Ejemplos familiares serían cosas como esta:

map :: (a -> b) -> [a] -> [b]

-- Substitute b := b -> x
map :: (a -> b -> c) -> [a] -> [b -> c]

-- Substitute a := Int
map :: (Int -> b -> c) -> [Int] -> [b -> c]

-- etc.

En el caso del map , ¿cómo funciona esto? Bueno, todo se reduce al hecho de que los argumentos del map proporcionan todo lo necesario para producir una respuesta, sin importar qué sustituciones y especializaciones realicemos para sus variables de tipo. Si tiene una lista y una función que consume valores del mismo tipo que los elementos de la lista, puede hacer lo que hace el mapa, punto.

Pero en el caso de undefined :: a , lo que significaría esta firma es que no importa a qué tipo se especialice, undefined es capaz de generar un valor de ese tipo. ¿Cómo puede hacerlo? Bueno, en realidad no puede, por lo que si un programa alcanza un paso donde se necesita el valor de undefined , no hay forma de continuar. Lo único que el programa puede hacer en ese momento es fallar.

La historia detrás de este otro caso es similar pero diferente:

loop :: a
loop = loop

Aquí, podemos probar que el loop tiene a tipo a por este argumento de sonido loco: supongamos que ese loop tiene el tipo a . Necesita producir un valor de tipo a . ¿Cómo puede hacerlo? Fácil, simplemente llama loop . ¡Presto!

Eso suena loco, ¿verdad? Bueno, la cuestión es que realmente no es diferente de lo que está pasando en la segunda ecuación de esta definición de map :

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

En esa segunda ecuación, fx tiene el tipo b , y (fx:) tiene el tipo [b] -> [b] ; Ahora para concluir nuestra prueba de que el map hecho tiene el tipo que nuestra firma afirma, debemos producir un [b] . Entonces, ¿cómo lo estamos haciendo? ¡Suponiendo que el map tiene el tipo que estamos tratando de demostrar que tiene!

La forma en que funciona el algoritmo de inferencia de tipos de Haskell es que primero adivina que el tipo de expresión es a , y luego solo cambia su suposición cuando encuentra algo que contradice esa suposición. chequeos de tipo undefined a porque es una mentira descarada. loop pruebas de tipo de loop realizan en a porque la recursividad está permitida, y todo lo que se hace en loop es repetido

EDIT: ¿Qué diablos, bien podría explicar un ejemplo. Aquí hay una demostración informal de cómo inferir el tipo de map de esta definición:

map f [] = []
map f (x:xs) = f x : map f xs

Dice así:

1. Comenzamos asumiendo provisionalmente ese map :: a .
2. Pero el mapa toma dos argumentos, por lo que no puede ser el tipo. Revisamos nuestro supuesto a esto: map :: a -> b -> c; f :: a map :: a -> b -> c; f :: a .
3. Pero como podemos ver en la primera ecuación, el segundo argumento es una lista: map :: a -> [b] -> c; f :: a map :: a -> [b] -> c; f :: a .
4. Pero como también podemos ver en la primera ecuación, el resultado es también una lista: map :: a -> [b] -> [c]; f :: a map :: a -> [b] -> [c]; f :: a .
5. En la segunda ecuación, tenemos un patrón que coincide con el segundo argumento contra el constructor (:) :: b -> [b] -> [b] . Esto significa que en esa ecuación, x :: b xs :: [b] .
6. Considere el lado derecho de la segunda ecuación. Como el resultado del map f (x:xs) debe ser de tipo [c] , eso significa que fx : map f xs también debe ser de tipo [c] .
7. Dado el tipo de constructor (:) :: c -> [c] -> [c] , eso significa que fx :: c y map f xs :: [c] .
8. En (7) concluimos que el map f xs :: [c] . Habíamos asumido que en (6), y si hubiéramos llegado de otra manera en (7), habría sido un error de tipo. Ahora también podemos sumergirnos en esta expresión y ver qué tipos requiere esto de f y xs , pero para abreviar una historia más larga, todo se va a ver.
9. Como fx :: c y x :: b , debemos concluir que f :: b -> c . Así que ahora tenemos map :: (b -> c) -> [b] -> [c] .
10. Hemos terminado

El mismo proceso, pero para loop = loop :

1. Asumimos provisionalmente ese loop :: a .
2. loop no toma argumentos, por lo que su tipo es consistente con a hasta ahora
3. El lado derecho del loop es el loop , al que hemos asignado provisionalmente el tipo a , por lo que se comprueba.
4. No hay nada más que considerar; hemos terminado loop tiene tipo a .

Answer 2

Bueno, básicamente undefined = undefined - si intentas evaluarlo, obtienes un bucle sin fin. Pero Haskell no es un lenguaje estricto, por lo que head [1.0, 2.0, undefined] no evalúa todos los elementos de la lista, por lo que imprime 1.0 y termina. Pero si imprime show [1.0, 2.0, undefined] , verá [1.0,2.0,*** Exception: Prelude.undefined .

En cuanto a cómo puede ser de todos los tipos ... Bueno, si la expresión es de tipo A , significa que evaluarla producirá un valor de tipo A , o la evaluación se desviará, sin generar ningún valor. Ahora, undefined siempre divergen, por lo que se ajusta a la definición para cada tipo A imaginable.

Además, una buena publicación de blog sobre los temas relacionados: http://james-iry.blogspot.ru/2009/08/getting-to-bottom-of-nothing-at-all.html

Answer 3

Hay dos cosas separadas a tener en cuenta acerca de indefinido:

• Puedes poner indefinido en casi todas partes y el typechecker estará feliz. Es porque undefined tiene tipo (para todos a. A).
• Puede poner indefinido en casi todas partes y tendrá una representación bien definida en el tiempo de ejecución.

Para el segundo, el comentario de GHC dice claramente:

La representación de ⊥ debe ser un puntero: es un objeto que, cuando se evalúa, lanza una excepción o entra en un bucle infinito.

Para obtener más detalles, puede leer el G-Machine sin etiquetas sin etiquetas .

Answer 4

La propiedad interesante que está examinando es que undefined tiene el tipo a para cualquier tipo que elijamos, es decir, undefined :: a a sin restricciones. Como otros lo han señalado, undefined podría considerarse como un error o un bucle infinito. Me gustaría argumentar que es mejor pensarlo como "la declaración vacuamente verdadera". Es un agujero casi inevitable en cualquier sistema de tipo estrechamente relacionado con el problema de la detención, pero es divertido pensar en ello desde el punto de vista de la lógica.

Una forma de pensar acerca de la programación con tipos es que es un rompecabezas. Alguien le da un tipo y le pide que implemente una función que sea de ese tipo. Por ejemplo

Question:    fn  ::  a -> a
Answer:      fn  =  /x -> x

es fácil Necesitamos producir un a para cualquier tipo a , pero nos dan uno como entrada para que podamos devolverlo.

Con undefined , este juego siempre es fácil.

Question:    fn  ::  Int -> m (f [a])
Answer:      fn  =  /i   -> undefined    -- backdoor!

Así que vamos a deshacernos de él. Darle sentido a lo undefined es más fácil cuando vives en un mundo sin él. Ahora nuestro juego se vuelve más difícil. A veces es posible

Question:    fn  :: (forall r. (a -> r) -> r) -> a
Answer:      fn  =  /f                        -> f id

¡Pero de repente a veces tampoco es posible!

Question:    fn  ::  a -> b
Answer:      fn  =   ???                  -- this is `unsafeCoerce`, btw.
                                          -- if `undefined` isn''t fair game,
                                          -- then `unsafeCoerce` isn''t either

¿O es eso?

-- The fixed-point combinator, the genesis of any recursive program

Question:    fix  ::  (a -> a) -> a
Answer:      fix  =   /f       -> let a = f a in a

                                          -- Why does this work?
                                          -- One should be thinking of Russell''s 
                                          -- Paradox right about now. This plays
                                          -- the same role as a non-wellfounded set.

Lo cual es legal porque el enlace de Haskell es perezoso y (generalmente) recursivo . Ahora estamos de oro.

Question:    fn   ::  a -> b
Answer:      fn   =  /a -> fix id         -- This seems unfair?

Incluso sin tener undefined incorporado, podemos reconstruirlo en nuestro juego usando cualquier bucle infinito antiguo. Los tipos echa un vistazo. Para evitar realmente que tengamos undefined en Haskell, deberíamos resolver el problema de la detención.

Question:    undefined  ::  a
Answer:      undefined  =   fix id

Ahora, como ha visto, undefined es útil para la depuración, ya que puede ser un marcador de posición para cualquier valor. Lamentablemente, es terrible para las operaciones, ya que conduce a un bucle infinito o a una caída inmediata. También es muy malo para nuestro juego porque nos permite hacer trampa. Finalmente, espero haber demostrado que es bastante difícil no tener undefined mientras su lenguaje tenga bucles (potencialmente infinitos).

Existen lenguajes como Agda y Coq que intercambian loops para eliminar realmente lo undefined . Lo hacen porque este juego que he inventado puede, en algunos casos, ser muy valioso. Puede codificar declaraciones de lógica y, por lo tanto, utilizarse para formar pruebas matemáticas muy, muy rigurosas. Sus tipos representan teoremas y sus programas son garantías de que ese teorema está fundamentado. La existencia de undefined significaría que todos los teoremas son sustentables y, por lo tanto, hacen que todo el sistema no sea confiable.

Pero en Haskell, estamos más interesados ​​en los bucles que en las pruebas, por lo que preferiríamos fix de estar seguros de que no había un undefined .

Answer 5

No hay nada realmente especial acerca de undefined . Es solo un valor excepcional: podría representarlo con un bucle infinito, un crash o un segfault. Una forma de escribirlo es como un fallo:

undefined :: a
undefined | False = undefined

O un bucle:

undefined = undefined

Es un valor excepcional que puede ser un elemento de cualquier tipo.

Dado que Haskell es perezoso, aún puede usar dichos valores en los cálculos. P.ej

 > length [undefined, undefined]
 2

Pero por lo demás, es solo una consecuencia natural del polimorfismo y la falta de rigor.

Answer 6

Si trato undefined en GHCi, obtengo una excepción:

Prelude> undefined
*** Exception: Prelude.undefined

Por lo tanto, supongo que solo se implementa como lanzando una excepción:
http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#g:2