mexico - ¿Por qué no hay una palabra clave "Existir" en Haskell para la cuantificación existencial?

haskell logo

Question

Según la documentación de GHC, dada la siguiente declaración:

data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

entonces

MkFoo :: forall a. a -> (a -> Bool) -> Foo

Es (casi) isomorfo a la siguiente declaración de pseudo-Haskell

MkFoo :: (exists a . (a, a -> Bool)) -> Foo

Por lo tanto, no hay necesidad de una palabra clave "Existir" separada. Porque:

Los programadores de Haskell pueden pensar con seguridad en el tipo ordinario cuantificado universalmente que se ha indicado anteriormente.

Pero no estoy seguro de lo que eso significa. ¿Puede alguien explicarme por qué podemos usar el cuantificador universal para expresar la cuantificación existencial?

Answer 1

En lógica (clásica o intuicionista), las fórmulas

(exists x. p x) -> q
forall x. (p x -> q)

son equivalentes (tenga en cuenta que q no depende de x arriba). Esto se puede utilizar para expresar la cuantificación existencial en términos de cuantificación universal, siempre que las mentiras existenciales en el lado izquierdo en una implicación. (Aquí hay una proof clásica.)

En programación funcional, puedes lograr lo mismo. En lugar de escribir

-- Pseudo-Haskell follows
f :: (exists a. (a, a->Int)) -> Int
f (x,h) = h x

nosotros podemos usar

-- Actual Haskell
f :: forall a. (a, a->Int) -> Int
f (x,h) = h x

por lo que podemos prescindir de la cuantificación existencial, al menos en casos como el anterior.

La cuantificación existencial todavía es necesaria cuando ocurre no a la izquierda de una flecha. Por ejemplo,

g :: exists a. (a, a->Int)
g = (2 :: Int, /x -> x+3)

Por desgracia, Haskell optó por no incluir estos tipos. Probablemente, esta elección se tomó para evitar que el sistema de tipos ya sofisticado se vuelva demasiado complejo.

Sin embargo, Haskell obtuvo tipos de datos existenciales, que solo requieren envolver / desempaquetar un constructor alrededor de lo existencial. Por ejemplo, usando la sintaxis de GADT, podemos escribir:

data Ex where
  E :: forall a. (a, a->Int) -> Ex
g :: Ex
g = E (2 :: Int, /x -> x+3)

Finalmente, permítanme agregar que los existenciales también pueden simularse por tipos de rango 2 y paso de continuación:

g :: forall r. (forall a. (a, a->Int) -> r) -> r
g k = k (2 :: Int, /x -> x+3)

Answer 2

Lo primero que hay que notar es que el cuantificador forall aparece en el lado derecho del signo igual, por lo que está asociado con un constructor de datos (no tipo): MkFoo . Por lo tanto, el tipo Foo no dice nada sobre a .

Nos encontramos de nuevo cuando intentamos hacer coincidir patrones en valores de tipo Foo . En ese momento, no sabrá casi nada sobre los componentes de MkFoo , excepto que existen (debe existir un tipo utilizado para llamar a MkFoo ) y que el primer componente se puede usar como un argumento para el segundo componente, que es un función:

f :: Foo -> Bool
f (MkFoo val fn) = fn val

Answer 3

Si observa el tipo de constructores de datos, notará que usamos de manera similar -> para significar de alguna manera producto. P.ej

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

realmente significa que estamos usando (:) para empaquetar un a junto con una lista de tipo [a] y entregar una lista de tipo [a] .

En su ejemplo, el uso de forall simplemente significa que MkFoo , como constructor, está dispuesto a empaquetar cualquier tipo a . Cuando lea (exists a . (a, a -> Bool)) -> Foo en la documentación de GHC, debe pensar que se trata de una versión no apurada del tipo original de MkFoo . La versión no apurada correspondiente de (:) sería (a, [a]) -> [a] .