该哈斯克尔维基做了解释如何使用存在类型的一个很好的工作,但我不太神交背后的理论.
考虑这个存在类型的例子:
data S = forall a. Show a => S a -- (1)
为我们可以转换为的东西定义一个类型包装器String.维基提到我们真正想要定义的是类似的类型
data S = S (exists a. Show a => a) -- (2)
即一个真正的"存在主义"类型 - 松散地我认为这是"数据构造函数S采用Show实例存在并包装它的任何类型".事实上,你可能会写一个GADT如下:
data S where -- (3)
S :: Show a => a -> S
我没有尝试过编译,但似乎它应该可行.对我来说,GADT显然等同于我们想写的代码(2).
然而,对我来说,完全不明白为什么(1)等同于(2).为什么将数据构造函数移到外面forall变成了exists？
我能想到的最接近的是De Morgan的逻辑定律,其中交换否定的顺序和量词将存在量词转换为通用量词,反之亦然:
¬(?x. px) ? ?x. ¬(px)
但是数据构造函数似乎与否定运算符完全不同.
使用forall而不是不存在来定义存在类型的能力背后的理论是什么exists？