Qual é a base teórica para os tipos existenciais?
oWiki do Haskell faz um bom trabalho de explicar como usar os tipos existenciais, mas não apresso a teoria por trás deles.
Considere este exemplo de um tipo existencial:
data S = forall a. Show a => S a -- (1)
para definir um tipo de wrapper para coisas que podemos converter para umString
. A wiki menciona que o que nósrealmente quer definir é um tipo como
data S = S (exists a. Show a => a) -- (2)
ou seja, um verdadeiro tipo "existencial" - vagamente eu penso nisso como "o construtor de dadosS
leva qualquer tipo para o qual umShow
instânciaexiste e envolve-o ". Na verdade, você provavelmente poderia escrever um GADT da seguinte maneira:
data S where -- (3)
S :: Show a => a -> S
Eu não tentei compilar isso, mas parece que deveria funcionar. Para mim, o GADT é obviamente equivalente ao código (2) que gostaríamos de escrever.
No entanto, não é totalmente óbvio para mim porque (1) é equivalente a (2). Por que mover o construtor de dados para o exteriorforall
em umexists
?
A coisa mais próxima que consigo pensar éLeis de De Morgan na lógica, onde o intercâmbio da ordem de uma negação e um quantificador transforma os quantificadores existenciais em quantificadores universais, e vice-versa:
¬(∀x. px) ⇔ ∃x. ¬(px)
mas os construtores de dados parecem ser uma fera totalmente diferente do operador de negação.
Qual é a teoria que está por trás da capacidade de definir tipos existenciais usandoforall
em vez do inexistenteexists
?