Chr*_*lor 66 haskell types type-systems existential-type quantifiers
该哈斯克尔维基做了解释如何使用存在类型的一个很好的工作,但我不太神交背后的理论.
考虑这个存在类型的例子:
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？
Die*_*Epp 55
首先,看看"Curry Howard对应",其中指出计算机程序中的类型对应于直觉逻辑中的公式.直觉逻辑就像你在学校学到的"常规"逻辑,但没有被排除的中间或双重否定消除的规律:
不是公理:P⇔¬¬P(但P⇒¬P很好)
不是公理:P∨¬P
你与DeMorgan的法律走在正确的轨道上,但首先我们将使用它们来推导一些新的法则.DeMorgan法律的相关版本是:
我们可以推导出(∀x.P⇒Q(x))=P⇒(∀x.Q(x)):
并且(∀x.Q(x)⇒P)=(∃x.Q(x))⇒P(下面使用这个):
请注意,这些法则也适用于直觉逻辑.我们得出的两个定律在下面的论文中引用.
最简单的类型易于使用.例如:
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
让我们将存在量词∃添加到我们的原始类型(第一个,没有类型构造函数).而不是在类型定义中引入它(看起来不像逻辑),而是在构造函数/访问器定义中引入它,它看起来像逻辑.我们稍后会修复数据定义以匹配.
而不是Int,我们现在将使用?x. t.这里t是某种类型表达式.
Con :: (?x. t) -> T
unCon :: T -> (?x. t)
根据逻辑规则(上面的第二条规则),我们可以重写以下类型Con:
Con :: ?x. t -> T
当我们将存在量词移到外面(prenex形式)时,它变成了一个通用的量词.
所以以下在理论上是等价的:
data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil
除了existsHaskell中没有语法.
在非直觉逻辑中,允许从以下类型推导出以下类型unCon:
unCon :: ? T -> t -- invalid!
这是无效的原因是因为在直觉逻辑中不允许这种转换.因此,如果unCon没有exists关键字,则无法编写类型,并且不可能将类型签名放在prenex格式中.很难使类型检查器保证在这种条件下终止,这就是Haskell不支持任意存在量词的原因.
"带类型推理的一流多态",Mark P. Jones,第24届ACM SIGPLAN-SIGACT会议论文集编程语言原理(网络)
Don*_*art 10
Plotkin和Mitchell在他们的着名论文中建立了存在类型的语义,它将编程语言中的抽象类型与逻辑中的存在类型联系起来,
Mitchell,John C.; Plotkin,Gordon D.; 摘要类型有存在类型,ACM事务编程语言和系统,卷.1988年7月10日第3号,第470-502页
在高层次上,
抽象数据类型声明出现在类型化的编程语言中,如Ada,Alphard,CLU和ML.这种声明形式将标识符列表绑定到具有相关操作的类型,复合"值"我们称之为数据代数.我们使用二阶类型lambda演算SOL来显示数据代数如何被赋予类型,作为参数传递,并作为函数调用的结果返回.在此过程中,我们讨论了抽象数据类型声明的语义,并回顾了类型化编程语言和构造逻辑之间的联系.
在你链接的haskell wiki文章中说明了这一点.我将从中借用一些代码和注释,并尝试解释.
data T = forall a. MkT a
这里有一个T带有类型构造函数的类型MkT :: forall a. a -> T,对吧？MkT是(大致)一个函数,因此对于每种可能的类型a,函数MkT都有类型a -> T.因此,我们同意通过使用该构造函数,我们可以构建类似于[MkT 1, MkT 'c', MkT "hello"]所有类型的值T.
foo (MkT x) = ... -- what is the type of x?
但是当你尝试提取(例如通过模式匹配)包含在一个T？中的值时会发生什么？它的类型注释只是说T,没有任何引用实际包含在其中的值的类型.我们只能就这样一个事实达成一致:无论它是什么,它都只有一种(而且只有一种); 我们如何在Haskell中陈述这一点？
x :: exists a. a
这只是说存在一个类型a,其x所属.在这一点上,应该清楚的是,通过删除forall afrom MkT的定义并通过显式指定包装值的类型(即exists a. a),我们能够实现相同的结果.
data T = MkT (exists a. a)
如果您在示例中添加实现的类型类的条件,那么底线也是相同的.