结构体

编写程序的第一步通常是找出问题域中的概念，然后用合适的代码表示它们。有时，一个域概念是其他更简单概念的集合。此时，将这些更简单的组件分组到一个「包」中会很方便，然后可以给它取一个有意义的名称。在 Lean 中，这是使用 结构体（Structure） 完成的，它类似于 C 或 Rust 中的 struct 和 C# 中的 record。

定义一个结构体会向 Lean 引入一个全新的类型，该类型不能化简为任何其他类型。这很有用，因为多个结构体可能表示不同的概念，但它们包含相同的数据。例如，一个点可以用笛卡尔坐标或极坐标表示，每个都是一对浮点数。分别定义不同的结构体可以防止 API 的用户将一个与另一个混淆。

Lean 的浮点数类型称为 Float，浮点数采用通常的表示法。

#check 1.2

1.2 : Float

#check -454.2123215

-454.2123215 : Float

#check 0.0

0.0 : Float

当浮点数使用小数点书写时，Lean 会推断其类型为 Float。如果不使用小数点书写，则可能需要类型标注。

#check 0

0 : Nat

#check (0 : Float)

0 : Float

笛卡尔点是一个结构体，它有两个 Float 字段，称为 x 和 y。它使用 structure 关键字声明。

structure Point where
  x : Float
  y : Float
deriving Repr

声明之后，Point 就是一个新的结构体类型了。最后一行写着 deriving Repr，它要求 Lean 生成代码以显示类型为 Point 的值。此代码用于 #eval 显示求值结果以供程序员使用，类似于 Python 中的 repr 函数。编译器生成的显示代码也可以被覆盖。

创建结构体类型值通常的方法是在大括号内为其所有字段提供值。笛卡尔平面的原点是 x 和 y 均为零的点：

def origin : Point := { x := 0.0, y := 0.0 }

如果 Point 定义中的 deriving Repr 行被省略，则尝试 #eval origin 会产生类似于省略函数参数时产生的错误：

expression
  origin
has type
  Point
but instance
  Lean.MetaEval Point
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

该消息表明求值机制不知道如何将求值结果传达给用户。

幸运的是，使用 deriving Repr，#eval origin 的结果看起来非常像 origin 的定义。

{ x := 0.000000, y := 0.000000 }

由于结构体是用来「打包」一组数据，并将其命名后作为单个单元进行处理的，因此能够提取结构体的各个字段也很重要。这可以使用点记法，就像在 C、Python 或 Rust 中一样。

#eval origin.x

0.000000

#eval origin.y

0.000000

可以定义以结构体为参数的函数。例如，点的加法可通过底层坐标值相加来执行。 #eval addPoints { x := 1.5, y := 32 } { x := -8, y := 0.2 } 会产生

{ x := -6.500000, y := 32.200000 }

该函数本身以两个 Points 作为参数，分别为 p1 和 p2。结果点基于 p1 和 p2 的 x 和 y 字段：

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

类似地，两点之间的距离（即其 x 和 y 分量之差的平方和的平方根）可以写成：

def distance (p1 : Point) (p2 : Point) : Float :=
  Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))

例如，(1, 2) 和 (5, -1) 之间的距离为 5：

#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := -1.0 }

5.000000

不同结构体可能具有同名的字段。例如，三维点数据类型可能共享字段 x 和 y，并使用相同的字段名实例化：

structure Point3D where
  x : Float
  y : Float
  z : Float
deriving Repr

def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }

这意味着必须知道结构体的预期类型才能使用大括号语法。如果类型未知，Lean 将无法实例化结构体。例如，

#check { x := 0.0, y := 0.0 }

会导致错误

invalid {...} notation, expected type is not known

通常，可以通过提供类型标注来补救这种情况。

#check ({ x := 0.0, y := 0.0 } : Point)

{ x := 0.0, y := 0.0 } : Point

为了使程序更加简洁，Lean 还允许在大括号内标注结构体类型。

#check { x := 0.0, y := 0.0 : Point}

{ x := 0.0, y := 0.0 } : Point

更新结构体

设想一个函数 zeroX，它将 Point 的 x 字段置为 0.0。在大多数编程语言社区中，这句话意味着指向 x 的内存位置将被新值覆盖。但是，Lean 没有可变状态。在函数式编程社区中，这种说法几乎总是意味着分配一个新的 Point，其 x 字段指向新值，而其他字段指向输入中的原始值。编写 zeroX 的一种方法是逐字遵循此描述，填写 x 的新值并手动传入 y：

def zeroX (p : Point) : Point :=
  { x := 0, y := p.y }

然而，这种编程风格也存在一些缺点。首先，如果向结构体中添加了一个新字段，那么所有更新任何字段的代码都需要更新，这会导致维护困难。其次，如果结构体中包含多个具有相同类型的字段，那么存在真正的风险，即复制粘贴代码会导致字段内容被复制或交换。最后，程序会变得冗长且呆板。

Lean 提供了一种便捷的语法，用于替换结构体中的一些字段，同时保留其他字段。这是通过在结构体初始化中使用 with 关键字来完成的。未更改字段的源代码写在 with 之前，而新字段写在 with 之后。例如，zeroX 可以仅使用新的 x 值编写：

def zeroX (p : Point) : Point :=
  { p with x := 0 }

请记住，此结构体更新语法不会修改现有值，它会创建一个与旧值共享某些字段的新值。例如，给定点 fourAndThree：

def fourAndThree : Point :=
  { x := 4.3, y := 3.4 }

对其进行求值，然后使用 zeroX 对其进行更新，然后再次对其进行求值，将产生原始值：

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

#eval zeroX fourAndThree

{ x := 0.000000, y := 3.400000 }

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

结构体更新不会修改原始结构体，这样更容易推理新值是从旧值计算得出的。对旧结构体的所有引用会在所有提供的新值中继续引用相同的字段值。

幕后

每个结构体都有一个 构造子（Constructor） 。「Constructor」一词在英文中可能会引起混淆。与 Java 或 Python 等语言中的构造函数不同，Lean 中的构造子不是在初始化数据类型时运行的任意代码。相反，构造子只会收集要存储在新分配的数据结构中的数据。不可能提供一个预处理数据或拒绝无效参数的自定义构造子。这实际上是「Constructor」一词在两种情况下具有不同但相关的含义的情况。

默认情况下，名为 S 的结构体的构造子命名为 S.mk。其中，S 是命名空间限定符， mk 是构造子本身的名称。除了使用大括号初始化语法外，还可以直接应用构造子。

#check Point.mk 1.5 2.8

然而，这通常不被认为是良好的 Lean 风格，Lean 甚至会使用标准结构体初始化语法返回其结果。

{ x := 1.5, y := 2.8 } : Point

构造子具有函数类型，这意味着它们可以在需要函数的任何地方使用。例如，Point.mk 是一个接受两个 Float（分别是 x 和 y），并返回一个新 Point 的函数。

#check (Point.mk)

Point.mk : Float → Float → Point

要覆盖结构体的构造子名称，请在开头写出新的名称后跟两个冒号。例如，要使用 Point.point 而非 Point.mk，请编写：

structure Point where
  point ::
  x : Float
  y : Float
deriving Repr

除了构造子，结构体的每个字段还定义了一个访问器函数。它们在结构体的命名空间中与字段具有相同的名称。对于 Point，会生成访问器函数 Point.x 和 Point.y。

#check (Point.x)

Point.x : Point → Float

#check (Point.y)

Point.y : Point → Float

实际上，就像大括号结构体构造语法会在幕后转换为对结构体构造函数的调用一样， addPoints 中先前定义中的语法 p1.x 会被转换为对 Point.x 访问器的调用。也就是说，#eval origin.x 和 #eval Point.x origin 都会产生

0.000000

访问器的点记法不仅可以与结构字段一起使用。它还可以用于接受任意数量参数的函数。更一般地说，访问器记法具有以下形式：TARGET.f ARG1 ARG2 ...。如果 TARGET 的类型为 T，则调用名为 T.f 的函数。 TARGET 是其类型为 T 的最左边的参数，它通常但并非总是第一个参数，并且 ARG1 ARG2 ... 按顺序作为其余参数提供。例如，即使 String 不是具有 append 字段的结构体，也可以使用访问器记法从字符串中调用 String.append。

#eval "one string".append " and another"

"one string and another"

在该示例中，TARGET 表示 "one string"，ARG1 表示 " and another"。

Point.modifyBoth 函数（即在 Point 命名空间中定义的 modifyBoth）将一个函数应用于 Point 中的两个字段：

def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
  { x := f p.x, y := f p.y }

即使 Point 参数位于函数参数之后，也可以使用点记法：

#eval fourAndThree.modifyBoth Float.floor

{ x := 4.000000, y := 3.000000 }

在这种情况下，TARGET 表示 fourAndThree，而 ARG1 是 Float.floor。这是因为访问器记法的目标用作第一个类型匹配的参数，而不一定是第一个参数。

练习

定义一个名为 RectangularPrism 的结构体，其中包含一个矩形棱柱的高度、宽度和深度，每个都是 Float。
定义一个名为 volume : RectangularPrism → Float 的函数，用于计算矩形棱柱的体积。
定义一个名为 Segment 的结构，它通过其端点表示线段，并定义一个函数 length : Segment → Float，用于计算线段的长度。Segment 最多应有两个字段。
RectangularPrism 的声明引入了哪些名称？
以下 Hamster 和 Book 的声明引入了哪些名称？它们的类型是什么？

structure Hamster where
  name : String
  fluffy : Bool

structure Book where
  makeBook ::
  title : String
  author : String
  price : Float

Lean 函数式编程

结构体

更新结构体

幕后

练习