losHaskell Wiki hace un buen trabajo explicando cómo usar los tipos existenciales, pero no estoy muy de acuerdo con la teoría detrás de ellos.

Considere este ejemplo de un tipo existencial:

data S = forall a. Show a => S a      -- (1)

para definir un tipo de envoltura para cosas que podemos convertir a unaString. La wiki menciona que lo que nosotrosDe Verdad querer 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 como "el constructor de datosS Toma cualquier tipo para el cual unShow ejemploexiste y lo envuelve ". De hecho, probablemente puedas escribir un GADT de la siguiente manera:

data S where                          -- (3)
    S :: Show a => a -> S

No he intentado 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 da vuelta alforall en unaexists?

Lo más cercano que puedo pensar sonLas leyes 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 se encuentra detrás de la capacidad de definir tipos existenciales utilizandoforall en lugar de lo inexistenteexists?