总结

类型类与结构体

在幕后，类型类由结构体表示。 定义一个类就是定义一个结构体，并额外创建一个空的实例表。 定义一个实例会创建一个值，该值要么具有该结构体作为其类型，要么是一个可以返回该结构体的函数，并另外在表中添加一个条目。 实例搜索包括通过查询实例表来构建一个实例。 结构体和类都可以为属性提供默认值（即方法的默认实现）。

结构体和继承

结构体可以继承自其他结构体。 在幕后，继承自另一个结构体的结构体将原始结构体的实例作为一个属性。 换句话说，继承是通过复合实现的。 当使用多重继承时，只有附加父结构体中的唯一属性会被使用以避免菱形问题，并且通常用来提取父值的函数则被组织起来构造一个函数。 记录点表示法会考虑结构体继承。

因为类型类只是应用了一些额外自动化的结构体，所以所有这些功能都可以在类型类中使用。 结合默认方法，这可以用来创建一个精细的接口层次结构，但不会给用户带来很大的负担，因为大型类所继承自的小型类可以自动实现。

应用函子

应用函子是具有两个附加操作的函子：

• pure，与 Monad 中的运算符相同
• seq，允许在函子中应用一个函数

虽然单子可以表示具有控制流的任意程序，但应用函子只能从左到右运行函数参数。 由于它们的功能较弱，因此它们对针对于接口所编写的程序提供的控制较少，而方法的实现者则有更大的自由度。 一些有用的类型可以实现 Applicative，但无法实现 Monad。

实际上，类型类 Functor、Applicative 和 Monad 形成了一个能力层级体系。 在这个层级体系中，从 Functor 向 Monad 逐级上升，可以编写更强大的程序，但实现更强大类的类型会更少。 多态程序应尽可能使用较弱的抽象，而数据类型应赋予尽可能强大的实例。 这样可以最大限度地提高代码的复用率。 更强大的类型类扩展自较弱的类型类，这意味着 Monad 的实现会免费提供 Functor 和 Applicative 的实现。

每个类都有一组需要实现的方法和一个相应的契约，该契约规定了这些方法的附加规则。 针对这些接口编写的程序期望遵循这些附加规则，否则可能会出现错误。 Functor 方法在 Applicative 的基础上的默认实现，以及 Applicative 方法在 Monad 的基础上实现 的默认实现，都将遵循这些规则。

宇宙

为了使 Lean 既能用作编程语言又能用作定理证明器，对该语言的一些限制是必要的。 这包括对递归函数的限制，以确保它们要么全部终止，要么被标记为 partial 并且返回的类型不是空类型。 此外，必须确保某些逻辑悖论不可能表示为类型。

排除某些悖论的限制之一是，每个类型都被分配到一个 宇宙。 宇宙是诸如 Prop、Type、Type 1、Type 2 等类型。 这些类型描述了其他类型——就像 0 和 17 是由 Nat 描述，Nat 本身是由 Type 描述，而 Type 是由 Type 1 描述。 以类型作为参数的函数的类型必须是比参数的宇宙更大的宇宙。

由于每个声明的数据类型都有一个宇宙，因此编写使用类型的数据等等的代码会变得非常麻烦，因为需要每个多态类型都用复制粘贴以接受 Type 1 的参数。 一种称为 宇宙多态 的特性允许 Lean 程序和数据类型将宇宙层级作为参数，就像普通的多态允许程序将类型作为参数一样。 通常来说，Lean 的库在实现多态操作的库时应使用宇宙多态性。