kee*_*gan 19
标题和标签应该充分解释这个问题.
呃,不是真的.您使用了标记existential-type,但您提供的类型都不存在.
这里已经有了一些很好的答案,所以我会采取不同的方法并且更加正式.多态值本质上是类型上的函数,但Haskell的语法使得类型抽象和类型应用都隐含,这掩盖了问题.我们将使用System F的符号,它具有显式类型抽象和类型应用程序.
例如,map将编写熟悉的函数
map :: ?a. ?b. (a ? b) ? [a] ? [b]
map = ?a. ?b. ?(f :: a ? b). ?(xs :: [a]). case xs of
[] ? []
(y:ys) ? f y : map @a @b f ys
map现在是四个参数的函数:两种类型(a和b),一个函数和一个列表.我们使用Λ(大写lambda)在类型上编写函数,并且像往常一样使用λ函数.包含Λ的项产生包含∀的类型,就像包含λ的项一样,产生包含→的类型.我使用符号@a(如在GHC Core中)来表示类型参数的应用.
因此,多态类型的值就像从类型到值的函数.多态函数的调用者可以选择一个类型参数,该函数必须符合.
那么,我们如何编写一个类型的术语?a. [a]？我们知道包含∀的类型来自包含Λ的术语:
term1 :: ?a. [a]
term1 = ?a. ?
在标记的身体内,?我们必须提供类型的术语[a].也就是说,类型的术语?a. [a]意味着"给定任何类型a,我会给你一个类型列表[a]".
但是,我们一无所知a,因为它是从外部传递的论据.所以我们可以返回一个空列表
term1 = ?a. []
或未定义的值
term1 = ?a. undefined
或仅包含未定义值的列表
term1 = ?a. [undefined, undefined]
但没有其他的.
怎么样[?a. a]呢？如果∀表示类型的函数,则[?a. a]是函数列表.我们可以尽可能少地提供:
term2 :: [?a. a]
term2 = []
或者尽可能多:
term2 = [f, g, h]
但什么是我们的选择f,g和h？
f :: ?a. a
f = ?a. ?
现在我们真的被困了.我们必须提供类型的值a,但我们对类型一无所知a.所以我们唯一的选择是
f = ?a. undefined
所以我们的选择term2看起来像
term2 :: [?a. a]
term2 = []
term2 = [?a. undefined]
term2 = [?a. undefined, ?a. undefined]
等等,让我们不要忘记
term2 = undefined
通用(∀)类型的值是从类型到值的函数.存在(∃)类型的值是一对类型和值.
更具体地说:类型的值
?x. T
是一对
(S, v)
其中S是一个类型,并且其中v :: T,假设你的类型变量绑定x到S内T.
这是一个存在类型签名和一些类型的术语:
term3 :: ?a. a
term3 = (Int, 3)
term3 = (Char, 'x')
term3 = (?a. a ? Int, ?a. ?(x::a). 4)
换句话说,?a. a只要我们将该值与其类型配对,我们就可以将任何我们喜欢的值放入其中.
类型值的用户处于?a. a有利位置; 他们可以使用类型应用程序选择他们喜欢的任何特定类型@T,以获得类型的术语T.类型值的生产者?a. a处于一个糟糕的位置:他们必须准备好生产任何要求的类型,因此(如上一节所述)唯一的选择是?a. undefined.
类型值的用户?a. a处于可怕的位置; 里面的值是某种未知的特定类型,而不是灵活的多态值.类型价值的生产者处于?a. a有利地位; 正如我们上面所看到的那样,他们可以将他们喜欢的任何价值都粘在一对
那么什么是一个不那么无用的存在主义？如何将值与二元运算配对:
type Something = ?a. (a, a ? a ? a, a ? String)
term4_a, term4_b :: Something
term4_a = (Int, (1, (+) @Int , show @Int))
term4_b = (String, ("foo", (++) @Char, ?(x::String). x))
使用它:
triple :: Something ? String
triple = ?(a, (x :: a, f :: a?a?a, out :: a?String)).
out (f (f x x) x)
结果:
triple term4_a ? "3"
triple term4_b ? "foofoofoo"
我们打包了一种类型和一些类型的操作.用户可以应用我们的操作但不能检查具体值 - 我们不能在x内部进行模式匹配triple,因为它的类型(因此构造函数集)是未知的.这有点像面向对象的编程.
使用∃和类型 - 值对的存在性的直接语法将非常方便. UHC部分支持这种直接语法.但GHC没有.要在GHC中引入存在性,我们需要定义新的"包装"类型.
翻译上面的例子:
{-# LANGUAGE ExistentialQuantification #-}
data Something = forall a. MkThing a (a -> a -> a) (a -> String)
term_a, term_b :: Something
term_a = MkThing 1 (+) show
term_b = MkThing "foo" (++) id
triple :: Something -> String
triple (MkThing x f out) =
out (f (f x x) x)
我们的理论处理有两点不同.类型应用程序,类型抽象和类型对再次是隐式的.此外,包装器混淆写forall而不是exists.这引用了我们声明一个存在类型的事实,但数据构造函数具有通用类型:
MkThing :: forall a. a -> (a -> a -> a) -> (a -> String) -> Something
通常,我们使用存在量化来"捕获"类型类约束.我们可以在这里做类似的事情:
data SomeMonoid = forall a. (Monoid a, Show a) => MkMonoid a
有关该理论的介绍,我强烈推荐Pierce的类型和编程语言.有关GHC中存在类型的讨论,请参阅GHC手册和Haskell维基.
该类型forall a. [a]意味着对于任何单一类型,它都是包含该类型的列表.这也是简单的[a]意思,也就是[]空列表数据构造函数的类型.
类型[forall a. a]意味着您有一个具有多态类型的值列表,也就是说,每个值都是任何可能类型的值,不一定与列表中的其他元素相同.没有可能的值可以具有类型forall a. a,因此这也必须是空列表.
不同的是,虽然第一个可以用作任何类型的列表(根据定义,基本上),后者不能用作任何具体类型的列表,因为没有办法固定它到任何一种类型.
为了解决标记 - 存在类型是在某个范围内将被实例化为某种未知的具体类型的类型.它可以是任何东西,所以用forall a. a上面的东西来表示.为了确保具有存在类型的任何内容仅在实际类型可用的范围内使用,编译器会阻止存在类型"转义".
将forall量词视为lambda表达式可能有所帮助- 它引入了一个新的类型变量并在某个范围内绑定了该标识符.在该范围之外,标识符没有意义,这就是为什么forall a. a没有用处.