术语：在 Thompson 的书中，Haskell 中“类型表达式”的精确定义是啥？

Posted 2023-02-27

【中文标题】术语：在 Thompson 的书中，Haskell 中“类型表达式”的精确定义是啥？

【英文标题】：Terminology: what is the precise definition of "type expression" in Haskell, as used in Thompson's book?术语：在 Thompson 的书中，Haskell 中“类型表达式”的精确定义是什么？

【发布时间】：2015-04-22 04:04:30

【问题描述】：

Thompson 的“Haskell - 函数式编程的工艺”一书中使用的术语“类型表达式”的精确定义是什么？书上好像没有定义这个词。

例如未在索引中列出。另外，我试图在书中寻找明确的定义，但一无所获。

相关问题：type variable 是 type expression 吗？

让我们考虑例如以下类型（表达式？）：

a->b

现在，如果我将a 替换为c，那么c->b 会成为a->b 的一个实例吗？

术语“类型表达”例如在第 314 页（本书第三版）中使用：

作为类型的集合，我们寻找由给出的集合的交集 (a, [Char]) 和 (Int, [b])。我们怎样才能得出一个描述 这个路口？在此之前，我们修改并介绍一些 术语。

回想一下，一个类型的实例是通过替换给出的 类型变量或类型表达式的变量。类型表达式 是两个类型表达式的公共实例，如果它是 每个表达式。

两个表达式的最普遍的例子 是一个公共实例 mgci，具有其他所有公共的属性 instance 是 mgci 的一个实例。

现在我们可以描述 由两个类型表达式给出的集合的交集。它被称为 两者的统一，这是最普遍的常见情况 两种类型的表达式。

【参考方案1】：

如果您想将类型视为“事物”，则可以谈论我们为描述它们而写的词，例如 Int 和 Cont (r -> a) (Maybe q) 之类的词作为描述这些事物的语言。数字 3 和 Haskell 代码片段 3 之间也有类似的区别。

与3 是表示数字3 的（值）表达式一样，Integer 是表示整数类型的类型表达式。

【讨论】：

感谢您的回答，所以从这个意义上说a 和b 是两个不同的多态类型表达式，但它们指的是相同的多态类型（即任何类型），对吗？

这个问题有点复杂。类型表达式a 和b 作为表达式当然不同，但实际上可能被解释为格式错误的（“开放”）表达式，因此不代表实际类型。你可能更喜欢写forall a . a 和forall b . b，它们现在是格式良好的类型表达式，它们都表示相同的类型。然而，现在还不清楚称它们为不同的表达式是否合适！你可以清楚地说它们有不同的书写形式，但由于我们通常只将表达式分类到 alpha 等价，我们可能无法区分它们。

另一种理解方式是从“书面表达式 -> 抽象绑定树 -> 类型”而不是直接的“书面表达式 -> 类型”。 ABT 中点很好，因为它是在计算机科学中做大量工作的好对象——您可以将 ABT 视为带有“绑定”和“变量”的良好概念注释的树。 ABT 具有“内置”的 alpha 等价性，例如仅在绑定变量的有效重命名上不同的两个 ABT 是相同的，因此无法区分 forall a . a 和 forall b . b 有更明确的原因。

感谢您的解释，现在我正在尝试找到一个示例，即两个表达式（或 ABT）不同但它们引用相同的类型。我读过 TAPL，什么是类型表达式，例如在简单类型的 lambda 演算或 System F（第 323 页，TAP）中？这些系统中有这样的东西吗？

STLC 类型表达式的 Haskell 类型是 data Type = Arr Type Type，或者更有趣的是，如果您有一些基本类型，则类似于 data Type = Arr Type Type | Star。 System F 用变量和绑定来增强这种类型语言，就像我上面讨论的那样。 Harper 的 PFPL 很好地讨论了 ABT 和类型语言，我建议您看看。