5.1. 结构与继承
为了理解 Functor、Applicative 和 Monad 的完整定义，还需要另一个 Lean 特性：结构继承。
结构继承允许一种结构类型提供另一种结构的接口，并附带额外字段。
当对具有清晰分类关系的概念建模时，这可能很有用。
例如，考虑一个神话生物模型。
其中有些体型大，有些体型小：
structure MythicalCreature where
large : Bool
deriving Repr
在幕后，定义 MythicalCreature 结构会创建一个归纳类型，它带有一个名为 mk 的单一构造子：
#check MythicalCreature.mk
类似地，会创建一个函数 MythicalCreature.large，它实际从构造子中提取该字段：
#check MythicalCreature.large在大多数古老故事中，每个怪物都能以某种方式被击败。 对一个怪物的描述应当包括这一信息，以及它是否巨大：
structure Monster extends MythicalCreature where
vulnerability : String
deriving Repr
标题中的 extends MythicalCreature 表明每个怪物也是神话中的存在。
要定义一个 Monster，应同时提供来自 MythicalCreature 的字段和来自 Monster 的字段。
巨魔是一种大型怪物，且易受阳光伤害：
def troll : Monster where
large := true
vulnerability := "sunlight"
在幕后，继承是用组合实现的。
构造子 Monster.mk 接受一个 MythicalCreature 作为其参数：
#check Monster.mk
除了定义用于提取每个新字段的值的函数之外，还定义了一个类型为 Monster → MythicalCreature 的函数 Monster.toMythicalCreature。
这可用于提取底层的生物。
在 Lean 中沿继承层级向上移动，并不等同于面向对象语言中的向上转型。
向上转型运算符会使来自派生类的值被当作父类的一个实例来处理，但该值保留其身份和结构。
然而，在 Lean 中，沿继承层级向上移动实际上会擦除底层信息。
要观察这一点的实际效果，请考虑对 troll.toMythicalCreature 求值的结果：
#eval troll.toMythicalCreature
只保留 MythicalCreature 的字段。
正如 where 语法一样，带有字段名的花括号记法也适用于结构继承：
def troll : Monster := {large := true, vulnerability := "sunlight"}然而，委托给底层构造子的匿名尖括号记法会暴露内部细节：
def troll : Monster := ⟨true, "sunlight"⟩
需要额外的一组尖括号，这会在 true 上调用 MythicalCreature.mk：
def troll : Monster := ⟨⟨true⟩, "sunlight"⟩
Lean 的点记法能够将继承纳入考虑。
换言之，已有的 MythicalCreature.large 可以与 Monster 一起使用，并且 Lean 会在调用 MythicalCreature.large 之前自动插入对 Monster.toMythicalCreature 的调用。
然而，这只在使用点记法时发生；若使用普通函数调用语法来应用字段查找函数，则会导致类型错误：
#eval MythicalCreature.large troll点记法也可以在用户定义函数中考虑继承。 小型生物就是非大型的生物：
def MythicalCreature.small (c : MythicalCreature) : Bool := !c.large
对 troll.small 求值会得到 false，而尝试对 MythicalCreature.small troll 求值会产生：
5.1.1. 多重继承
助手是一种神话生物，在得到正确报酬时可以提供帮助：
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 := true
assistance := "heavy labor"
payment := "toy goats"
vulnerability := "sunlight"
这两个父结构类型都扩展了 MythicalCreature。
如果以朴素的方式实现多重继承，那么这可能导致“菱形问题”：对于给定的 MonstrousAssistant，应当通过哪条路径到达 large 将不明确。
它应当从所包含的 Monster 中取得 large，还是从所包含的 Helper 中取得？
在 Lean 中，答案是采用第一个指定的到祖父结构的路径，而额外父结构的字段会被复制，并不是让新结构直接同时包含两个父结构。
这一点可以通过考察 MonstrousAssistant 的构造子的签名看出：
#check MonstrousAssistant.mk
它以一个 Monster 作为参数，并同时接收 Helper 在 MythicalCreature 之上引入的两个字段。
类似地，虽然 MonstrousAssistant.toMonster 只是从构造子中提取 Monster，但 MonstrousAssistant.toHelper 没有可供提取的 Helper。
#print 命令会揭示它的实现：
#print MonstrousAssistant.toHelper
此函数从 MonstrousAssistant 的字段构造一个 Helper。
@[reducible] 属性与写作 abbrev 具有相同效果。
5.1.1.1. 默认声明
当一个结构继承自另一个结构时，可以使用默认字段定义，基于子结构的字段来实例化父结构的字段。
如果需要比判断某个生物是否大型更精细的大小特异性，则可以将一个专门描述大小的数据类型与继承结合使用，从而得到一个结构，其中 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如果子结构不应偏离父结构，则有几种选择：
第二种选择可以如下所示：
abbrev SizesMatch (sc : SizedCreature) : Prop :=
sc.large = (sc.size == Size.large)
注意，单个等号用于表示相等性命题，而双等号用于表示一个检查相等性并返回 Bool 的函数。
SizesMatch 被定义为 abbrev，因为它应当在证明中自动展开，使得 decide 能够看到应当证明的等式。
huldre 是一种中等大小的神话生物——事实上，它们与人类一样高大。
huldre 上的两个大小字段彼此一致：
def huldre : SizedCreature where
size := .medium
example : SizesMatch huldre := ⊢ SizesMatch huldre
All goals completed! 🐙5.1.1.2. 类型类继承
在幕后，类型类就是结构。 定义一个新的类型类会定义一个新的结构，而定义一个实例会创建该结构类型的一个值。 随后它们会被加入 Lean 的内部表中，使 Lean 能够在需要时找到这些实例。 由此可知，类型类可以从其他类型类继承。
由于类型类继承使用的正是相同的语言特性，它支持结构继承的所有特性，包括多重继承、父类型方法的默认实现，以及菱形结构的自动折叠。 这在许多与 Java、C# 和 Kotlin 等语言中的多接口继承有用的相同场景中也很有用。 通过仔细设计类型类继承层次，程序员可以同时获得两方面的优点：一组细粒度、可独立实现的抽象，以及从更大、更一般的抽象自动构造这些特定抽象的能力。