LEAN 通过 类型类（Type Class）来提供的多态机制（Polymorphism）。

        以∅：Set α 为例，有 Set α 实现 class EmptyCollection。

        其中，class EmptyCollection 定义如下：

         也就是，符号  ∅ 或 {}，LEAN 编译器会转译成，EmptyCollection.emptyCollection。当对应的类型是 Set α，如 ∅：Set α，那么，因为 Set α 实现了 class EmptyCollection，因此，EmptyCollection.emptyCollection：Set α 会转换成，〈fun _ ↦ False〉：Set α。

        这是，LEAN 通过 类型类（Type Class）来提供的多态机制（Polymorphism）。当  Set α 实现了 class EmptyCollection，即上上图所示。其中，instance 关键字相当于 定义一个无名对象（anonymous object），记为 xxx，其类型为 EmptyCollection (Set α)，其包含了一个类型为Set α，值为〈fun _ ↦ False〉 的 成员 emptyCollection。并且，将该对象注册在一个类型类实例化表（Type class instance table）里，包含了，EmptyCollection 有多少个不同的实例信息。当遇到 EmptyCollection.emptyCollection：Set α 时，编译器，会发现，EmptyCollection 是一个 type class，并推断其类型参数α 为 Set α，因此，会去类型类实例化表寻找 类型为 EmptyCollection (Set α) 的实例，即，上面通过 instance 定义的无名对象，实际是有唯一名称的，只是没显示给用户看而已。找到那对象 xxx 后，会使用其 emptyCollection 成员，替代 EmptyCollection.emptyCollection，同时，其emptyCollection 成员的实现为 〈fun _ ↦ False〉，那么，就有，〈fun _ ↦ False〉：Set α。

        因此，可以看到 EmptyCollection.emptyCollection 的实际类型，如下：

        其中，[self: EmptyCollection α]，对于 ∅：Set α 来说，就是那无名对象 xxx: EmptyCollection (Set α)。

        相当于，

        fun EmptyCollection.emptyCollection.{u} {α: Type u} [self: EmptyCollection α]: α

        := self.emptyCollection

        这样就清楚这个，LEAN 通过 类型类（Type Class）来提供的多态机制（Polymorphism）了。