将
data DatumType a b = Datum a b
的定义翻译成英语大概是这样的:
创建一个名为
DatumType
的新类型构造器,和一个名为
Datum
的新数据构造器,使得对于所有类型
a
和
b
,将
Datum
应用于类型为
a
和
b
的值会得到一个类型为
DatumType a b
的值。
“我一直在想这个类型是
DatumType
还是隐式地
forall a. DatumType a b
。”
我认为理解的障碍在于术语“类型”可以有两种不同的含义,具体取决于上下文:
1. 一个
类型是指任何存在于类型级别的实体。
2. 一个
类型是指那些可以作为项的类型的类型级别实体;任何种类为
Type
(也称为
*
)的东西,而且只有这种东西。
这两个定义基本上是由于我们使用“类型的”这个短语来描述项级别和类型级别之间的关系而产生的——因此在“类型”的含义中包括不能参与该关系的事物似乎很奇怪。然而,在类型表达式中存在许多不能直接参与该关系的东西,我们希望在不必一直使用笨拙的短语(如“类型级别实体”)的情况下谈论它们。作为一个社区,我们似乎没有找到比仅在不同时间使用不同含义的“类型”更好的解决方案,并希望从上下文中清楚地表明。
因此,根据定义2,很明显
DatumType
不是一个类型;它需要应用于两个类型参数才能产生某些项级别的类型。如果我们这样考虑,我可以理解为什么你会倾向于认为数据声明定义的“类型”是
forall a b. DatumType a b
。
然而,我认为这可能是一种混乱的想法。单独看来,
forall a b. DatumType a b
是可以在所有形式为
DatumType _ _
的类型中使用的项的类型;这个类型中唯一的值是诸如
Datum undefined undefined
的东西。相反,
forall a b
通常会在你看到
DatumType a b
时更远一些;例如,数据构造器本身的类型(如果使用 GADT 语法定义,则会编写这个类型)可以写为
Datum :: forall a b. a -> b -> DatumType a b
。
因此,说“由数据声明定义的类型是forall a b. DatumType a b”非常奇怪。数据声明定义了一整个“族”类型,其中类型forall a b. DatumType a b只是一个极为局限(且相当无用)的示例。相反,我会说“对于所有类型a和b,数据声明定义了一个类型DatumType a b”;涉及的“for all”概念范围比您可以在单个类型表达式中使用的forall关键字更广泛,因此我将其移出正式类型表达式到英语描述中。
当然,如果我们专注于“类型”的定义1,则解释起来要简单得多。数据声明只是定义了一个具有kind * -> * -> *的类型DatumType。
这就引出了问题:哪种观点才是正确的?
也许令人不满意的是,在这两个观点之间没有什么有趣的东西。这两件事情都发生了:我们得到了一个新的类型构造函数DatumType,其kind为*->*->*,并且对于所有类型a和b,DatumType a b都是一些术语的类型。这就是kind为*->*->*的事物的意思。只有在你试图确定“特定类型”而没有意识到term type通常在这两个意义上使用时,才会出现困境,因此,如果你没有清楚地知道你正在使用哪种意义,你可能会被绊倒。
某些情况下说,那些没有kind *的东西不是类型,因此DatumType并不真正是一种类型。其他人则将DatumType称为类型。然而,这纯粹是我们选择使用的术语之间的差异;无论哪种方式,DatumType :: * -> * -> *都存在,并且在任何观点中都具有相同的功能。纠缠于特定类型级实体是否是类型的问题并不涉及事物如何实际运作,而只是英语语言用法的问题。
所以,回到您更具体的一些问题:
因此,这意味着像
[a]
这样的多态类型是TYPE(即*),该类型的完整名称为forall a. [a]。
换句话说,我想确认Haskell中的多态类型的类型声明总是以缩写形式出现,并且完整的类型名称始终带有隐式的
forall a. ....
。
正如我所提到的,我认为这不太正确。是的,类型级别上的
[]
需要一个参数才能产生术语类型;
[] :: * -> *
。因此,根据定义2,
[]
不是类型。但是,将完整列表类型称为“真正的”
forall a. [a]
并不完全正确,因为这是普遍多态列表的特定类型表达式(它只能是空列表的类型,或者是充满底部值的列表,或者是底部值)。特别地,
[True, False]
是
[Bool]
类型的成员,而不是
forall a. [a]
类型的成员。
相反,
[]
只是种类为
* -> *
的类型级别实体。无论您是否称其为类型,都取决于您。无论如何,它都不是任何术语的类型,而且无论如何,在类型表达式中使用它是有效的(前提是它们的种类检查通过)。
因此,在
data Mytype a
中,类型不是
Mytype
,也不仅仅是
Mytype a
,而是
forall a. Mytype a
,而
Mytype
是一个类型构造函数。
Mytype
确实是一种类型构造函数。 (无论使用哪个“类型”定义,即使我们愿意将所有类型级别实体都称为类型,“类型构造函数”仍然是一个特定的类别,因为是否为“类型构造函数”不能仅通过查看其种类来确定,就像您无法仅通过查看其类型来确定某个数据构造函数是什么一样)
Mytype a
本身是没有意义的,这是正确的;它必须在作用域内使用一个类型变量
a
。
并不是说
forall a. Mytype a
是“由
data Mytype a
定义的类型”正确的方式。对于
任何 类型
a
,
Mytype a
都是一种类型;
forall a. Mytype a
是一个
特定的 类型表达式,它并不包含我们可以用
Mytype
类型构造器形成的大部分类型。
因此,任何时候你想要使用
Mytype a
时都会有一个
forall
(无论是显式还是隐式) 。但通常它会比直接包围
Mytype a
更进一步,类似于
someFunc :: forall a. a -> Bool -> MyType a
。
OP在另一个答案中留下了一条评论,我认为回应这条评论会有所启发:
我想我会编辑这个问题,解释所有澄清问题的来源。就让我们说,在学习和实验类型类的过程中,我对 instance Eq (a,b)
感到困惑。为什么不是 instance Eq (,)
,答案不仅仅是因为需要在实现中引用类型变量。将类型定义为 data (,) a b = (,) a b
时,Eq
只能在适当的类型上定义, 而任何可能的二元组实际上都是一种类型,即一个多态类型。然后就有了问题,当我们写 data (,) a b = (,) a b
时,我们到底在定义什么?是 (,)
还是 forall a b. (a,b)
。
请记住,将类型作为
Eq
的一个实例意味着你可以比较该类型的值是否相等。
当你说
instance Eq (a, b)
时,它实际上意味着
instance forall a b. Eq (a, b)
;用英语来说,“对于所有类型
a
和
b
,类型
(a, b)
是类
Eq
的成员。这意味着你可以选择任何两种你喜欢的类型,将它们应用到
(,)
类型构造器中,得到的结果类型将是一些可以用来比较相等性的值。(当然,这并不是真的,我们实际使用的实例更像是
instance forall a b. (Eq a,Eq b) => Eq (a, b)
,因为我们需要
Eq a
和
Eq b
)。
(,)
构造器不适合成为Eq
类的成员,因为它在说“类型构造器(,)
是Eq
类的成员”,而“可以比较(,)
的值”的说法毫无意义,因为(,)
不是那种具有值的东西。
但是,(,)
仍然是一种存在的东西!并且它就是由data (,) a b = (,) a b
所定义的东西。它只是一个带有* -> * -> *
的类型,这种类型我们无法为其创建Eq
实例。短语“Eq
只能定义在适当的类型上”使用了 “类型” 的定义,其中只包括具有*
类型的东西,但请记住,“不是适当的类型”根据此定义并不意味着“不是真正的事物”,这只是我们选择(至少在那个特定的句子中)用一个狭义的含义来使用“类型”这个词。 Eq
类被定义为具有*
类型的成员,这就是全部。其他类可以定义具有不同类型的成员; 如果它们具有* -> * -> *
类型的成员,则(,)
本身可以是这些类的实例。例如,请查看Bifunctor
的示例列表。 Eq
实例必须是Eq(a,b)
而不是Eq (,)
,这一事实并不意味着(,)
不是在类型层次上存在的有效实体。