Haskell中的多态类型的真实类型是隐式全称量化的类型吗？

Question

Haskell中的多态类型的真实类型是隐式全称量化的类型吗？

haskell

3

我正在努力澄清一些 Haskell 概念。当通过数据声明定义类型时，例如：

data DatumType a b = Datum a b

我一直在想这个类型是 DatumType 还是隐式的 forall a. DatumType a b。

因为实际上使用 ExplicitForAll 可以将其重写成 DatumType :: forall a b. a -> b -> DatumType a b。

λ> :set -XExplicitForAll
λ> :k forall a. Maybe a
forall a. Maybe a :: *

λ> :k forall a b . DatumType a b
forall a b . DatumType a b :: *

λ> :k DatumType
DatumType :: * -> * -> *

我们可以看到，类型forall a b. DatumType a b是一个合适的类型，即*。

然而，DatumType本身只是一个类型构造器。

因此，这意味着像[a]这样的多态类型是TYPE（即*），并且完整的类型名称是forall a. [a]。

换句话说，我的目的是确认Haskell中的多态类型声明总是以简写形式存在，并且完整的类型名称始终带有隐含的forall a. ...。

也就是说，在data Mytype a中，类型不是Mytype，也不仅仅是Mytype a，而是forall a. Mytype a，而Mytype是一个类型构造器。

这种解释正确吗？

编辑1（根据@Daniel Wagner答案）

我想我会编辑问题，解释所以澄清的来源。简言之，当学习和实验型类时，我对instance Eq(a, b)感到困惑。为什么不是instance Eq(,)，答案不仅仅是因为在实现中需要引用类型变量。Eq只能定义在合适的类型上，任何可能的对都是一个类型，一个多态类型。然后出现了一个问题，当我们编写data (,) a b = (,) ab时，我们定义的是(,)还是forall a b.(a，b)。

编辑2（根据@Ben答案）

推动我的形式化与上述：set -XExplicitForAll实验一起进行的材料之一是来自此处的以下声明 Haskell简介，版本98-2 值、类型和其他好东西

Haskell还包括多态类型——在某种程度上对所有类型进行全称量化的类型。多态类型表达式本质上描述了类型族。例如，（forall a）[a]是一个由类型a的所有类型组成的类型族，此类型族由列表类型a的类型组成。整数列表（例如[1,2,3]），字符列表（['a'，'b'，'c']），甚至是整数列表的列表等都是这个类型族的成员。

- MaatDeamon

1

嗨Maat。我已经为您修复了多次这个拼写错误。当您说“trough”时，您的意思是“through”。槽是一种长而开放的容器，通常用于给农场动物提供食物。 - halfer

2个回答

3

The declaration

data DatumType a b = Datum a b

声明一个新类型，DatumType，其种类为 * -> * -> *。还声明了一个新术语，Datum，其类型为 forall a b. a -> b -> DatumType a b。

在正常情况下，类型签名隐含地普遍量化其顶层提到的所有类型变量。但是数据声明不是类型签名，因此你问题中的某些部分没有意义。

还可以通过打开扩展来使类型变量成为单态的，而不是普遍量化的。例如：

{-# LANGUAGE ScopedTypeVariables #-}

foo :: forall a. Monoid a => a -> a
foo x = mconcat xs where
    xs :: [a]
    xs = [x, mempty, x]

在这段代码片段中，所有的量词都已被明确指定。在 where 块内，xs 的单态类型为 [a]，其中 a 是由一个包含类型范围约束的封闭作用域绑定的类型变量。如果插入额外的量词，该代码将无法编译。

foo :: forall a. Monoid a => a -> a
foo x = mconcat xs where
    xs :: forall a. [a]
    xs = [x, mempty, x]
    -- type error: can't match type a and type a0, whoops

希望这些信息能使你的每个语句的真实状态更加清晰，但让我们一次解决一个问题：

我一直在想类型是 DatumType 还是隐式的 forall a. DatumType a b。

无法回答。哪个类型？ DatumType 和 forall a. DatumType a b 都是合法的类型级表达式。

这意味着类似 [a] 的多态类型是 TYPE ，并且类型的全名为 forall a. [a]。

有时候。量词的插入不是一个局部过程，而是整个类型签名全局性的操作。它们被隐含地向上移动到顶层。因此，这是两种不同的类型：

-- these are all the same with ScopedTypeVariables off
forall a. [a] -> ()
forall a. ([a] -> ())
[a] -> ()

-- this is a different type from the ones above
(forall a. [a]) -> ()

因此，如果在正常的未扩展的 Haskell 中，你写了类型签名 x :: [a]，那么 [a] 确实是 forall a. [a] 的简写；但如果你写了签名 f :: [a] -> ()，那么 [a] 就不是 forall a. [a] 的简写，因为 forall 必须从参数到箭头浮动，才能覆盖整个类型。

换句话说，我想确认 Haskell 中的多态类型的类型声明总是以缩写形式存在，并且完整的类型名称始终带有隐含的 forall a. ...。

是的。

也就是说，在 data Mytype a 中，类型不是 Mytype 或者仅仅是 Mytype a，而是 forall a. Mytype a，...

种类错误。 data Mytype a 不是类型签名，因此没有 the type。如果我要从这样的声明中挑选一个类型来称之为 "the type"，那么它将是单独的 Mytype，因为这是该声明创建的唯一类型。

...而 Mytype 是一个类型构造器。

是的。

- Daniel Wagner

如果数据定义包括类型及其值的定义，则该类型必须是适当的类型，而我所看到的唯一适当的类型是多态类型，它是具体的，更高级别的类型不能具有值。 - MaatDeamon

在这里发现了一个有趣的帖子，主题是 https://dev59.com/JVMI5IYBdhLWcg3wFndC - MaatDeamon

@MaatDeamon 我在我的答案中进行了一些编辑，以回应您在最后一条评论中提到的内容。看看它是否有帮助！ - Ben

1

@MaatDeamon 我相信我已经直接回答了这个问题，对吧？你正在定义 (,)。（引用我的回答：“声明 data DatumType a b = Datum a b 声明了一个新类型，DatumType。DatumType 本质上只是另一种拼写方式 (,)。”） - Daniel Wagner

1

@MaatDeamon 听起来像是一份相当惊人的阅读列表！我很高兴你找到了帮助你达成目标的资源。 - Daniel Wagner

显示剩余9条评论

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Ben · Accepted Answer

将 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 (,)，这一事实并不意味着(,)不是在类型层次上存在的有效实体。