haskell - ¿Cuál es la base teórica para los tipos existenciales?
types type-systems (3)
Antes que nada, eche un vistazo a la "correspondencia de Curry Howard" que establece que los tipos en un programa de computadora corresponden a fórmulas en lógica intuicionista. La lógica intuitiva es exactamente como la lógica "regular" que aprendiste en la escuela pero sin la ley de la eliminación de la negación media o doble excluida:
No es un axioma: P ⇔ ¬¬P (pero P ⇒ ¬ ¬ P está bien)
No es un axioma: P ∨ ¬P
Leyes de la lógica
Estás en el camino correcto con las leyes de DeMorgan, pero primero vamos a usarlas para derivar algunas nuevas. La versión relevante de las leyes de DeMorgan es:
- ∀x. P (x) = ¬∃x. ¬P (x)
- ∃x. P (x) = ¬∀x. ¬P (x)
Podemos derivar (∀x. P ⇒ Q (x)) = P ⇒ (∀x. Q (x)):
- (∀x. P ⇒ Q (x))
- (∀x. ¬P ∨ Q (x))
- ¬P ∨ (∀x. Q (x))
- P ⇒ (∀x. Q)
Y (∀x. Q (x) ⇒ P) = (∃x. Q (x)) ⇒ P (este se usa a continuación):
- (∀x. Q (x) ⇒ P)
- (∀x. ¬Q (x) ∨ P)
- (¬¬∀x. ¬Q (x)) ∨ P
- (¬∃x. Q (x)) ∨ P
- (∃x. Q (x)) ⇒ P
Tenga en cuenta que estas leyes también se sostienen en la lógica intuicionista. Las dos leyes que derivamos se citan en el documento a continuación.
Tipos simples
Los tipos más simples son fáciles de trabajar. Por ejemplo:
data T = Con Int | Nil
Los constructores y los usuarios tienen las siguientes firmas de tipo:
Con :: Int -> T
Nil :: T
unCon :: T -> Int
unCon (Con x) = x
Tipo de constructores
Ahora abordemos los constructores de tipos. Tome la siguiente definición de datos:
data T a = Con a | Nil
Esto crea dos constructores,
Con :: a -> T a
Nil :: T a
Por supuesto, en Haskell, las variables de tipo están implícitamente cuantificadas universalmente, por lo que estas son realmente:
Con :: ∀a. a -> T a
Nil :: ∀a. T a
Y el acceso es igualmente fácil:
unCon :: ∀a. T a -> a
unCon (Con x) = x
Tipos cuantificados
Agreguemos el cuantificador existencial, ∃, a nuestro tipo original (el primero, sin el constructor de tipo). En lugar de introducirlo en la definición de tipo, que no se parece a la lógica, introdúzcalo en las definiciones de constructor / acceso, que se parecen a la lógica. Arreglaremos la definición de datos más tarde para que coincida.
En lugar de Int , ahora usaremos ∃x. t ∃x. t . Aquí, t es algún tipo de expresión de tipo.
Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)
Con base en las reglas de la lógica (la segunda regla anterior), podemos reescribir el tipo de Con para:
Con :: ∀x. t -> T
Cuando movimos el cuantificador existencial al exterior (forma de prenexo), se convirtió en un cuantificador universal.
Entonces los siguientes son teóricamente equivalentes:
data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil
Excepto que no existe una sintaxis para exists en Haskell.
En lógica no intuicionista, es permisible derivar lo siguiente del tipo de unCon :
unCon :: ∃ T -> t -- invalid!
La razón por la cual esto no es válido es porque tal transformación no está permitida en la lógica intuicionista. Por lo tanto, es imposible escribir el tipo para unCon sin una palabra clave exists , y es imposible poner la firma del tipo en forma de prenexo. Es difícil hacer que un comprobador de tipos garantice la terminación en tales condiciones, razón por la cual Haskell no admite cuantificadores existenciales arbitrarios.
Fuentes
"Polimorfismo de primera clase con inferencia de tipo", Mark P. Jones, Actas del XXIV simposio ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación ( web )
The Haskell Wiki hace un buen trabajo al explicar cómo usar tipos existenciales, pero no entiendo muy bien la teoría detrás de ellos.
Considera este ejemplo de tipo existencial:
data S = forall a. Show a => S a -- (1)
para definir un contenedor de tipo para cosas que podemos convertir a una String . La wiki menciona que lo que realmente queremos definir es un tipo como
data S = S (exists a. Show a => a) -- (2)
es decir, un verdadero tipo "existencial". En términos generales, pienso en esto diciendo que "el constructor de datos S toma cualquier tipo para el que exista una instancia de Show y lo envuelve". De hecho, probablemente puedas escribir un GADT de la siguiente manera:
data S where -- (3)
S :: Show a => a -> S
No intenté compilar eso, pero parece que debería funcionar. Para mí, el GADT es obviamente equivalente al código (2) que nos gustaría escribir.
Sin embargo, no es completamente obvio para mí por qué (1) es equivalente a (2). ¿Por qué mover el constructor de datos al exterior convierte el campo en una exists ?
Lo más parecido que puedo pensar son las Leyes de De Morgan en lógica, donde intercambiar el orden de una negación y un cuantificador convierte los cuantificadores existenciales en cuantificadores universales, y viceversa:
¬(∀x. px) ⇔ ∃x. ¬(px)
pero los constructores de datos parecen ser una bestia totalmente diferente al operador de negación.
¿Cuál es la teoría que subyace a la capacidad de definir tipos existenciales usando forall lugar de lo que no exists ?
Está indicado en el artículo wiki de haskell que vinculó. Tomaré prestadas algunas líneas de código y comentarios para tratar de explicar.
data T = forall a. MkT a
Aquí tienes un tipo T con un constructor de tipo MkT :: forall a. a -> T MkT :: forall a. a -> T , ¿verdad? MkT es (más o menos) una función, por lo que para cada tipo posible a , la función MkT tiene a -> T tipo a -> T Por lo tanto, aceptamos que al usar ese constructor podemos construir valores como [MkT 1, MkT ''c'', MkT "hello"] , todos de tipo T
foo (MkT x) = ... -- what is the type of x?
Pero, ¿qué ocurre cuando intentas extraer (por ejemplo, mediante la coincidencia de patrones) el valor incluido dentro de un T ? Su anotación de tipo solo dice T , sin ninguna referencia al tipo del valor realmente contenido en él. Solo podemos estar de acuerdo en el hecho de que, sea lo que sea, tendrá un (y solo uno) tipo; ¿Cómo podemos decir esto en Haskell?
x :: exists a. a
Esto simplemente dice que existe un tipo a al que pertenece x . En este punto, debe quedar claro que, al eliminar todo el MkT de la definición de MkT y al especificar explícitamente el tipo de valor envuelto (que exists a. a ), podemos lograr el mismo resultado.
data T = MkT (exists a. a)
El resultado final es el mismo también si agrega condiciones en las clases de tipos implementadas como en sus ejemplos.
Plotkin y Mitchell establecieron una semántica para los tipos existenciales, en su famoso artículo, que hacía la conexión entre los tipos abstractos en los lenguajes de programación y los tipos existenciales en la lógica,
Mitchell, John C .; Plotkin, Gordon D .; Los tipos abstractos tienen tipo existencial , transacciones ACM en lenguajes y sistemas de programación, vol. 10, No. 3, julio de 1988, pp. 470-502
A un nivel alto,
Las declaraciones abstractas de tipos de datos aparecen en lenguajes de programación tipados como Ada, Alphard, CLU y ML. Esta forma de declaración vincula una lista de identificadores a un tipo con operaciones asociadas, un "valor" compuesto que llamamos álgebra de datos. Utilizamos un cálculo lambda tipado de segundo orden SOL para mostrar cómo se pueden dar tipos de álgebras de datos, pasan como parámetros y se devuelven como resultados de llamadas a funciones. En el proceso, discutimos la semántica de las declaraciones de tipos de datos abstractos y revisamos una conexión entre los lenguajes de programación tipados y la lógica constructiva.