存在类型的理论基础是什么？

Question

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

为可以转换为字符串的东西定义类型包装。wiki提到，我们真正想要定义的是一种类型，比如

data S = S (exists a. Show a => a)    -- (2)

即一个真正的“存在”类型--我松散地认为这是说“数据构造函数s接受show实例存在的任何类型并包装它”。实际上，您可以编写一个GADT，如下所示：

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

我没有试过编译它，但它似乎应该可以工作。对我来说，GADT显然等同于我们想要编写的代码（2）。

¬(∀x. px) ⇔ ∃x. ¬(px)

Answer 1

首先，看一看“库里霍华德对应关系”，它指出计算机程序中的类型对应于直觉逻辑中的公式。直觉逻辑就像你在学校里学的但没有排中律或双否定排除律的“规律性”逻辑：

>

不是公理:P，P（但P，P很好）

不是公理:P≠P

null

我们可以导出（公牛x.P Q(x)） = P（公牛x.Q(x)）：

1. （运行参数x.P Q(x))
2. (dx.píQ(x))
3. ，pø(uncx.Q(x))
4. P（运行参数Q)

和（unx.Q(x)P） = (x.Q(x)）P（下面使用这个）：

null

data T = Con Int | Nil

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

data T a = Con a | Nil

这将创建两个构造函数,

Con :: a -> T a
Nil :: T a

当然，在Haskell中，类型变量是隐式通用量化的，因此这些实际上是：

Con :: ∀a. a -> T a
Nil :: ∀a. T a

而访问者也同样容易：

unCon :: ∀a. T a -> a
unCon (Con x) = x

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

Con :: ∀x. t -> T

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

只是在Haskell中没有exists的语法。

在非直觉逻辑中，允许从uncon类型导出以下内容：

unCon :: ∃ T -> t -- invalid!

这是无效的原因是这样的转换在直觉逻辑中是不允许的。因此，在没有exists关键字的情况下，不可能为uncon编写类型，也不可能将类型签名设置为prenex形式。很难保证类型检查器在这种情况下终止，这就是Haskell不支持任意存在量词的原因。