10. 类型类
如果一个操作可以用于多种类型，它就是多态的。 在 Lean 中，多态有三种变体：
-
宇宙多态，其中定义中的 Sort 可以用各种方式实例化，
-
接受类型作为（可能是隐式）参数的函数，允许单段代码可用于任何类型，以及
-
用类型类实现的 特设多态，其中被重载的操作对于不同类型可能有不同的实现。
因为 Lean 不允许对类型进行情况分析，所以多态函数实现了对任何类型参数选择都统一的操作；例如，List.map 不会仅仅因为输入列表包含的是 String 还是 Nat 就突然采取不同的计算方式。
当无法以“统一”的方式实现某个操作时，特设多态操作就非常有用；最典型的用例是重载算术运算符，使它们能用于 Nat、Int、Float，以及其他任何具有合理加法概念的类型。
特设多态也可能涉及多种类型；在一个集合的给定索引处查找值时，就涉及了集合类型、索引类型以及要提取的成员元素的类型。
类型类类型类最早在 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. 中描述。 描述了一组重载操作（称为 方法）以及它们所涉及的类型。
类型类非常灵活。 重载可能涉及多种类型；例如在数据结构中通过索引取值的操作，可以针对特定的数据结构、索引类型、元素类型甚至断言键存在于结构中的谓词进行重载。 得益于 Lean 富有表现力的类型系统，重载操作不仅限于类型；类型类可以通过普通值、类型族甚至谓词或命题进行参数化。 所有这些可能情况在实践中都有应用：
- 自然数字面量
OfNat类型类用于解释自然数字面量。 其实例不仅可能取决于被实例化的类型，还可能取决于数字面量本身。- 计算效应
像
Monad这样的类型类（其参数是一个从某个类型到另一个类型的函数）被用于为 具有副作用的程序提供特殊语法。 这里被重载操作的“类型”实际上是一个类型级函数，例如Option、IO或Except。- 谓词与命题
Decidable类型类允许 Lean 自动找到一个命题的判定过程。 这是termIfThenElse : term`if c then t else e` 是 `ite c t e`（即“如果—那么—否则”）的记法；它根据 `c` 是否为真返回 `t` 或 `e`。 显式参数 `c : Prop` 本身没有计算内容；另有一个由实例合成得到的 `[Decidable c]` 参数，真正决定如何把 `c` 求值为真或假。 写成 `if h : c then t else e` 时表示依赖式条件 `dite`，此时 `t` 和 `e` 可以使用 `c` 为真或假的事实。 标识符中的记法约定：建议将 `if c then t else e` 写作 `ite`，并分别用 `left`、`right` 指代 `t`、`e`。if-表达式的基础，使其可以基于任何可判定命题进行分支。
虽然普通的多态定义仅仅期望使用任意参数进行实例化，但被类型类重载的运算符要被 实例实例化，这些实例为某组特定参数定义了重载后的操作。 这些 实例隐式参数在方括号中指定。 在调用位置，Lean 要么从候选列表中 合成 一个合适的实例，要么报告错误。 由于实例本身也可能有实例参数，这个搜索过程可能是递归的，并产生一个将各种实例的代码组合在一起的最终复合实例值。 因此，类型类实例合成也是一种类型制导的程序构建手段。
以下是类型类的一些典型用例：
-
类型类可以表示重载运算符，比如可用于多种数值类型的算术运算符，或者可用于多种数据结构的成员判定谓词。对于给定类型，运算符通常有一个唯一的规范选择——毕竟对于
Nat的加法没有其他合理的替代定义——但这并非一个必然属性，库如果需要也可以提供替代实例。 -
类型类可以表示代数结构，提供该结构所需的额外结构及其公理。例如，表示阿贝尔群的类型类可能包含二元运算符、一元逆元运算符、单位元的方法，以及证明二元运算符具有结合律和交换律、单位元确实是单位元，以及逆元运算符在运算符两边都产生单位元的证明。在这里，可能没有规范的结构选择，库可能会提供许多实例化给定公理集合的方法；例如整数上就有两个同样规范的幺半群结构。
-
类型类可以表示两种类型之间的关系，允许它们在库中以某种新颖的方式一起使用。
Coe类表示自动插入的从一种类型到另一种类型的强制转换，MonadLift表示在期望另一种效应的上下文中运行带有某一种效应操作的方法。 -
类型类可以表示类型制导的代码生成框架，其中多态类型的实例各自贡献最终程序的一部分。
Repr类为一个类型定义了规范的美观打印器，而多态类型最终会有多态的Repr实例。 当美观打印最终在已知具体类型的表达式（如List (Nat × (String ⊕ Int))）上被调用时，产生的美观打印器将包含由List、Prod、Nat、Sum、String和Int的Repr实例组装而成的代码。