haskell - ¿Qué es la predicatividad?

type-theory

Question

Tengo una intuición bastante decente sobre los tipos que Haskell prohíbe como "impredicativos": aquellos en los que aparece un argumento en un argumento para un constructor de tipos distinto de -> . Pero, ¿qué es la predicatividad? ¿Qué lo hace importante? ¿Cómo se relaciona con la palabra "predicado"?

Answer 1

La pregunta central de estos sistemas de tipo es: "¿Se puede sustituir un tipo polimórfico por una variable de tipo?". Los sistemas de tipo predictivo son la respuesta sin sentido de la escuela, "ABSOLUTAMENTE NO", mientras que los sistemas de tipo impredicativo son su compañero despreocupado que piensa que suena como una idea divertida y ¿qué podría salir mal?

Ahora, Haskell enturbia un poco la discusión porque cree que el polimorfismo debería ser útil pero invisible. Entonces, durante el resto de esta publicación, escribiré en un dialecto de Haskell donde los usos de forall no solo están permitidos sino también obligatorios. De esta forma podemos distinguir entre el tipo a , que es un tipo monomórfico que extrae su valor de un entorno de tipado que podemos definir más adelante, y el tipo para todo forall a. a forall a. a , que es uno de los tipos polimórficos más difíciles de habitar. También permitiremos que forall vaya prácticamente a cualquier lugar en un tipo: como veremos, GHC restringe su sintaxis de tipo como un mecanismo "fail-fast" en lugar de un requisito técnico.

Supongamos que le hemos dicho al compilador id :: forall a. a -> a id :: forall a. a -> a . ¿Podemos luego pedir usar id como si tuviera el tipo (forall b. b) -> (forall b. b) ? Los sistemas de tipo impredicativo están bien con esto, porque podemos instanciar el cuantificador en el tipo de id para forall b. b forall b. b , y sustituto forall b. b forall b. b por a en todas partes en el resultado. Los sistemas de tipo predicativo son un poco más cautelosos: solo se permiten los tipos monomórficos. (Entonces, si tuviéramos un b particular, podríamos escribir id :: b -> b ).

Hay una historia similar sobre [] :: forall a. [a] [] :: forall a. [a] y (:) :: forall a. a -> [a] -> [a] (:) :: forall a. a -> [a] -> [a] . Mientras que tu compañero despreocupado puede estar bien con [] :: [forall b. b] [] :: [forall b. b] y (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] , la escuela predicativa no es, tanto. De hecho, como puede ver en los dos únicos constructores de listas, no hay forma de producir listas que contengan valores polimórficos sin instanciar la variable de tipo en sus constructores a un valor polimórfico. Entonces, aunque el tipo [forall b. b] [forall b. b] está permitido en nuestro dialecto de Haskell, no es realmente sensato; no hay términos (de terminación) de ese tipo. Esto motiva la decisión de GHC de quejarse si siquiera piensa en un tipo de este tipo: es la forma del compilador de decirle "no se moleste". *

Bueno, ¿qué hace que la escuela sea tan estricta? Como de costumbre, la respuesta es hacer posible el control de tipos y la inferencia de tipos. La inferencia tipo para tipos impredicativos es correcta. La comprobación de tipos parece que podría ser posible , pero es terriblemente complicado y nadie quiere mantener eso.

Por otro lado, algunos podrían objetar que GHC está perfectamente satisfecho con algunos tipos que parecen requerir impredicativity:

> :set -Rank2Types
> :t id :: (forall b. b) -> (forall b. b)
{- no complaint, but very chatty -}

Resulta que algunas versiones ligeramente restringidas de impredicativity no son tan malas: específicamente, el tipo de comprobación de tipos de rango superior (que permiten que las variables de tipo sean sustituidas por tipos polimórficos cuando son solo argumentos para (->) ) es relativamente simple . Se pierde la inferencia de tipo por encima del rango 2 y los tipos principales por encima del rango 1, pero a veces los tipos de rango más altos son justo lo que ordenó el médico.

Sin embargo, ¡no sé nada sobre la etimología de la palabra!

* Quizás se pregunte si puede hacer algo como esto:

data FooTy a where
     FooTm :: FooTy (forall a. a)

Entonces obtendrías un término ( FooTm ) cuyo tipo tuviera algo polimórfico como argumento para algo que no sea (->) (a saber, FooTy ), no tienes que cruzar la escuela para hacerlo, y entonces la creencia "aplicando" las cosas que no son (->) a los tipos polimórficos no son útiles porque no se puede hacer que "sean invalidadas". GHC no le permite escribir FooTy , y admitiré que no estoy seguro de si hay una razón de principio para la restricción o no.

(Actualización rápida algunos años después: hay una buena razón de principio para que FooTm todavía no está bien. A saber, la forma en que las GADT se implementan en GHC es a través de igualdades de tipo, por lo que el tipo expandido de FooTm es realmente FooTm :: forall a. (a ~ forall b. b) => FooTy (forall b. b) . Por lo tanto, para usar realmente FooTm , uno necesitaría instanciar una variable tipo con un tipo polimórfico. Gracias a Stephanie Weirich por señalarme esto.)

Answer 2

Me gustaría hacer un comentario sobre el tema de la etimología, ya que la respuesta de @ sclv no es del todo correcta (etimológicamente, no conceptualmente).

Retrocede en el tiempo, a los días de Russell, cuando todo se basa en la teoría, incluida la lógica. Una de las nociones lógicas de particular importancia es el "principio de comprensión"; es decir, dado un predicado lógico φ:A→2 nos gustaría tener algún principio para determinar el conjunto de todos los elementos que satisfacen ese predicado, escrito como " {x | φ(x) } " o alguna variación sobre el mismo. El punto clave a tener en cuenta es que los "conjuntos" y los "predicados" se consideran como cosas fundamentalmente diferentes: los predicados son asignaciones de objetos a valores de verdad, y los conjuntos son objetos. Por lo tanto, por ejemplo, podemos permitir la cuantificación de conjuntos, pero no la cuantificación de los predicados.

Ahora, Russell estaba bastante preocupado por su paradoja epónima, y ​​buscó la forma de deshacerse de ella. Existen numerosas correcciones, pero la que interesa aquí es restringir el principio de comprensión. Pero primero, la definición formal del principio: ∃S.∀xS x ↔︎ φ(x) ; es decir, para nuestro particular φ existe algún objeto (es decir, conjunto) S tal que para cada objeto (también un conjunto, pero pensado como un elemento) x , tenemos ese S x (se puede pensar que esto tiene el significado " x∈S ", aunque los lógicos de la época le dieron a" ∈ "un significado diferente a la mera yuxtaposición) es verdadero solo en caso de que φ(x) sea ​​verdadero. Si tomamos el principio exactamente como está escrito, terminamos con una teoría impredicativa. Sin embargo, podemos poner restricciones sobre las cuales φ se nos permite comprender. (Por ejemplo, si decimos que φ no debe contener ningún cuantificador de segundo orden.) Por lo tanto, para cualquier restricción R , si un conjunto S es determinado (es decir, generado a través de la comprensión) por algún R -predicado, entonces decimos que S es " R -predicativo". Si cada conjunto en nuestro idioma es R predictivo, entonces decimos que nuestro lenguaje es " R -predativo". Y luego, como suele ser el caso con las cosas con prefijo con guiones, el prefijo se quita y se deja implícito, de ahí los lenguajes "predicativos". Y, naturalmente, los lenguajes que no son predicativos son "impredicativos".

Esa es la etimología de la vieja escuela. Desde esos días, los términos han ido y han cobrado vida propia. Las formas en que usamos "predicativo" e "impredicativo" hoy en día son bastante diferentes, porque las cosas que nos preocupan han cambiado. Por lo tanto, a veces puede ser un poco difícil ver cómo diablos nuestro uso moderno se relaciona con esto. Honestamente, no creo que saber la etimología realmente ayude a ninguno en términos de entender de qué se tratan realmente las palabras (en estos días).

Answer 3

Permítanme agregar un punto sobre el tema "etimología", ya que la otra respuesta de @DanielWagner cubre gran parte del terreno técnico.

Un predicado sobre algo como a es a -> Bool . Ahora bien, una lógica de predicados es una que puede en cierto sentido razonar sobre los predicados, de modo que si tenemos un predicado P y podemos hablar, para un a dado, P(a) , ahora en una "lógica de predicados" (como la primera -orden lógica) también podemos decir ∀a. P(a) ∀a. P(a) . Entonces, podemos cuantificar las variables y discutir el comportamiento de los predicados sobre tales cosas.

Ahora, a su vez, decimos que una afirmación es predicativa si todas las cosas a las que se aplica un predicado se introducen antes . Entonces las declaraciones se "basan en" cosas que ya existen. A su vez, una afirmación es impredicativa si, en cierto sentido, puede referirse a sí misma por sus "bootstraps".

Entonces, en el caso de, por ejemplo, el ejemplo de id anterior, encontramos que podemos dar un tipo a la id manera que lleve algo del tipo de id a otra cosa del tipo de id . Así que ahora podemos darle a una función un tipo en el que una variable cuantificada (introducida por forall a. ) Puede "expandirse" para ser del mismo tipo que la función entera.

Por lo tanto, la impredicatividad introduce la posibilidad de una cierta "auto referencia". Pero espera, podrías decir, ¿no conduciría esto a una contradicción? La respuesta es: "bueno, a veces". En particular, el "Sistema F" que es el cálculo lambda polimórfico y el "núcleo" esencial del lenguaje "central" de GHC permite una forma de impredicatividad que, no obstante, tiene dos niveles: el nivel de valor y el nivel de tipo, que está permitido cuantificarse sobre sí mismo. En esta estratificación de dos niveles, podemos tener impredicativity y no contradicción / paradoja.

Aunque tenga en cuenta que este truco es muy delicado y fácil de arruinar por la adición de más características, como lo indica esta colección de artículos de Oleg: http://okmij.org/ftp/Haskell/impredicativity-bites.html