存在类型的理论基础是什么？ [英] What's the theoretical basis for existential types?
问题描述
Haskell Wiki 在解释如何使用存在类型方面做得很好，但我不完全赞同他们背后的理论。
考虑这种存在型的例子：
data S = forall a。显示a => S a - （1）
为我们可以转换为字符串。维基提到，我们真正想要定义的是一种类型，例如：
pre $ s $ s $ data S = S（存在a。显示a => a） - （2）
即一个真正的存在类型 - 松散地我认为这是数据构造函数 S 采用任何类型为显示实例存在并包装它。事实上，你可以写一个GADT，如下所示：
data S其中 - （3）
S： ：显示a => a - > S
我还没有试过编译它，但它好像应该可以工作。对我来说，GADT显然等同于我们想写的代码（2）。
然而，我完全不明白为什么（1）是相当于（2）。为什么将数据构造函数移到外部将 forall 转换为 exists ？ 我能想到的最接近的东西是德摩根定律在逻辑中，交换否定和量词的顺序将存在量词转换为通用量词，反之亦然：
¬（∀x。px）⇔∃x。 ¬（px）
但数据构造函数似乎与否定运算符完全不同。 p>
使用 forall 而不是不存在的<$ c定义存在类型的理论背后的理论是什么$ c>存在？
首先，看看咖喱霍华德通信它指出计算机程序中的类型对应于直觉逻辑中的公式。直觉逻辑就像你在学校学到的常规逻辑，但没有排除中间或双重否定排除的规律： 不是公理：P∨¬P
逻辑定律
您与DeMorgan的合作法律，但首先我们要用它们来衍生一些新的。德摩根法律的相关版本是：
（x））：
$ b $ ol
和（∀x.Q（x）⇒P）=（∃x.Q（x））⇒P （这个在下面使用）：
$ b $ ol
<
请注意，这些定律也适用于直觉逻辑。我们推导出的两个法则在下面的论文中被引用。
$ b $ h2简单类型
最简单的类型很容易与...合作。例如：
data T = Con Int |无
构造函数和访问器具有以下类型签名：
Con :: Int - > T
Nil :: T
unCon :: T - > Int
unCon（Con x）= x
类型构造函数
现在我们来处理类型构造函数。以下数据定义：
data T a = Con a |无
这会创建两个构造函数，
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
量化类型
让我们将存在量词∃添加到我们的原始类型（第一个，没有类型构造函数）。而不是将其引入类似于逻辑的类型定义中，而是将其引入构造函数/访问器定义中，这看起来像逻辑。我们将稍后修改数据定义以匹配。
而不是 Int ，我们现在将使用∃x。吨。这里， t 是某种类型的表达式。
Con :: （∃x。t） - > T
unCon :: T - > （∃x。t）
根据逻辑规则（上述第二条规则），我们可以将 Con 类型重写为：
Con ::∀x。 t - > T
当我们将存在量词移到外部时（prenex形式），它变成了一个通用量词。
因此以下理论上是等价的：
data T = Con（存在x。t）|无
数据T =全部x。 Con t |无
除
在非直觉逻辑中，允许从 unCon 的类型推导出以下内容：
unCon ::∃T - > t - 无效！
这是无效的原因是因为这种转换在直觉逻辑中是不允许的。因此，如果没有 exists 关键字，就不可能为 unCon 写入类型，并且不可能将类型签名在prenex形式。很难让类型检查器保证在这种情况下终止，这就是为什么Haskell不支持任意存在量词的原因。
来源
带类型推断的一类多态性，马克·P·琼斯，第24届ACM SIGPLAN-SIGACT关于编程语言原理的讨论会（网站）
The Haskell Wiki does a good job of explaining how to use existential types, but I don't quite grok the theory behind them.
Consider this example of an existential type:
data S = forall a. Show a => S a -- (1)
to define a type wrapper for things that we can convert to a String. The wiki mentions that what we really want to define is a type like
data S = S (exists a. Show a => a) -- (2)
i.e. a true "existential" type - loosely I think of this as saying "the data constructor S takes any type for which a Show instance exists and wraps it". In fact, you could probably write a GADT as follows:
data S where -- (3)
S :: Show a => a -> S
I haven't tried compiling that, but it seems as though it should work. To me, the GADT is obviously equivalent to the code (2) that we'd like to write.
However, it's completely not obvious to me why (1) is equivalent to (2). Why does moving the data constructor to the outside turn the forall into an exists?
The closest thing I can think of are De Morgan's Laws in logic, where interchanging the order of a negation and a quantifier turns existential quantifiers into universal quantifiers, and vice-versa:
¬(∀x. px) ⇔ ∃x. ¬(px)
but data constructors seem to be a totally different beast to the negation operator.
What is the theory that lies behind the ability to define existential types using forall instead of the non-existent exists?
First of all, take a look at the "Curry Howard correspondence" which states that the types in a computer program correspond to formulas in intuitionistic logic. Intuitionistic logic is just like the "regular" logic you learned in school but without the law of the excluded middle or double negation elimination:
Not an axiom: P ⇔ ¬¬P (but P ⇒ ¬¬P is fine)
Not an axiom: P ∨ ¬P
Laws of logic
You are on the right track with DeMorgan's laws, but first we are going to use them to derive some new ones. The relevant version of DeMorgan's laws are:
- ∀x. P(x) = ¬∃x. ¬P(x)
- ∃x. P(x) = ¬∀x. ¬P(x)
We can derive (∀x. P ⇒ Q(x)) = P ⇒ (∀x. Q(x)):
- (∀x. P ⇒ Q(x))
- (∀x. ¬P ∨ Q(x))
- ¬P ∨ (∀x. Q(x))
- P ⇒ (∀x. Q)
And (∀x. Q(x) ⇒ P) = (∃x. Q(x)) ⇒ P (this one is used below):
- (∀x. Q(x) ⇒ P)
- (∀x. ¬Q(x) ∨ P)
- (¬¬∀x. ¬Q(x)) ∨ P
- (¬∃x. Q(x)) ∨ P
- (∃x. Q(x)) ⇒ P
Note that these laws hold in intuitionistic logic as well. The two laws we derived are cited in the paper below.
Simple Types
The simplest types are easy to work with. For example:
data T = Con Int | Nil
The constructors and accessors have the following type signatures:
Con :: Int -> T
Nil :: T
unCon :: T -> Int
unCon (Con x) = x
Type Constructors
Now let's tackle type constructors. Take the following data definition:
data T a = Con a | Nil
This creates two constructors,
Con :: a -> T a
Nil :: T a
Of course, in Haskell, type variables are implicitly universally quantified, so these are really:
Con :: ∀a. a -> T a
Nil :: ∀a. T a
And the accessor is similarly easy:
unCon :: ∀a. T a -> a
unCon (Con x) = x
Quantified types
Let's add the existential quantifier, ∃, to our original type (the first one, without the type constructor). Rather than introducing it in the type definition, which doesn't look like logic, introduce it in the constructor / accessor definitions, which do look like logic. We'll fix the data definition later to match.
Instead of Int, we will now use ∃x. t. Here, t is some kind of type expression.
Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)
Based on the rules of logic (the second rule above), we can rewrite the type of Con to:
Con :: ∀x. t -> T
When we moved the existential quantifier to the outside (prenex form), it turned into a universal quantifier.
So the following are theoretically equivalent:
data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil
Except there is no syntax for exists in Haskell.
In non-intuitionistic logic, it is permissible to derive the following from the type of unCon:
unCon :: ∃ T -> t -- invalid!
The reason this is invalid is because such a transformation is not permitted in intuitionistic logic. So it is impossible to write the type for unCon without an exists keyword, and it is impossible to put the type signature in prenex form. It's hard to make a type checker guaranteed to terminate in such conditions, which is why Haskell doesn't support arbitrary existential quantifiers.
Sources
"First-class Polymorphism with Type Inference", Mark P. Jones, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (web)
这篇关于存在类型的理论基础是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
