1.4. 结构
编写程序的第一步通常是识别问题域的概念，然后在代码中为它们找到合适的表示。
有时，一个域概念是其他更简单概念的集合。
在这种情况下，将这些更简单的组件组合到一个单独的"包"中会很方便，然后可以为其赋予有意义的名称。
在 Lean 中，这是通过 结构（Structure） 来完成的，它类似于 C 或 Rust 中的 struct 和 C# 中的 record。
定义结构会向 Lean 引入一个全新的类型，该类型不能化简为任何其他类型。 这很有用，因为多个结构可能表示不同的概念，但包含相同的数据。 例如，一个点可以用笛卡尔坐标或极坐标表示，每个坐标都是一对浮点数。 定义单独的结构可以防止 API 客户端将一个结构与另一个结构混淆。
Lean 的浮点数类型称为 Float，浮点数以通常的记法编写。
#check 1.2#check -454.2123215#check 0.0
当浮点数以小数点形式编写时，Lean 会推断类型为 Float。如果没有小数点，则可能需要类型注解。
#check 0#check (0 : Float)
笛卡尔点是一个具有两个 Float 字段的结构，分别称为 x 和 y。
这使用 structure 关键字声明。
structure Point where
x : Float
y : Float
在此声明之后，Point 是一个新的结构类型。
创建结构类型值的典型方法是在花括号内为其所有字段提供值。
笛卡尔平面的原点是 x 和 y 都为零的地方：
def origin : Point := { x := 0.0, y := 0.0 }
#eval origin 的结果看起来很像 origin 的定义。
因为结构的存在是为了"打包"数据集合，为其命名并将其作为单个单元处理，所以能够提取结构的各个字段也很重要。 这使用点符号完成，就像在 C、Python、Rust 或 JavaScript 中一样。
#eval origin.x#eval origin.y这可以用来定义接受结构作为参数的函数。 例如，点的加法是通过添加底层坐标值来执行的。 应该是这样的情况：
#eval addPoints { x := 1.5, y := 32 } { x := -8, y := 0.2 }产生
函数本身接受两个 Point 作为参数，分别称为 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 }
多个结构可能具有相同名称的字段。
三维点数据类型可以共享字段 x 和 y，并用相同的字段名实例化：
structure Point3D where
x : Float
y : Float
z : Floatdef origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }这意味着必须知道结构的预期类型才能使用花括号语法。 如果类型未知，Lean 将无法实例化结构。 例如，
#check { x := 0.0, y := 0.0 }会导致错误
通常，可以通过提供类型注解来解决这种情况。
#check ({ x := 0.0, y := 0.0 } : Point)为了使程序更简洁，Lean 还允许在花括号内进行结构类型注解。
#check { x := 0.0, y := 0.0 : Point}1.4.1. 更新结构
想象一个函数 zeroX，它将 Point 的 x 字段替换为 0。
在大多数编程语言社区中，这句话意味着 x 指向的内存位置要被新值覆盖。
然而，Lean 是一种函数式编程语言。
在函数式编程社区中，这种陈述几乎总是意味着分配一个新的 Point，其中 x 字段指向新值，所有其他字段指向输入的原始值。
编写 zeroX 的一种方法是按字面意思遵循此描述，填写 x 的新值并手动传输 y：
def zeroX (p : Point) : Point :=
{ x := 0, y := p.y }然而，这种编程风格有缺点。 首先，如果向结构添加新字段，那么所有更新任何字段的位置都必须更新，这会导致维护困难。 其次，如果结构包含多个相同类型的字段，那么复制粘贴编码会导致字段内容重复或交换的真正风险。 最后，程序变得冗长且官僚化。
Lean 提供了一种方便的语法来替换结构中的某些字段，同时保持其他字段不变。
这通过在结构初始化中使用 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#eval zeroX fourAndThree#eval fourAndThree结构更新不修改原始结构这一事实的一个后果是，更容易推理从旧值计算新值的情况。 对旧结构的所有引用继续引用所有提供的新值中的相同字段值。
1.4.2. 幕后的原理
每个结构都有一个构造器。 这里，术语“构造器”可能是混淆的来源。 与 Java 或 Python 等语言中的构造器不同，Lean 中的构造器不是在数据类型初始化时运行的任意代码。 相反，构造器只是收集要存储在新分配的数据结构中的数据。 不可能提供预处理数据或拒绝无效参数的自定义构造器。 这实际上是“构造器”这个词在两种上下文中具有不同但相关含义的情况。
默认情况下，名为 S 的结构的构造器命名为 S.mk。
这里，S 是命名空间限定符，mk 是构造器本身的名称。
除了使用花括号初始化语法外，构造器也可以直接应用。
#check Point.mk 1.5 2.8然而，这通常不被认为是好的 Lean 风格，Lean 甚至使用标准结构初始化器语法返回其反馈。
构造器具有函数类型，这意味着它们可以在期望函数的任何地方使用。
例如，Point.mk 是一个接受两个 Float（分别为 x 和 y）并返回新 Point 的函数。
#check (Point.mk)
要覆盖结构的构造器名称，请在开头用两个冒号编写。
例如，要使用 Point.point 而不是 Point.mk，请写：
structure Point where
point ::
x : Float
y : Float
除了构造器外，还为结构的每个字段定义了访问器函数。
这些函数与字段同名，在结构的命名空间中。
对于 Point，生成访问器函数 Point.x 和 Point.y。
#check (Point.x)#check (Point.y)
实际上，正如花括号结构构造语法在幕后被转换为对结构构造器的调用一样，在 addPoints 的先前定义中的语法 x 被转换为对 x 访问器的调用。
也就是说，#eval origin.x 和 #eval Point.x origin 都产生
访问器点符号不仅可用于结构字段。
它也可以用于接受任意数量参数的函数。
更一般地，访问器记法具有形式 TARGET.f ARG1 ARG2 ...。
如果 TARGET 具有类型 T，则调用名为 T.f 的函数。
TARGET 成为其最左边的 T 类型参数，这通常但不总是第一个参数，ARG1 ARG2 ... 按顺序作为其余参数提供。
例如，String.append 可以使用访问器记法从字符串调用，尽管 String 不是具有 append 字段的结构。
#eval "one string".append " 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
在这种情况下，TARGET 表示 fourAndThree，而 ARG1 是 Float.floor。
这是因为访问器记法的目标用作类型匹配的第一个参数，不一定是第一个参数。
1.4.3. 练习
-
定义一个名为
RectangularPrism的结构，包含长方体的高度、宽度和深度，每个都是Float。 -
定义一个名为
volume : RectangularPrism → Float的函数，计算长方体的体积。 -
定义一个名为
Segment的结构，通过其端点表示线段，并定义一个函数length : Segment → Float来计算线段的长度。Segment最多应该有两个字段。 -
RectangularPrism的声明引入了哪些名称？ -
以下
Hamster和Book的声明引入了哪些名称？它们的类型是什么？structure Hamster where name : String fluffy : Boolstructure Book where makeBook :: title : String author : String price : Float