10. Type 类别🔗

如果一个操作可以与多种类型一起使用，那么它就是多态。在 Lean 中，多态性分为三种：

宇宙多态性，其中定义中的排序可以通过各种方式实例化，
将类型作为（可能是隐式的）参数的函数，允许单个代码体处理任何类型，以及
ad-hoc多态性，用类型类实现，其中要重载的操作对于不同类型可能有不同的实现。

由于 Lean 不允许对类型进行大小写分析，因此多态函数实现的操作对于任何类型参数的选择都是统一的；例如，List.map 不会根据输入列表是否包含 String 或 Nat 突然进行不同的计算。当没有“统一”的方法来实现操作时，临时多态操作非常有用；规范用例是重载算术运算符，以便它们与 Nat、Int、Float 以及具有合理加法概念的任何其他类型一起使用。 Ad-hoc多态性也可能涉及多种类型；在集合中查找给定索引处的值涉及集合类型、索引类型以及要提取的成员元素的类型。 type classType 类首先在 Philip Wadler and Stephen Blott, 1980. “How to make ad-hoc polymorphism less ad hoc”. In Proceedings of the 16th Symposium on Principles of Programming Languages. 中描述，描述了重载操作的集合（称为 methods）以及所涉及的类型。

Type 类非常灵活。重载可能涉及多种类型；对于数据结构、索引类型、元素类型甚至断言结构中键存在的谓词的特定选择，可以重载诸如对数据结构进行索引之类的操作。由于Lean的表达类型系统，重载操作不仅限于类型；类型类可以通过普通值、类型族、甚至谓词或命题来参数化。所有这些可能性都在实践中使用：

自然数文字: OfNat 类型类用于解释自然数文字。实例可能不仅取决于被实例化的类型，还取决于数字文字本身。
计算效果: Type类，例如Monad，其参数是从一种类型到另一种类型的函数，用于提供具有副作用的程序的特殊语法。重载操作的“类型”实际上是类型级函数，例如 Option、IO 或 Except。
谓词和命题: Decidable 类型类允许 Lean 自动找到命题的决策过程。这用作 termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false.if 表达式的基础，该表达式可以在任何可判定的命题上分支。

虽然普通的多态定义只是期望使用任意参数进行实例化，但使用类型类重载的运算符将使用 instances 进行实例化，instances 定义某些特定参数集的重载操作。这些 instance-implicit 参数在方括号中指示。在调用站点，Lean 或者 synthesizes 来自可用候选的合适实例，或者发出错误信号。因为实例本身可能具有实例参数，所以该搜索过程可以是递归的并且产生组合来自各种实例的代码的最终复合实例值。因此，类型类实例合成也是以类型导向的方式构造程序的一种手段。

以下是类型类的一些典型用例：

Type 类可以表示重载运算符，例如可与各种类型的数字一起使用的算术或可用于各种数据结构的成员谓词。对于给定类型，通常有一个规范的运算符选择——毕竟，Nat 没有合理的加法替代定义——但这不是一个基本属性，如果需要，库可以提供替代实例。
Type 类可以表示代数结构，提供额外的结构和结构所需的公理。例如，表示阿贝尔群的类型类可能包含二元运算符、一元逆运算符、单位元素的方法，以及证明二元运算符是结合性和交换性的、单位是单位以及逆运算符在运算符两侧产生单位元素的证明。这里，可能没有规范的结构选择，并且库可以提供多种方法来实例化给定的一组公理；整数上有两个同样规范的幺半群结构。
类型类可以表示两种类型之间的关系，允许库以某种新颖的方式一起使用它们。 Coe 类表示自动插入从一种类型到另一种类型的强制转换，MonadLift 表示一种在需要另一种效果的上下文中运行具有一种效果的操作的方法。
Type 类可以表示类型驱动代码生成的框架，其中多态类型的实例各自贡献最终程序的一部分。 Repr 类定义了类型的规范漂亮打印机，多态类型最终得到多态 Repr 实例。当最终在具有已知具体类型的表达式（例如 List (Nat × (String ⊕ Int))）上调用漂亮打印时，生成的漂亮打印机包含从 List、Prod、Nat、Sum、String 的 Repr 实例组装的代码，以及Int。