Geekly articles weekly

Arend-基于HoTT的依存类型语言（第1部分）

在这篇文章中，我们将讨论Arend依赖类型的新发布的JetBrains语言（该语言以Gating Rent命名）。 该语言是JetBrains Research在过去几年开发的。 尽管一年前的存储库已在github.com/JetBrains上公开提供，但Arend的完整版本仅在今年7月才发布。

我们将尝试说明Arend与基于依赖类型的形式化数学的现有系统有何不同，以及它的用户现在可以使用哪些功能。 我们假定本文的读者通常熟悉依赖类型，并且至少听说过基于依赖类型的一种语言：Agda，Idris，Coq或Lean。 但是，我们不希望读者拥有高级的依赖类型。

为了简单和具体，我们关于Arend和同伦类型的故事将在Arend上实现最简单的排序列表算法的实现-即使使用此示例，您也可以感受到Arend与Agda和Coq之间的区别。 关于Habré的文章已经有很多专门针对依赖类型。 让我们说说在Agda上使用QuickSort方法实现排序列表的方法。 我们将实现一种用于对插入物进行排序的简单算法。 在这种情况下，我们将专注于Arend语言的构造，而不是排序算法本身。

因此，Arend语言与其他具有依赖类型的语言之间的主要区别在于它所基于的逻辑理论。 Arend就这样使用了最近发现的V. Voevodsky同伦类型理论（ HoTT ）。 更具体地说，Arend基于HoTT的一种变体，称为“带间距类型理论”。 回想一下，Coq基于所谓的归纳构造演算（归纳构造演算），而Agda和Idris则基于类型的Martin-Löf内涵理论 。 Arend基于HoTT的事实极大地影响了其语法构造和类型检查算法（typcheker）的操作。 我们将在本文中讨论这些功能。

让我们尝试简要描述语言基础架构的状态。 对于Arend，有一个IntelliJ IDEA插件，可以直接从IDEA插件存储库中安装。 原则上，安装插件足以与Arend完全兼容，您仍然不需要下载并安装任何东西。 除了类型检查外，Arend插件还提供IDEA用户熟悉的功能：突出显示和对齐代码，各种重构和技巧。 也可以选择使用Arend的控制台版本。 有关安装过程的详细说明，请参见此处 。

本文中的代码示例基于Arend标准库，因此我们建议从资源库中下载其源代码。 下载后，必须使用“导入项目”命令将源目录作为IDEA项目导入。 在Arend，同伦类型理论和环理论的某些部分已经被形式化。 例如，在标准库中，有理数环Q的实现以及所有必需的环理论性质的证明。

公共语言中也提供了详细的语言文档 ，其中对本文中涉及的许多要点进行了详细说明。 您可以在电报频道中直接向Arend开发人员提问。

1. HoTT / Arend概述


同伦类型理论（或简称为HoTT）是一种类型的内涵类型理论，与经典的Martin-Löf类型理论（基于Agda的MLTT）和归纳构造演算（基于Coq的CIC）不同。语句和集合包含较高同伦水平的所谓类型。

在本文中，我们没有为自己设定详细解释HoTT基础的目的-为了对该理论进行详细说明，有必要重述整本书（请参阅本帖子 ）。 我们仅注意到，在某种意义上，基于HoTT公理的理论比经典的Martin-Löf类型理论更为优雅和有趣。 因此，在HoTT中证明了许多以前必须额外假设的公理（例如，功能可扩展性）。 此外，在HoTT中，可以内部定义多维同伦球，甚至可以计算它们的某些同伦群 。

但是，HoTT的这些方面主要是数学家感兴趣的，本文的目的是通过以将任何程序员实体都这么简单和熟悉的方式表示为有序列表的示例来说明基于HoTT的Arend如何与Agda / MLTT和Coq / CIC相比。 在阅读本文时，将HoTT视为一种具有更广泛的公理学的内涵类型理论就足够了，这为处理宇宙和平等提供了便利。

1.1依赖类型，咖喱-霍华德对应，宇宙


回想一下，具有依赖类型的语言与普通函数式编程语言的不同之处在于，除了常见的数据类型（例如列表或自然数）之外，还有一些类型取决于参数值。 这种类型的最简单示例是给定长度n的矢量或给定深度d的平衡树。 这种类型的其他一些例子在这里提到。

回想一下， Curry-Howard对应关系允许将逻辑语句解释为从属类型。 这种对应关系的主要思想是，空类型对应于错误语句，而填充类型对应于真实语句。 类型元素可以视为相应逻辑语句的证明。 例如，可以将任何元素（例如整数）视为证明存在整数（即，填充了整数的类型）这一事实的证明。

类型上的不同自然构造对应于不同的逻辑连接词：

  • 类型A×B的乘积有时称为对Pair A B的类型。由于仅当同时填充了类型A和B时才填充该类型，因此该构造对应于逻辑“和”。
  • 类型A + B的总和。在Haskell中，此类型称为E BB。由于仅当填充类型A或B中的一种时，才会填充此类型，因此此构造对应于逻辑“或”。
  • 功能类型A→B。 这种类型的任何函数都会将A的元素转换为B的元素。因此，当类型A的元素的存在暗示类型B的元素的存在时，该函数就存在。因此，此构造对应于含义。

现在假设给定了一个特定的类型A和一个由类型A的元素a参数化的类型B的族。让我们给出有关从属类型的更复杂构造的示例。

  • 从属函数类型 Π （a：A）（B a）。 如果B独立于A，则此类型与通常的功能类型A→B一致。类型Π （a：A）（B a）的函数将类型A的任何元素a转换为类型b a的元素。 因此，只有当a ：A中存在一个元素B a时，这种功能才存在。 因此，该构造对应于通用量词∀。 对于从属函数类型，Arend使用语法\Pi (x : A) -> B a ，并且可以使用lambda表达式\lam (a : A) => f a.构造此类型的术语\lam (a : A) => f a.
  • 相关对的类型为Σ （a：A）（B a）。 如果B独立于A，则此类型与A×B对的常规类型重合。当存在元素a：A和类型B a的元素时，将完全填充类型Σ （a：A）（B a）。 因此，该类型对应于存在量∃ 。 Arend中依赖对的类型由\Sigma (a : A) (B a) ，并且使用（依赖）对(a, b)的构造函数构造居住在依赖对中的术语。
  • 等式的类型为 a = a'，其中a和a'是某种类型A的两个元素。如果a和'相等，则填充此类型，否则为空。 显然，这种类型是逻辑上相等谓词的类似物。

在这一点上，我们为读者提供了参考资料，其中详细讨论了Curry-Howard的对应关系（例如，请参阅此处或此处 的讲座或文章课程 ）。

类型理论中考虑的所有表达式都必须具有某种类型。 由于在本理论的框架内还考虑了表示类型的表达式，因此还需要为其分配某种类型。 问题是，应该是哪种类型？

想到的第一个天真决定是为所有类型分配一个正式类型\Type ，称为Universe （之所以这样称呼是因为它通常包含所有类型）。 如果我们使用此Universe，则上述总和构造和类型乘积将收到签名\Type → \Type → \Type ，从属乘积和从属和的更复杂构造将获得签名Π (A : \Type) → ((A → \Type) → \Type) 。

此时，出现了一个问题， \Type宇宙本身应该具有哪种类型？ 天真地说宇宙\Type的定义是\Type本身会导致Girard悖论 ，因此代替单个Universe \Type考虑无限层次的宇宙 ，即。 嵌套的Universe链\Type 1 < \Type 2 < … ，其级别由自然数编号，Universe的\Type i （根据定义）是Universe \Type (i+1) 。 对于上述类型构造，还必须引入更复杂的签名 。

因此，需要类型理论中的Universe，以便任何表达式都具有特定类型。 在某些类型变体理论中，宇宙用于另一个目的：区分类型变体。 我们已经看到集合和语句是类型的特殊情况。 这表明在理论中引入一个单独的Prop宇宙用于语句，以及一个Set i宇宙的层次结构用于集合可能是有意义的。 这正是Coq系统所基于的归纳演算微积分中使用的方法。

1.2最简单的归纳类型和递归函数的示例


考虑Arend上最简单的归纳数据类型的定义：布尔类型，自然数类型和多态列表。 Arend使用\data关键字引入新的归纳类型。

\data Empty -- ,

\data Bool
| true
| false

\data Nat
| zero
| suc Nat

\data List (A : \Set)
| nil
| \infixr 5 :-: A (List A)

从上面的示例中可以看到，在\data关键字之后，您需要指定归纳类型的名称及其构造函数的列表。 同时，数据类型和构造函数可能具有一些参数。 假设在上面的示例中， List类型具有一个参数A nil list构造函数没有参数，而构造函数：-：有两个参数（其中一个为A类型，另一个为List A类型）。 Universe \Set由作为\Set的类型组成（集合的定义将在下一节中给出）。 \infixr允许您对构造函数使用前缀表示法：- \infixr并且还告诉Arend解析器运算符：-：是优先级为5的右关联运算。

在Arend中，所有关键字均以反斜杠字符（“ \”）开头，该实现受LaTeX启发。 请注意，Arend中的词汇规则非常宽松： Circle_HSpace, contrFibers=>Equiv, suc/=0, zro_*-left甚至n:Nat Circle_HSpace, contrFibers=>Equiv, suc/=0, zro_*-left所有这些文字都是Arend中有效标识符的示例。 最后一个示例显示Arend用户记住在标识符和冒号之间放置空格的重要性。 请注意，在Arend标识符中，不允许使用Unicode字符（尤其是您不能使用西里尔字母）。

Arend使用\func关键字定义函数。 这种构造的语法如下：在\func关键字之后，您需要指定函数的名称，其参数和返回值的类型。 定义函数的最后一个元素是它的主体。

如果可以显式指定要在其中计算给定函数的表达式，则为了指示函数的主体，可以使用标记=>。 考虑例如类型否定函数的定义。

 \func Not (A : \Type) : \Type => A -> Empty

函数的返回类型不一定总是必须明确指定。 在上面的示例中，Arend能够独立地推断出Not类型，并且我们可以在方括号之后省略表达式“： \Type ”。

与大多数形式化数学系统中一样，用户不必在\Type宇宙中指示明确的预测水平，并且在不明确指定预测水平的情况下使用宇宙的定义被认为是多态的 。

现在，让我们尝试定义一个计算列表长度的函数。 这种功能很容易通过模式匹配来识别。 Arend为此使用\elim关键字。 之后，您必须指定用于执行比较的变量（如果有多个这样的变量，则应该用逗号编写）。 如果对所有显式参数执行比较，则\elim和变量可以省略。 随后是一组比较点，以竖线“ |”彼此分隔。 此块中的每个项目都是«, » => «» 。

 \func length {A : \Set} (l : List A) : Nat | nil => 0 | :-: x xs => suc (length xs)

在上面的示例中， length函数的参数A被花括号包围。 Arend中的这些括号用于表示隐式参数，即 用户在调用函数或使用类型时可以忽略的参数。 请注意，在Arend中，当与模式匹配时，不能使用前缀表示法来指定构造函数，因此在示例示例中将使用前缀表示法。

与Coq / Agda中一样，在Arend中必须确保所有功能都已完成（即Arend中存在终止检查）。 在长度函数的定义中，此检查成功，因为递归调用严格减少了第一个显式参数。 如果没有发生这种减少，Arend将给出错误消息。

 \func bad : Nat => bad [ERROR] Termination check failed for function 'bad' In: bad

Arend允许循环依赖项和相互递归函数，还可以对它们执行完成检查。 此检查的算法是根据A. Abel的文章实现的。 在其中，您将找到相互递归函数必须满足的条件的更详细描述。

1.3集与语句有何不同？


我们之前曾写过，类型的例子是集合和语句。 此外，我们使用关键字\Type和\Set表示Arend中的Universe。 在本节中，我们将尝试更详细地说明语句在内涵类型理论（MLTT，CIC，HoTT）的变体方面与集合有何不同，同时解释Arend中关键字\Prop ， \Set和\Type的含义。

回想一下，在经典的马丁·洛夫理论中，没有将类型分为集合和陈述。 特别是，从理论上讲，只有一个累积的宇宙（在Agda中用Set表示，在Idris中用Type表示，在Lean中用Sort表示）。 这种方法是最简单的，但是在某些情况下会表现出其缺点。 假设我们正在尝试将“有序列表”类型实现为由列表及其排序证明组成的从属对。 事实证明，那么，在“纯” MLTT框架中，将不可能证明由相同元素组成的有序列表的相等性，在这种情况下，证据术语是不同的。 拥有这样的平等将是很自然和可取的，因此不可能证明它是MLTT的理论缺陷。

在Agda中，该问题借助所谓的非实质性注释得到了部分解决（请参阅参考资料，其中详细讨论了清单示例）。 但是，这些注释不是MLTT理论的构造，也不是关于类型的完整构造（不可能用未在函数参数中使用的类型注释进行标记）。

在CIC的基础上，基于CIC，有两个相互嵌套的不同Universe： Prop （语句的Universe）和Set （ Set的Universe），它们浸入到Type Universe的综合层次结构中。 Prop和Set之间的主要区别在于，对属于Coq中Prop类型的变量有很多限制。 例如，它们不能用于计算，并且仅在其他陈述的证据之内才能与样本进行比较。 另一方面，在不重要的证据公理下，属于Prop宇宙的所有类型的元素都相等，请参见Coq.Logic.ProofIrrelevance中的声明。 使用该公理，我们可以轻松证明上述有序列表的相等性。

最后，考虑对语句和Universe的Arend / HoTT方法。 主要区别在于HoTT放弃了无足轻重的证据的公理。 也就是说，HoTT中没有特殊的公理可以假定语句的所有元素都相等。 但是在HoTT中， 根据定义 ，如果可以证明其所有元素彼此相等，则该类型就是语句。 如果类型是语句，我们可以在类型上定义谓词：

 \func isProp (A : \Type) => \Pi (aa' : A) -> a = a'

随之而来的问题是：哪些类型满足该谓词，即语句？ 很容易验证对于空和单例类型是否正确。 对于至少包含两个不同元素的类型，这将不再成立。

当然，我们希望在语句上定义所有必要的逻辑连接词。 在1.1节中，我们已经讨论了如何使用类型理论构造来确定它们。 但是，存在以下问题：并非我们输入的所有操作都保留isProp属性。 类型和（从属）功能类型的乘积的构造保留此属性，而类型和从属对之和的构造则不保留。 因此，我们不能使用析取和存在量。

可以通过将新结构添加到HoTT中来解决此问题，即所谓的命题截断 。 这种设计使您可以将任何类型转换为语句。 可以将其视为正式操作，使居住在此类型的所有条件均等。 此操作有点类似于来自Agda的非重要性注释，但是，与它们不同的是，它是对具有签名\Type -> \Prop类型的完整操作。

语句的最后一个重要示例是某种类型的两个元素相等。 事实证明，在一般情况下，等式a = a'不必一定是语句。 它是其中一种的类型称为集合：

 \func isSet (A : \Type) => \Pi (aa' : A) -> isProp (a = a')

普通编程语言中找到的所有类型都满足该谓词，即，它们上的相等性是一个语句。 例如，对于自然数，整数，集合的乘积，集合的和，集合上的函数，集合的列表以及从集合构造的其他归纳数据类型，这是正确的。 这意味着，如果我们仅对这种熟悉的构造感兴趣，那么我们将无法考虑不满足该谓词的任意类型。 Coq中找到的所有类型都是set 。

如果要处理同伦类型理论，则非集合类型会很有用。 现在，我们仅向读者介绍标准库模块 ，该模块包含n维球体的定义，这是一个非集合类型的示例。

Arend具有特殊的Universe \Prop和\Set ，分别由语句和集合组成。 如果我们已经知道类型A包含在\Prop （或\Set ）Universe中，那么可以使用Path.inProp内置的Path.inProp公理来获得Arend中对应的isProp （或isSet ） isSet的证明（我们给出了使用此公理的示例）在2.3节中）。

 \func inProp {A : \Prop} : \Pi (aa' : A) -> a = a'

我们已经注意到，并非所有类型的自然构造都保留isProp属性。 例如，具有两个或多个构造函数的归纳数据类型永远无法满足它。 如上所述，我们可以使用命题截断构造将任何类型转换为语句。
在Arend库中，命题截断的标准实现称为Logic.TruncP 。 我们可以在Arend中将逻辑“或”定义为截断类型总和：

 \data \fixr 2 Or (AB : \Type) -- Sum of types; analogue of Coq's type "sum" | inl A | inr B \func \infixr 2 || (AB : \Type) => TruncP (sum AB) -- Logical “or”, analogue of Coq's type "\/"

在Arend中，还有另一种更简单，更方便的方法来定义命题截断的归纳类型。 为此，只需在定义数据类型之前添加\truncated关键字即可。 例如，Arend标准库中逻辑“或”的定义如下。

 \truncated \data \infixr 2 || (AB : \Type) : \Prop -- Logical “or”, analogue of Coq's type "\/" | byLeft A | byRight B

命题截断类型的进一步工作类似于Coq中分配给Prop宇宙的类型。 例如，仅在定义的表达式类型本身是语句的情况下才允许对类型为语句的变量进行模式匹配。 因此，定义函数Or-to-||总是很容易的 仅通过与示例进行比较，但具有与示例相反的功能，只有类型A `Or` B是语句（例如，当类型A和B都是语句并且互斥时，这种情况很少见）。

 \func Or-to-|| {AB : \Prop} (a-or-b : A `Or` B) : A || B | inl a => byLeft a | inr b => byRight

还记得Coq中的宇宙机制的特殊之处在于，如果将一些定义分配给Prop宇宙，那么就不可能在计算中使用它。 因此，Coq开发人员自己不建议使用命题构造，但建议尽可能使用集合中的类似物来代替它们。 Arend Universe的机制没有此缺点，也就是说，在某些情况下可以在计算中使用语句。 在讨论列表排序算法的实现时，我们将给出这种情况的示例。

1.4 Arend中的类


由于我们的目标是实现最简单的排序算法，因此熟悉Arend标准库中可用的有序集的实现似乎很有用。

在Arend中，类用于封装定义数学结构的运算和公理，并使用继承突出显示这些结构之间的关系。 类也是名称空间，在其中可以方便地放置含义合适的结构和理论。

继承Arend中的所有订单类的基类是BaseSet类，该BaseSet类除主机集的名称E （即BaseSet后代已在其上引入各种操作的集合）之外不包含其他任何成员。 考虑标准Arend库中此类的定义。

 \class BaseSet (E : \Set) -- ,

在上面的定义中，载体E声明为类参数。 可能会问，上面的BaseSet定义与下面的定义（其中将载波E定义为类字段）有区别吗？

 \class BaseSet' --      | E : \Set

一个稍微出乎意料的答案是，在Arend中，这两个定义之间没有区别 ，因为Arend中的任何类参数（甚至是隐式的）实际上都是其字段。 因此，对于这两种BaseSet实现，都可以使用表达式xE来访问字段E.上述BaseSet定义的变体之间仍然存在差异，但更为细微，我们将在下一节讨论类实例时对其进行更详细的研究（类实例）。

仅在列表中的对象类型上指定线性顺序时，对列表进行排序的操作才有意义，因此，我们首先考虑严格的部分有序集和线性有序集的定义。

 \class StrictPoset \extends BaseSet { | \infix 4 < : E -> E -> \Prop | <-irreflexive (x : E) : Not (x < x) | <-transitive (xyz : E) : x < y -> y < z -> x < z } \class LinearOrder \extends StrictPoset { | <-comparison (xyz : E) : x < z -> x < y || y < z | <-connectedness (xy : E) : Not (x < y) -> Not (y < x) -> x = y }

从类型理论的角度来看，可以将Arend中的类视为sigma类型的类似物，并且对投影和构造函数使用更方便的语法。 , Arend- -, .

, . , . , StrictPoset <-irreflexive <-transitive , E < — . , (, , ) , .

, , . , Arend , , . , . , , , , . :

 \class DecSet \extends BaseSet | decideEq (xy : E) : Dec (x = y)

Dec , Dec E , E , E , E .

 \data Dec (E : \Prop) | yes E | no (Not E)

, , Dec ( decidable) Order.LinearOrder . Dec , , , trichotomy , , E , <. , Dec Comparable Java.

 \class Dec \extends LinearOrder, DecSet { | trichotomy (xy : E) : (x = y) || (x < y) || (y < x) | <-comparison xyz x<z => {?} --   | <-connectedness xyx/<yy/<x => {?} | decideEq xy => {?} }

Dec Dec , , , , . Dec , .

, Dec ( ). Dec , Arend ( Dec LinearOrder, DecSet ), , (diamond inheritance).

: , ( , ).

Dec Order.LinearOrder IDEA ( [Ctrl]+[H]), , .



Arend ( IDEA BaseSet ). , .

1.5 , , .


StrictPoset Nat. Arend , . -, , , - ( ), .

: . .

 data \infix 4 < (ab : Nat) \with | zero, suc _ => zero<suc_ | suc a, suc b => suc<suc (a < b) \lemma irreflexivity (x : Nat) (p : x < x) : Empty | suc a, suc<suc a<a => irreflexivity a a<a \lemma transitivity (xyz : Nat) (p : x < y) (q : y < z) : x < z | zero, suc y', suc z', zero<suc_, suc<suc y'<z' => zero<suc_ | suc x', suc y', suc z', suc<suc x'<y', suc<suc y'<z' => suc<suc (transitivity x' y' z' x'<y' y'<z')

\func \lemma . , , , . , \lemma , \Prop .

x'<y' — -, x' < y' . - (.. , , ).

(instance) StrictPoset . Arend . \new . « ».

 \func NatOrder => \new StrictPoset { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

StrictPoset { … } \new : - StrictPoset . - , , , \new . \new C { … } C { … } . C, C. , , NatOrder StrictPoset .

, . , StrictPoset Nat StrictPoset { | E => Nat } . , NatOrder StrictPoset , ( ).

NatOrder \cowith ( - ).

 \func NatOrder : StrictPoset \cowith { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

, , \instance.

 \instance NatOrder : StrictPoset { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

Arend , Haskell. NatOrder \instance \cowith , StrictPoset ( ).

, BaseSet - E ( ), , E . .

, Arend . Arend , , ( , « » \classifying \field , Arend ). :

  • Arend . , X StrictPoset , List X List XE .
  • Arend .

, . , \instance StrictPoset , Nat Int ( NatOrder IntOrder ).

, x < y , x, y , , x, y . Arend , NatOrder.< , — IntOrder.< .

, . Arend , < StrictPoset , E. , Arend x<y StrictPoset ( ), E . , < .

, Arend. , \use \coerce . Arend — , , . - , \where .

. fromNat .

 \data Int | pos Nat | neg Nat \with { zero => pos zero } \where { \use \coerce fromNat (n : Nat) => pos n }

\use \coerce \func , . , , (, , ).

: HoTT JetBrains Research.

Source: https://habr.com/ru/post/zh-CN469569/

More articles:


All Articles