数学和编程语言中的类型与集合

几年来，我一直在设计和实施一种功能性教学语言，特别是在离散数学课程的背景下使用。这个想法是让学生在他们的计算机科学教育早期接触一些函数式和静态类型的编程，并为他们提供一种有趣而具体的方式来了解他们在离散数学课程中学到的概念与计算之间的联系。我不是第一个想到结合 FP + 离散数学的人，但我认为有机会使用专门为此目的而设计的语言来做得很好。 （而且，我在开玩笑，设计和实现一种语言只是很有趣。）当然，该语言有一个富有表现力的静态类型系统，具有自然数、有理数、布尔值和 Unicode 字符等基本类型，以及 sum 和产品类型、列表、字符串以及定义任意递归类型的能力。它还具有有限集的内置类型和语法。例如，（顺便说一句，我将使用 Unicode 语法，因为它看起来不错，但也有所有内容的 ASCII 等价物。）集合支持通常的操作，如并集、交集和差集，以及集合理解符号。这样做的目的是，这将为学生提供一个丰富的操场，让他们玩弄通常在离散数学课中教授的基本集合论。如果您习惯于使用静态类型语言进行编程，希望以上所有内容看起来都很正常。不幸的是，我怀疑这里有些东西会让学生感到非常困惑。我太习惯了，我花了很长时间才意识到哪里出了问题；也许你也没有意识到。 （好吧，也许我在博客文章的标题中泄露了它……）在数学课上，我们通常告诉学生这是一个集合。但在 Disco 中，ℕ 是一种类型，而 {1,2,3} 之类的东西是一个集合。如果你被告知这是一个集合，那么这种区别对你来说会显得非常奇怪和人为。例如，现在在 Disco 中，您可以询问 {1,2} 是否是 {1,2,3} 的子集：但是如果您尝试询问 {1,2} 是否是 ℕ 的子集，您会得到一个语法错误：Disco> {1,2} ⊆ ℕ1:10: |1 | {1,2} ⊆ ℕ | ^关键字“ℕ”不能用作标识符

现在，我们可以尝试各种方法来改进这个特定的例子——至少，让它更优雅地失败。但基本问题仍然存在：类型和集合之间的区别是什么，为什么它很重要？如果它不重要，我们应该摆脱它；如果它很重要，那么我需要能够向学生解释它！我们可以尝试完全摆脱这种区别，但这似乎会直接导致依赖类型系统和细化类型。细化类型非常酷，但我真的不想去那里（Disco 的类型系统已经足够复杂）。然而，我认为实际上有一个重要的区别；这篇博文是我第一次尝试明确我对区别的想法以及我计划如何向学生解释它。那么集合和类型有什么区别呢？口号是类型是内涵的，而集合是外延的。 （我实际上不会对我的学生使用这些词。） 那就是： 集合的特征在于关系：我们可以问哪些项目是集合的元素，哪些不是。另一方面，类型的特征在于类型的元素是如何构建的：我们可以以特定于类型的某些方式构造类型的元素（并解构它们）。这看起来有点对称，但事实并非如此。如果您一开始甚至不知道如何制作或谈论任何事物，您就不能问事物是否是集合的元素。所以类型先于集合：类型提供了一个以有序方式构建的值域，我们可以使用它；只有这样我们才能开始挑选某些值将它们放在一个集合中。

当然，这一切都以某种类型论为基础。当然，我知道人们可以将公理集合论作为基础，从空集建立一切。但是我正在构建一种类型化的函数式编程语言，所以我当然以类型理论为基础！然而，更重要的是，这几乎是每个在职数学家在实践中所做的。没有人真正根据公理集合论工作或思考（除了集合论者）。即使在典型的数学课上，有些集合也很特别。在我们谈论集合之前，我们必须先介绍特殊集合，以便我们知道什么是，什么是什么。在讨论集合之前，我们必须先介绍集合上的特殊笛卡尔积运算，以便我们知道元组是什么。等等。我们可以将类型视为一种语言，用于描述这种先验类的特殊集合。那么我到底要对我的学生说些什么呢？首先，在介绍语言时，我会告诉他们各种内置的原始类型，例如自然数、有理数、布尔值和字符。我不会对此有什么大不了的，而且我认为我不需要：在大多数情况下，他们已经看到了像 Python 或 Java 这样的具有原始值类型的语言。然而，当我们开始谈论集合时（通常是在从命题逻辑开始之后的第二单元），我们将集合定义为值的集合，我将明确指出与类型的相似性。我会告诉他们类型是特殊的内置集合，带有构建元素的规则。我们将继续讨论不相交联合和笛卡尔积，并练习构建和和积类型的元素。 （当我们稍后讨论递归时，他们将因此拥有开始构建递归类型（例如列表和树）所需的工具。）另外要提到的将是当我们编写集合类型时的方式，例如，集合ℕ，我们必须写下元素的类型——换句话说，是宇宙，或者从中选择元素的环境集。在介绍集合论时，传统上只有在谈到集合补运算时才提到宇宙集合；但事实是，数学家在描述给定集合时总是会想到一些宇宙。现在，回到 {1,2} ⊆ ℕ 的例子，如果这是一个语法错误，学生们仍然会感到困惑，我对如何使它起作用有一些想法。简而言之，这个想法是允许在表达式中使用类型（但不能反过来！），使用 T : Set T。如果我告诉他们类型是特殊的集合，那么从逻辑上讲，他们会期望能够使用它们像这样！然而，这是一个极其重要的变化：这意味着 Disco 现在能够表示无限集合，需要通过深度嵌入在内部表示集合，而不是简单地存储它们的元素（就像目前的情况）。例如， 2 ∈ (ℕ \ {3,5}) 应该评估为真，但我们显然不能仅仅枚举 ℕ \ {3,5} 的所有元素，因为有无穷多个。也许在以后的帖子中会详细介绍这个！此条目发布在项目、教学和标记基础、语言、数学、教学法、编程、集合、类型中。为永久链接添加书签。