使用联合、交集和否定类型进行编程
Programming with union, intersection, and negation types
AI总结：
本文阐述了集合论类型（联合、交集、否定）在编程中的优势，通过语义子类型理论及其扩展，提出并实现了三种有效的语言系统限制，以精确支持分支、模式匹配和函数重载等语言构造的类型化。
摘要：
在这篇文章中，我展示了使用集合论类型（即包含联合、交集和否定类型连接符的类型）进行编程的优势，以及我敢说的其美妙之处。我通过几个例子展示了集合论类型如何成为对一些常见编程模式进行类型化的必要条件，以及它们如何在非常精确地对多种语言构造（从分支和模式匹配到函数重载和类型分支）进行类型化中发挥关键作用。我首先介绍了被称为语义子类型化的类型理论，并将其扩展以包含多态类型。接下来，我讨论了使用这些类型的语言设计。我首先定义了一个涵盖演示第一部分中给出的所有示例的理论框架。由于该框架的系统无法被有效实现，我随后描述了该系统的三个有效限制：(i) 具有显式类型函数的多态语言，(ii) à la Hindley-Milner 的隐式类型多态语言，以及 (iii) 一种单态语言，它通过实现经典的联合消除，精确地为函数重构交集类型，并实现了一种非常通用的出现类型形式。我以对这些语言其他方面的简短概述结束了演示，如模式匹配、渐进式类型和指称语义。
英文摘要：
In this essay, I present the advantages and, I dare say, the beauty of programming in a language with set-theoretic types, that is, types that include union, intersection, and negation type connectives. I show by several examples how set-theoretic types are necessary to type some common programming patterns, but also how they play a key role in typing several language constructs-from branching and pattern matching to function overloading and type-cases-very precisely. I start by presenting the theory of types known as semantic subtyping and extend it to include polymorphic types. Next, I discuss the design of languages that use these types. I start by defining a theoretical framework that covers all the examples given in the first part of the presentation. Since the system of the framework cannot be effectively implemented, I then describe three effective restrictions of this system: (i) a polymorphic language with explicitly-typed functions, (ii) an implicitly-typed polymorphic language à la Hindley-Milner, and (iii) a monomorphic language that, by implementing classic union-elimination, precisely reconstructs intersection types for functions and implements a very general form of occurrence typing. I conclude the presentation with a short overview of other aspects of these languages, such as pattern matching, gradual typing, and denotational semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
