Lean 代数数据类型

代数数据类型（Algebraic Data Types，简称ADT）是函数式编程中的一个核心概念。在Lean中，ADT用于定义复杂的数据结构，允许我们通过组合简单的类型来构建更复杂的类型。本文将详细介绍Lean中的代数数据类型，并通过示例帮助你理解其用法。

什么是代数数据类型？

代数数据类型是一种复合类型，它通过组合其他类型来定义新的类型。在Lean中，ADT通常通过inductive关键字定义。ADT的核心思想是将类型视为“代数表达式”，通过“和类型”（sum types）和“积类型”（product types）来组合。

在Lean中，我们可以使用inductive关键字定义一个代数数据类型。以下是一个简单的例子：

lean
inductive Shape
  | circle (radius : Float)
  | rectangle (width : Float) (height : Float)

在这个例子中，Shape是一个代数数据类型，它有两个构造函数：

定义好代数数据类型后，我们可以使用它来创建具体的值。例如：

lean
def myCircle : Shape := Shape.circle 5.0
def myRectangle : Shape := Shape.rectangle 4.0 6.0

这里，myCircle是一个半径为5.0的圆形，myRectangle是一个宽度为4.0、高度为6.0的矩形。

代数数据类型的一个强大特性是模式匹配。我们可以根据不同的构造函数来处理不同的情况。例如：

lean
def area : Shape → Float
  | Shape.circle r => 3.14 * r * r
  | Shape.rectangle w h => w * h

在这个例子中，area函数根据传入的Shape类型计算面积。如果传入的是圆形，则计算圆的面积；如果传入的是矩形，则计算矩形的面积。

代数数据类型在编程中有广泛的应用。以下是一些常见的场景：

表示状态：在状态机中，可以使用ADT来表示不同的状态。例如，一个简单的开关状态可以定义为：
lean
```
inductive SwitchState
  | on
  | off
```
解析表达式：在解析数学表达式时，可以使用ADT来表示不同的表达式类型。例如：
lean
```
inductive Expr
  | num (n : Int)
  | add (e1 : Expr) (e2 : Expr)
  | mul (e1 : Expr) (e2 : Expr)
```
处理错误：在处理可能失败的操作时，可以使用ADT来表示成功或失败的结果。例如：
lean
```
inductive Result (α : Type)
  | success (value : α)
  | failure (error : String)
```

代数数据类型是Lean中一个强大的工具，它允许我们通过组合简单的类型来构建复杂的数据结构。通过inductive关键字，我们可以定义自己的ADT，并通过模式匹配来处理不同的情况。ADT在表示状态、解析表达式和处理错误等场景中有着广泛的应用。

提示

如果你想进一步练习，可以尝试定义一个表示二叉树的代数数据类型，并编写一个函数来计算树的高度。