tuplas - switch en haskell

Haskell patrón de coincidencia "diverge" y ⊥

Question

Estoy tratando de entender el informe Haskell 2010, sección 3.17.2 "Semántica informal de coincidencia de patrones". La mayor parte de esto, en relación con una coincidencia de patrón que tiene éxito o falla, parece sencillo, sin embargo, tengo dificultades para entender el caso que se describe como la coincidencia de patrón "divergente".

Estoy semi persuadido, significa que el algoritmo de coincidencia no "converge" a una respuesta (por lo tanto, la función de coincidencia nunca regresa). Pero si no se devuelve, entonces, ¿cómo puede devolver un valor, como lo sugiere el método "es decir, retorno return" entre paréntesis? ¿Y qué significa "devolver" de todos modos? ¿Cómo se maneja ese resultado?

El elemento 5 tiene el punto particularmente confuso (para mí) "Si el valor es, la coincidencia diverge". ¿Esto solo dice que un valor de ⊥ produce un resultado de coincidencia de ⊥ ? (Dejando de lado que no sé lo que significa ese resultado!)

¡Cualquier iluminación, posiblemente con un ejemplo, sería apreciada!

Addendum después de un par de respuestas largas: Gracias Tikhon y todo por tu esfuerzo.

Parece que mi confusión proviene de que existen dos reinos diferentes de explicación: el reino de las características y comportamientos de Haskell, y el reino de las matemáticas / semántica, y en la literatura de Haskell estos dos se entremezclan en un intento de explicar el primero en términos de este último , sin suficientes indicadores (a mí) en cuanto a qué elementos pertenecen a qué.

Evidentemente, "bottom" ⊥ está en el dominio semántico, y no existe como un valor dentro de Haskell (es decir, no se puede escribir, nunca se obtiene un resultado que se imprima como " ⊥ ").

Entonces, cuando la explicación dice que una función "devuelve ⊥ ", esto se refiere a una función que realiza cualquiera de una serie de cosas inconvenientes, como no terminar, lanzar una excepción o devolver "indefinido". ¿Está bien?

Además, aquellos que comentaron que ⊥ realidad es un valor que puede transmitirse, realmente están pensando en enlaces a funciones ordinarias a las que aún no se les ha pedido que evalúen ("bombas sin explotar", por así decirlo) y quizás nunca, debido a la pereza, ¿verdad?

Answer 1

Semantica de denotacion

Entonces, brevemente la semántica denotacional, que es donde vive ⊥ , es un mapeo de los valores de Haskell a algún otro espacio de valores. Usted hace esto para dar significado a los programas de una manera más formal que solo hablar sobre lo que deberían hacer los programas; usted dice que deben respetar su semántica de denotación.

Entonces, para Haskell, a menudo se piensa en cómo las expresiones de Haskell denotan valores matemáticos. Con frecuencia ve los corchetes de Strachey ⟦·⟧ para denotar el "mapeo semántico" de Haskell a Math. Finalmente, queremos que nuestros corchetes semánticos sean compatibles con las operaciones semánticas. Por ejemplo

⟦x + y⟧ = ⟦x⟧ + ⟦y⟧

donde en el lado izquierdo + está la función Haskell (+) :: Num a => a -> a -> a en el lado derecho es la operación binaria en un grupo conmutativo. Si bien es genial, porque sabemos que podemos usar las propiedades del mapa semántico para saber cómo deberían funcionar nuestras funciones Haskell. A saber, escribamos la propiedad conmutativa "en Matemáticas"

 ⟦x⟧ + ⟦y⟧ == ⟦y⟧ + ⟦x⟧
= ⟦x + y⟧ == ⟦y + x⟧
= ⟦x + y == y + x⟧

donde el tercer paso también indica que Haskell (==) :: Eq a => a -> a -> a debe tener las propiedades de una relación de equivalencia matemática.

Bueno, excepto ...

De todos modos, eso está muy bien hasta que recordemos que las computadoras son cosas finitas y que a Maths no le importa mucho (a menos que estés usando lógica intuicionista y luego obtengas Coq). Por lo tanto, debemos tomar nota de los lugares donde nuestra semántica no sigue Matemáticas del todo bien. Aquí hay tres ejemplos.

⟦undefined⟧ = ??
⟦error "undefined"⟧ = ??
⟦let x = x in x⟧ = ??

Aquí es donde ⊥ entra en juego. Simplemente afirmamos que, en lo que respecta a la semántica denotacional de Haskell, cada uno de esos ejemplos también podría significar (el concepto matemático / semántico recientemente introducido) ⊥ . ¿Cuáles son las propiedades matemáticas de ⊥ ? Bueno, aquí es donde empezamos a sumergirnos realmente en lo que es el dominio semántico y empezar a hablar de la monotonicidad de las funciones y los CPO y similares. Esencialmente, sin embargo, ⊥ es un objeto matemático que juega aproximadamente el mismo juego que la no terminación. Para el punto de vista del modelo semántico, es tóxico e infecta expresiones con su no determinismo tóxico.

Pero no es un concepto de Haskell-the-language, solo un tema de dominio semántico de Haskell. En Haskell tenemos undefined , error y bucle infinito. Esto es importante.

Comportamiento extra semántico (nota al margen)

Así que la semántica de ⟦undefined⟧ = ⟦error "undefined"⟧ = ⟦let x = x in x⟧ = ⊥ está claro una vez que entendemos los significados matemáticos de ⊥ , pero también está claro que cada uno tiene diferentes efectos "en realidad" . Esto es algo así como el "comportamiento indefinido" de C ... es un comportamiento indefinido en lo que respecta al dominio semántico. Podrías llamarlo semánticamente inobservable.

Entonces, ¿cómo regresa el patrón coincidente ⊥ ?

Entonces, ¿qué significa "semánticamente" devolver ⊥ ? Bueno, ⊥ es un valor semántico perfectamente válido que tiene la propiedad de infección que modela el no determinismo (o el lanzamiento asincrónico de errores). Desde el punto de vista semántico, es un valor perfectamente válido que puede devolverse tal como está.

Desde el punto de vista de la implementación, tiene una serie de opciones, cada una de las cuales se asigna al mismo valor semántico. undefined no está del todo bien, ni está ingresando a un bucle infinito, así que si va a elegir un comportamiento semánticamente indefinido, también puede elegir uno que sea útil y arrojar un error.

*** Exception: <interactive>:2:5-14: Non-exhaustive patterns in function cheers

Answer 2

El valor es ⊥, generalmente se pronuncia "fondo". Es un valor en el sentido semántico, no es un valor de Haskell normal per se . Representa cálculos que no producen un valor de Haskell normal: excepciones y bucles infinitos, por ejemplo.

La semántica se trata de definir el "significado" de un programa. En Haskell, generalmente hablamos de semántica denotacional, donde el valor es un objeto matemático de algún tipo. El ejemplo más trivial sería que la expresión 10 (pero también la expresión 9 + 1 ) tiene denotaciones del número 10 (en lugar del valor 10 Haskell ). Normalmente escribimos que ⟦9 + 1⟧ = 10 lo que significa que la denotación de la expresión de Haskell 9 + 1 es el número 10.

Sin embargo, ¿qué hacemos con una expresión como let x = x in x ? No hay valor de Haskell para esta expresión. Si tratara de evaluarlo, simplemente nunca terminaría. Además, no es obvio a qué objeto matemático corresponde esto. Sin embargo, para razonar sobre los programas, necesitamos dar alguna denotación para ello. Entonces, esencialmente, solo creamos un valor para todos estos cálculos, y llamamos el valor ⊥ (parte inferior).

Entonces, ⊥ es solo una manera de definir lo que significa "un cálculo" que no devuelve.

También definimos otros cálculos como undefined y error "some message" como ⊥ porque tampoco tienen valores normales obvios. Así que lanzar una excepción corresponde a ⊥ . Esto es exactamente lo que sucede con una coincidencia de patrón fallida.

La forma habitual de pensar acerca de esto es que cada tipo de Haskell se "levanta": contiene ⊥ . Es decir, Bool corresponde a {⊥, True, False} lugar de solo {True, False} . Esto representa el hecho de que no se garantiza que los programas de Haskell terminen y pueden tener excepciones. Esto también es cierto cuando define su propio tipo: el tipo contiene todos los valores que definió para él, así como también ⊥ .

Curiosamente, dado que Haskell no es estricto, exist puede existir en el código normal. Por lo tanto, podría tener un valor como Just ⊥ , y si nunca lo evalúa, todo funcionará bien. Un buen ejemplo de esto es const : const 1 ⊥ evalúa como 1 . Esto funciona también para coincidencias de patrones fallidos:

const 1 (let Just x = Nothing in x) -- 1

Debe leer la sección sobre semántica de denotación en el WikiBook de Haskell. Es una introducción muy accesible al tema, que personalmente me parece muy fascinante.