结构体和继承

为了理解 Functor、Applicative 和 Monad 的完整定义，另一个 Lean 的特性必不可少：结构体继承 (Structure Inheritance)。 结构体继承允许一种结构体类型提供另一种结构体类型的接口，并添加额外的属性。 这在对具有明确分类关系的概念进行建模时非常有用。 例如，以 神话生物 (Mythical Creature) 的模型为例。 其中有些很大型，有些很小型：

structure MythicalCreature where
  large : Bool
deriving Repr

在幕后，定义 MythicalCreature 结构体会创建一个具有名为 mk 的单一构造子的归纳类型：

#check MythicalCreature.mk

MythicalCreature.mk (large : Bool) : MythicalCreature

类似地，当一个函数 MythicalCreature.large 被创建，它实际上从构造子中提取了属性：

#check MythicalCreature.large

MythicalCreature.large (self : MythicalCreature) : Bool

在大多数古老的故事中，每个怪物都可以用某种方式被击败。 一只怪物 (Monster) 的描述应该包括以下信息，以及它是否庞大：

structure Monster extends MythicalCreature where
  vulnerability : String
deriving Repr

标题中的 extends MythicalCreature 表明每个 Monster 也都是 MythicalCreature。 要定义一个 Monster，其 MythicalCreature 的属性和 Monster 的属性应被同时提供。 巨魔 (Troll) 是一种对阳光敏感的大型怪物。

def troll : Monster where
  large := true
  vulnerability := "sunlight"

在幕后，继承是通过组合来实现的。构造子 Monster.mk 将 MythicalCreature 作为其参数：

#check Monster.mk

Monster.mk (toMythicalCreature : MythicalCreature) (vulnerability : String) : Monster

除了定义函数来提取每个新属性的值之外，一个类型为 Monster → MythicalCreature 的函数 Monster.toMythicalCreature 也被定义了。 其可以被用于提取底层的生物。

在 Lean 的继承层级体系中逐级上升与面向对象语言中的向上转型（Upcasting）并不相同。 向上转型运算符会使派生类的值被视为父类的实例，但该值会保留其原有的特性和结构体。 然而，在 Lean 中，在继承层级体系内逐级上升实际上会擦除原有的底层信息。 要查看此操作，请看 troll.toMythicalCreature 的求值结果：

#eval troll.toMythicalCreature

{ large := true }

只有 MythicalCreature 的属性被保留了。

如同 where 语法一样，使用属性名称的花括号表示法也适用于结构体继承：

def troll : Monster := {large := true, vulnerability := "sunlight"}

不过，委托给底层构造子的匿名尖括号表示法揭示了内部的细节：

def troll : Monster := ⟨true, "sunlight"⟩

application type mismatch
  Monster.mk true
argument
  true
has type
  Bool : Type
but is expected to have type
  MythicalCreature : Type

需要额外的一对尖括号，这将对 true 调用 MythicalCreature.mk：

def troll : Monster := ⟨⟨true⟩, "sunlight"⟩

Lean 的点表示法能够考虑继承。 换句话说，现有的 MythicalCreature.large 可以和 Monster 一起使用，并且 Lean 会在调用 MythicalCreature.large 之前自动插入对 Monster.toMythicalCreature 的调用。 不过，这仅在使用点表示法时发生，并且使用正常的函数调用语法来应用属性查找函数会致使一个类型错误的发生：

#eval MythicalCreature.large troll

application type mismatch
  troll.large
argument
  troll
has type
  Monster : Type
but is expected to have type
  MythicalCreature : Type

对于用户定义函数 (User-Defined Function)，点表示法还可以考虑其继承关系。 小型生物是指那些不大的生物：

def MythicalCreature.small (c : MythicalCreature) : Bool := !c.large

对于 troll.small 的求值结果是 false，而尝试对 MythicalCreature.small troll 求值则会产生以下结果：

application type mismatch
  MythicalCreature.small troll
argument
  troll
has type
  Monster : Type
but is expected to have type
  MythicalCreature : Type

多重继承

助手是一种神话生物，当给予适当的报酬时，它就可以提供帮助。

structure Helper extends MythicalCreature where
  assistance : String
  payment : String
deriving Repr

例如，nisse 是一种小精灵，众所周知，当给他提供美味的粥时，它就会帮忙打理家务。

def nisse : Helper where
  large := false
  assistance := "household tasks"
  payment := "porridge"

如果巨魔被驯化，它们便会成为出色的助手。 它们强壮到可以在一个晚上耕完整片田地，尽管它们需要模型山羊来让它们对自己的生活感到满意。 怪物助手是既是怪物又是助手。

structure MonstrousAssistant extends Monster, Helper where
deriving Repr

这种结构体类型的值必须由两个父结构体的所有属性进行填充：

def domesticatedTroll : MonstrousAssistant where
  large := false
  assistance := "heavy labor"
  payment := "toy goats"
  vulnerability := "sunlight"

这两种父结构体类型都扩展自 MythicalCreature。 如果多重继承被简单地实现，那么这可能会导致“菱形问题”，即在一个给定的 MonstrousAssistant 中，不清楚应该采用哪条路径来获取 large。 它应该从所包含的 Monster 还是 Helper 中去获取 large 呢？ 在 Lean 中，答案是采用第一条指定到祖先结构体的路径，并且其他父结构体的属性会被复制，而不是让新的结构体直接包含两个父结构体。

通过检验 MonstrousAssistant 的构造子的签名可以看到这一点。

#check MonstrousAssistant.mk

MonstrousAssistant.mk (toMonster : Monster) (assistance payment : String) : MonstrousAssistant

它接受一个 Monster 作为参数，以及 Helper 在 MythicalCreature 之上引入的两个属性。 类似地，虽然 MonstrousAssistant.toMonster 仅仅是从构造子中提取出 Monster，但 MonstrousAssistant.toHelper 并没有 Helper 可以提取。 #print 命令展现了其实现方式：

#print MonstrousAssistant.toHelper

@[reducible] def MonstrousAssistant.toHelper : MonstrousAssistant → Helper :=
fun self =>
  { toMythicalCreature := self.toMonster.toMythicalCreature, assistance := self.assistance, payment := self.payment }

此函数从 MonstrousAssistant 的属性中构造了一个 Helper。 @[reducible] 属性的作用与编写 abbrev 相同。

默认声明

当一个结构体继承自另一个结构体时，可以使用默认属性定义，即基于子结构体的属性去实例化父结构体的属性。 如果需要比生物是否庞大更具体的尺寸特征，则可以结合使用描述尺寸的专用数据类型和继承机制，以此产生一个结构体，其中 large 属性是根据 size 属性的内容计算得出的：

inductive Size where
  | small
  | medium
  | large
deriving BEq

structure SizedCreature extends MythicalCreature where
  size : Size
  large := size == Size.large

但是，这个默认定义只是一个默认定义。 与 C# 或 Scala 等语言中的属性继承不同，子结构体中的定义仅在没有提供 large 的具体值时才会使用，并且可能会出现无意义的结果：

def nonsenseCreature : SizedCreature where
  large := false
  size := .large

如果子结构体不应偏离父结构体，则有以下几种选择：

1. 记录其关系，如同 BEq 和 Hashable 所做的那样
2. 定义一个属性之间适当关联的命题，并设计 API 以在需要的地方要求提供命题为真的证据
3. 完全不使用继承

第二种选择可以如同这样：

abbrev SizesMatch (sc : SizedCreature) : Prop :=
  sc.large = (sc.size == Size.large)

请注意，单个等号用于表示等式 命题 ，而双等号用于表示一个检查相等性并返回 Bool 的函数。 SizesMatch 被定义为 abbrev，因为它应该在证明中自动展开，以使得 simp 能看到需要被证明的等式。

huldre 是一种中等体型的神话生物——实际上，它们与人类的体型相同。 huldre 上的两个大小属性是相互匹配的：

def huldre : SizedCreature where
  size := .medium

example : SizesMatch huldre := by
  simp

类型类继承

在幕后，类型类是结构体。 定义一个新的类型类会定义一个新的结构体，而定义一个实例会创建该结构体类型的一个值。 然后，它们被添加到 Lean 的内部表中，以便 Lean 可以根据请求找到实例。 这样做的结果是类型类能够继承其他类型类。

由于使用了完全相同的语言特性，类型类继承支持结构体继承的所有特性，包括多重继承、父类型方法的默认实现以及自动解决菱形继承问题。 这在许多情况下都很有用，就像 Java、C# 和 Kotlin 等语言中的多重接口继承。 通过精心设计类型类的继承层级体系，程序员可以兼得两方面的优势：一方面是得到一个可独立实现的抽象的精细集合，另一方面是从更大、更通用的抽象中自动构造出这些特定的抽象。