Lean 学习笔记——2. 语言基础、函数与类型系统

Some content in this article was created with AI assistance. Please verify as needed.

本篇只用工具链自带的 Init 和 Std，讨论表达式、函数、类型推断和依赖类型等语言基础，不引入 mathlib。Lean 的整体定位、执行模型和学习路线见第一篇“语言概述与思维转换”。

语言基础

表达式和类型

Lean 中几乎所有语法结构都是表达式：字面量、函数调用、if 和 match 都会产生值。#check 查看表达式的类型，#eval 对可计算的表达式求值。

#check 42          -- Nat
#check true        -- Bool
#check "Lean"      -- String
#check (3, "three") -- Nat × String

#eval 6 * 7        -- 42
#eval String.length "Lean" -- 4

常用的基础类型如下：

类型	含义	示例
`Nat`	自然数，没有负数	`0`、`42`
`Int`	整数	`-3`、`7`
`Float`	浮点数	`3.14`
`Bool`	布尔值	`true`、`false`
`Char`	Unicode 字符	`'λ'`
`String`	字符串	`"Lean"`
`Unit`	只有一个值的类型	`()`

数值字面量本身可能属于多种类型，最终类型由上下文和类型类推断决定：

#check (2 : Nat)
#check (2 : Int)
#check (2 : Float)

#eval (7 : Nat) / 2   -- 3
#eval (7 : Float) / 2 -- 3.500000

Lean 不会把任意值隐式当成布尔条件，if 后面必须是 Bool，或者是一个具有可判定性的命题。纯程序部分先使用 Bool：

def signName (n : Int) : String :=
  if n < 0 then "negative"
  else if n == 0 then "zero"
  else "positive"

#eval signName (-4) -- "negative"

定义

使用 def 创建定义。参数写在名称之后，返回类型写在冒号之后，:= 右边是定义体。

def double (n : Nat) : Nat :=
  n * 2

def greet (name : String) : String :=
  "Hello, " ++ name ++ "!"

#eval double 21
#eval greet "Lean"

返回类型通常可以推断，但公共定义最好显式写出，阅读代码时不必反推类型。

1 2	def answer := 42 #check answer -- Nat

abbrev 也可以创建定义，但它更倾向于在类型检查和打印时被展开，适合简单别名：

abbrev UserId := Nat

def nextUser (id : UserId) : UserId :=
  id + 1

Lean 的标识符区分大小写，通常使用小驼峰命名值和函数，使用大驼峰命名类型。数学对象可以使用 Unicode 字母命名：

1 2	def πApprox : Float := 3.1415926 #eval πApprox

本系列优先使用这种写法，但不使用 Unicode 上下标给名称编号：写 h1、h2、x0，不写 h₁、h₂、x₀。上下标适合排版公式，不适合承担源码中的版本号和序号。

局部绑定

let 在表达式内部绑定局部名称，最后一行是整个表达式的值：

def rectangleArea (width height : Nat) : Nat :=
  let area := width * height
  area

#eval rectangleArea 6 7 -- 42

同一个 let 块中，后面的绑定可以使用前面的绑定：

def circleInfo (radius : Float) : Float × Float :=
  let pi := 3.1415926
  let diameter := 2.0 * radius
  let circumference := pi * diameter
  (diameter, circumference)

where 可以把辅助定义放到主定义之后，避免打断主要逻辑：

def formatUser (name : String) (age : Nat) : String :=
  name ++ " (" ++ showAge age ++ ")"
where
  showAge (n : Nat) : String :=
    toString n

#eval formatUser "Ada" 36

注释和布局

Lean 使用 -- 表示单行注释，使用 /- ... -/ 表示可以嵌套的块注释：

-- 单行注释

/-
块注释
  /- 可以嵌套 -/
-/

Lean 对缩进敏感。缩进不是 Python 那样唯一的分块符号，但会参与 do、match、where 等布局语法的解析。稳定的做法是每进入一层就增加两个空格，并让同级分支对齐。

字符串插值

字符串可以使用 s!"..." 插入实现了字符串转换的值：

def report (name : String) (score : Nat) : String :=
  s!"{name}: {score}"

#eval report "Lean" 100

普通字符串拼接使用 ++。插值在混合多个非字符串值时更清楚。

类型错误

Lean 会在执行以前检查所有表达式的类型。例如下面的定义无法通过检查：

1	-- def bad : Nat := "42"

这类错误不是运行时异常，而是源文件 elaboration 阶段的错误。学习 Lean 时应该经常使用 #check 缩小问题：先确认函数类型，再确认每个参数的类型，最后检查组合后的表达式。

函数、参数与多态

Lean 是函数式语言，函数本身也是值。理解函数类型、柯里化和隐式参数以后，很多看似特殊的 Lean 语法都会变得直接。

函数类型

函数类型写成 A → B，表示接收 A 并返回 B。箭头向右结合：

1
2
3

#check Nat → String
#check Nat → Nat → Nat
-- Nat → (Nat → Nat)

因此下面的 add 并不是一次接收一个二元组，而是先接收 a，返回一个等待 b 的函数：

def add (a b : Nat) : Nat :=
  a + b

#check add      -- Nat → Nat → Nat
#check add 10   -- Nat → Nat
#eval add 10 32 -- 42

这种形式称为柯里化。部分应用不需要专门的 partial 或 bind：

1
2
3

def addTen : Nat → Nat := add 10

#eval addTen 5 -- 15

匿名函数

匿名函数使用 fun 和 =>，编辑器通常会把箭头显示为 ↦：

1 2	#check fun x : Nat => x + 1 #eval (fun x : Nat => x * x) 7

多个参数可以连续书写：

1 2	def multiply : Nat → Nat → Nat := fun x y => x * y

参数类型能从整体类型推断，因此定义体中的 x 和 y 不必重复标注。

高阶函数

接收函数或返回函数的函数称为高阶函数：

def twice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)

#eval twice (fun x => x + 3) 10 -- 16

函数组合可以写成一个普通定义：

def compose (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

#eval compose toString (fun n : Nat => n * 2) 21
-- "42"

这里的 α、β 和 γ 是自动引入的类型参数。项目若设置了 relaxedAutoImplicit = false，则应该显式声明：

1
2
3

def compose' {α β γ : Type}
    (g : β → γ) (f : α → β) : α → γ :=
  fun x => g (f x)

显式声明更容易发现名称拼写错误，大型项目通常采用这种写法。

多态函数

同一个函数可以操作任意类型，这里的多态发生在编译期，不依赖继承：

def first {α β : Type} (pair : α × β) : α :=
  pair.1

#eval first (42, "answer")
#eval first (true, 3.14)

Type 自己也有层级。最常见的程序类型写成 Type 即可，更一般的库代码会写宇宙参数：

universe u v

def keepLeft {α : Type u} {β : Type v}
    (a : α) (_ : β) : α :=
  a

宇宙层级避免了“所有类型构成的类型也属于自己”所造成的悖论。日常程序很少需要手动计算层级。

参数可见性

圆括号参数必须显式提供，花括号参数通常由 Lean 从其他参数推断：

def identity {α : Type} (x : α) : α := x

#eval identity 42
#eval identity "Lean"

需要手动提供隐式参数时，使用 @ 暴露所有参数，或者使用具名参数：

1
2
3

#check @identity
#eval @identity Nat 42
#eval identity (α := String) "Lean"

方括号参数 [C α] 是实例隐式参数，由类型类搜索负责补全，和普通花括号参数不是同一种机制：

def sameText {α : Type} [ToString α] (x : α) : String :=
  toString x ++ " / " ++ toString x

#eval sameText 42

类型类会在后面的笔记中单独整理。

具名参数

显式参数也可以按名称传递，适合参数较多、交换同类型参数容易出错的函数：

def sliceLabel (start stop : Nat) : String :=
  s!"[{start}, {stop})"

#eval sliceLabel (stop := 10) (start := 3)

具名参数使用定义中的参数名，因此公共 API 的参数名也是接口的一部分。

管道

|> 把左侧值作为右侧函数的最后一个显式参数：

1 2	#eval " lean " \|> String.trimAscii \|>.toString \|> String.toUpper -- "LEAN"

函数调用本身的优先级很高，复杂表达式最好用括号或管道明确数据流：

def surround (left right text : String) : String :=
  left ++ text ++ right

#eval "Lean" |> surround "[" "]"

局部函数

辅助函数可以通过 let 或 where 保持在局部作用域：

def transform (n : Nat) : Nat :=
  let step (x : Nat) := x * 2 + 1
  step (step n)

def transform' (n : Nat) : Nat :=
  step (step n)
where
  step (x : Nat) := x * 2 + 1

where 中的定义可以访问主定义的参数，但放在局部函数参数中通常更清楚，也更容易单独抽取和复用。

编译流程

Lean 前端承担的工作比普通静态语言更多。源码大致经历：

字符流
  ↓ parser
语法树 Syntax
  ↓ macro expansion
展开后的语法
  ↓ elaboration
带完整类型的表达式 Expr
  ↓ kernel checking
通过内核检查的声明
  ↓ compiler（需要运行的定义）
中间表示与原生代码

parser 只关心代码能不能按照语法规则读懂。elaborator 则负责：

名称解析；
插入隐式参数；
推断省略的类型；
解释重载记号；
求解类型类实例；
展开一部分语法糖；
把 tactic 脚本转换为证明项；
生成仍待解决的 metavariable。

内核检查的是 elaborator 生成的核心表达式，不是用户写下的表面语法。

这与 C++ 模板实例化、Rust trait 求解以及 Haskell 类型类推断有相似之处，但 Lean 的 elaborator 还必须处理依赖类型：后一个参数的类型可以依赖前一个参数的值，因此约束求解明显更复杂。

Lean 的许多错误信息来自 elaboration 阶段。“application type mismatch”不一定说明函数本身有问题，也可能是某个隐式参数或类型类实例没有被推断出来。

表达式语言与语句语言

C、Python 和 Java 把“产生值的表达式”与“控制执行的语句”区分得比较明显。Lean 更接近 ML 和 Haskell：

if 会产生值；
match 会产生值；
let 会产生值；
do 块最终也有一个类型和值；
函数体就是一个表达式。

因此可以把条件表达式直接放进更大的表达式：

def clamp (low high value : Int) : Int :=
  if value < low then low
  else if high < value then high
  else value

def clampLabel (low high value : Int) : String :=
  s!"result = {clamp low high value}"

if 的两个分支必须具有兼容类型：

1 2	-- 无法通过类型检查：两个分支分别是 Nat 和 String -- def badIf (flag : Bool) := if flag then 1 else "one"

Python 允许变量在不同分支中绑定为完全不同的运行时类型；Lean 要求表达式在执行以前具有确定类型。如果结果确实有两种形态，应使用 Sum、Option、Except 或自定义归纳类型表达，而不是隐藏差异。

类型推断

Lean 是静态类型语言，但具有较强的类型推断。下面三个定义都能推断出 Nat → Nat：

1
2
3

def inc1 (n : Nat) : Nat := n + 1
def inc2 (n : Nat) := n + 1
def inc3 : Nat → Nat := fun n => n + 1

推断不是从源码中凭空猜测作者意图，而是收集并求解约束。例如 inc3 的过程可以粗略理解为：

期望类型是 Nat → Nat；
因此匿名函数参数 n 的期望类型是 Nat；
函数体的期望类型也是 Nat；
n + 1 中的 + 和字面量 1 都按 Nat 解释。

这种由外向内传播期望类型、再由内向外合成实际类型的方式称为双向类型检查。

与 C++ 的 auto 相比，Lean 的推断还要同时处理隐式参数和类型类。与动态语言相比，推断只是在编译期省略标注，并没有把类型检查推迟到运行时。

公共函数建议写出参数和返回类型：

1 2	def normalizeName (name : String) : String := name.trimAscii.toString.toLower

这样做的好处包括：

定义本身就是接口文档；
修改函数体时不会无意改变公开类型；
错误位置更接近缺少信息的表达式；
elaborator 能利用标注继续求解其余约束。

重载字面量与运算符

Lean 中的 0、1、+、* 并不只属于某个内置数值类型。它们通过类型类解释：

#check (0 : Nat)
#check (0 : Int)
#check (0 : Float)

#check (fun x : Nat => x + x)
#check (fun x : Int => x + x)

从概念上看：

数字字面量依赖 OfNat；
加法依赖 HAdd 或 Add；
乘法依赖 HMul 或 Mul；
比较依赖相应的序关系或布尔比较实例。

这比 C++ 运算符重载更加系统，也更接近 Haskell 的 Num 类型类。区别是 Lean 的输出类型甚至可以依赖输入类型和实例参数，因此异构运算符可以表达更一般的接口。

上下文不足时，Lean 可能无法确定字面量类型：

1 2	def natZero : Nat := 0 def intZero : Int := 0

在错误信息中看到 OfNat ?m ... 或 HAdd.hAdd 一类名称时，通常不是让用户直接操作这些底层定义，而是提示需要补充类型标注。

Bool、Decidable 与 Prop

Bool 是可计算的数据类型，只有 true 和 false 两个值。Prop 是命题所在的 sort。二者都能表达真假，但用途不同：

def isEvenBool (n : Nat) : Bool :=
  n % 2 == 0

def IsEvenProp (n : Nat) : Prop :=
  ∃ k, n = 2 * k

isEvenBool 10 可以直接执行；IsEvenProp 10 描述的是一个需要证明的命题。

Lean 可以通过 Decidable P 把某些命题转成可计算判断，因此 if h : n = 0 then ... 也是合法语法：

def zeroOrSucc (n : Nat) : String :=
  if h : n = 0 then
    "zero"
  else
    "nonzero"

这里 h 在第一个分支中是 n = 0 的证明，在第二个分支中是 n ≠ 0 的证明。依赖 if 不只是选择运行路径，还会向各分支上下文加入不同的类型信息。

在普通语言中，条件表达式通常只改变控制流；在依赖类型语言中，控制流还会细化后续代码可用的事实。这与 Rust 根据 match 缩小枚举分支相似，但 Lean 细化的是任意命题。

定义相等

Lean 中有两种需要区分的“相等”：

定义相等：展开定义、执行归约以后得到同一个核心表达式；
命题相等：类型为 a = b 的命题，需要一个证明项。

例如：

def twiceNat (n : Nat) := n + n

example (n : Nat) : twiceNat n = n + n := by
  rfl

rfl 能完成，是因为展开 twiceNat 以后两边相同。这里不是调用了关于加法的数学定理。

下面的交换律则不是定义相等：

1
2
3

-- 需要数学证明，不能只依赖展开和计算
-- example (a b : Nat) : a + b = b + a := by
--   exact Nat.add_comm a b

定义相等决定了类型检查器何时可以把两个类型当作同一个类型。依赖类型中，类型里可能包含计算，因此内核必须在比较类型时进行受控归约。

求值与归约

几个看起来都能“算结果”的命令，实际目的并不相同：

1 2	#eval (List.range 6).map (fun n => n * n) #reduce (fun n : Nat => n + 1) 4

#eval 使用编译后的求值机制，速度较快，适合运行程序；
#reduce 使用定义归约，更接近内核理解表达式的方式，复杂程序可能很慢；
rfl 只在两边定义相等时构造反身性证明；
native_decide 等 mathlib 工具会利用原生计算完成可判定命题。

Lean 不是把证明过程简单地解释执行一遍。证明项会由内核检查，而普通程序定义可以走更高效的编译路径。两条路径共享类型系统，但性能目标不同。

值、多态与宇宙

普通数据类型本身也是值：

#check Nat       -- Type
#check String    -- Type
#check List Nat  -- Type
#check Type      -- Type 1

如果直接让“所有类型的类型”也属于自己，会产生类似 Russell 悖论的问题。Lean 因此使用宇宙层级：

universe u2 v2

#check Type u2

def swapTypes {α : Type u2} {β : Type v2}
    (pair : α × β) : β × α :=
  (pair.2, pair.1)

Type u 属于更高一层的 Type (u + 1)。大多数代码让 Lean 自动推断 universe，只在编写高度泛型的基础库时显式声明。

Prop 在层级体系中有特殊地位。命题证明在运行时代码中通常会被擦除，不同证明也不会因为携带不同计算数据而影响普通程序行为。这是 Lean 能同时作为编程语言和证明器的重要设计。

依赖函数类型

普通函数类型 α → β 的返回类型不依赖参数值。更一般的依赖函数写成：

1	#check ((n : Nat) → Fin (n + 1))

输入不同的 n 会得到不同返回类型。下面的函数总能返回合法的零下标：

def firstIndex (n : Nat) : Fin (n + 1) :=
  ⟨0, Nat.zero_lt_succ n⟩

#eval (firstIndex 10).val

这种函数类型也称为 dependent function type 或 Π 类型。普通箭头只是参数没有出现在返回类型中的特例。

与泛型相比，依赖类型的约束更强：C++ 模板可以为不同参数生成不同代码，但类型系统通常不会直接表达“返回的数组长度等于输入的自然数值”；Lean 可以把这种关系放进类型。

代价也很明显：

类型检查可能需要计算；
改写值时可能同时需要改写类型；
错误信息包含更多隐式信息；
API 设计需要在精确性和使用成本之间取舍。

因此并不是所有边界条件都应该塞进类型。对于普通应用程序，Option 或 Except 有时比携带复杂证明的 subtype 更实用。

柯里化

Lean 的：

1	def addCurried (a : Nat) (b : Nat) : Nat := a + b

核心类型是：

1	#check (Nat → Nat → Nat)

而不是：

1	#check (Nat × Nat → Nat)

两者可以相互转换：

def curry {α β γ : Type}
    (f : α × β → γ) : α → β → γ :=
  fun a b => f (a, b)

def uncurry {α β γ : Type}
    (f : α → β → γ) : α × β → γ :=
  fun pair => f pair.1 pair.2

柯里化的直接收益是部分应用：

1
2
3

def add100 := addCurried 100

#eval [1, 2, 3].map add100

Haskell、OCaml 和 F# 也以柯里化函数为主；Python 和 C++ 通常把参数列表视作一次调用，需要 lambda、partial 或 bind 才能显式固定一部分参数。

闭包与捕获

匿名函数可以捕获外层局部值：

def makeAdder (offset : Nat) : Nat → Nat :=
  fun value => offset + value

def addSeven := makeAdder 7

#eval addSeven 35

返回的函数必须保留 offset，因此它是一个闭包。编译器会把被捕获的环境与函数代码一起表示。

纯函数中的捕获值不可在闭包内部随意原地修改，这与 Python 的 nonlocal、C++ 的引用捕获不同。需要状态变化时，应显式返回新状态，或在 StateM、IO 等上下文中使用受控可变性。

隐式参数的语义

花括号参数：

1 2	def singleton {α : Type} (x : α) : List α := [x]

不是 Python 中“省略后使用默认值”的参数。它没有一个预先写死的值，而是由上下文推断：

1 2	#eval singleton 42 #eval singleton "Lean"

@singleton 会关闭隐式插入，展示真实参数列表：

1 2	#check @singleton #eval @singleton Nat 42

常见的三类参数：

写法	含义
`(x : α)`	调用者通常显式提供
`{α : Type}`	elaborator 根据上下文推断
`[inst : C α]`	类型类搜索寻找实例

它们最终都可以理解为函数参数，只是自动填充机制不同。

autoImplicit

Lean 默认会根据未知标识符自动引入隐式变量：

1	def keep (x : α) : α := x

这里的 α 可以自动成为 {α : Sort u}。这种写法在数学代码中很简洁，但拼写错误也可能被误认为新变量。

mathlib 项目模板通常设置：

1	set_option autoImplicit false

或在 Lake 配置中关闭宽松自动隐式。此时应显式写：

1	def keepExplicit {α : Type} (x : α) : α := x

阅读现有代码时需要认识自动隐式参数。自己维护的项目若关闭该选项，拼写错误会更早暴露。

工程细节

Unicode 输入

Lean 4 的 VS Code 扩展提供反斜杠输入法。在 Lean 文件中键入 \ 和缩写，例如 \alpha，完成后会自动替换为 α；缩写尚未自动完成时可以按 Tab。将鼠标悬停在已有符号上，可以查看它支持的缩写。命令面板中的 Lean 4: Docs: Show Unicode Input Abbreviations 会显示完整列表；Lean 4: Input: Find Unicode Symbol 可以按缩写或符号反向搜索。

常用输入如下。表中“ASCII 等价形式”有两类：->、forall 等是直接的替代语法；And、Set.inter 等是符号展开后的声明名称，语义等价但通常更冗长。

符号	输入	ASCII 等价形式
`α`、`β`、`γ`	`\alpha`、`\beta`、`\gamma`	标识符 `alpha`、`beta`、`gamma`
`ℕ`、`ℤ`、`ℚ`、`ℝ`	`\N`、`\Z`、`\Q`、`\R`	`Nat`、`Int`、`Rat`、`Real`
`→`、`↔`	`\to`、`\iff`	`->`、`<->`
`∀`、`∃`	`\forall`、`\exists`	`forall`、`exists`
`∧`、`∨`、`¬`	`\and`、`\or`、`\not`	`And`、`Or`、`Not`
`≠`、`≤`、`≥`	`\ne`、`\le`、`\ge`	`Not (a = b)`、`<=`、`>=`
`∈`、`∉`、`⊆`	`\in`、`\notin`、`\sub`	`Membership.mem`、`Not (Membership.mem ...)`、`Set` 上的 `<=`
`∅`、`∩`、`∪`	`\empty`、`\inter`、`\union`	`Set.empty`、`Set.inter`、`Set.union`
`∑`、`∏`、`•`	`\sum`、`\prod`、`\smul`	`Finset.sum`、`Finset.prod`、`SMul.smul`
`⟨⟩`	`\<>`	由目标类型决定具体构造器

尖括号没有唯一的 ASCII 展开：⟨hP, hQ⟩ 在合取目标中对应 And.intro hP hQ，在积类型中可能对应 Prod.mk，在存在命题中则携带见证及其证明。理解底层名称有助于查文档，但实际代码应选择最清楚的写法，而不是机械地消除 Unicode。

名称解析与点号语法

函数调用：

1	#eval String.toUpper "lean"

可以写成：

1	#eval "lean".toUpper

点号语法会根据参数类型和定义所在命名空间寻找合适函数，并把左侧值插入指定参数位置。它不表示值携带虚函数表，也不代表运行时动态派发。

这一点与 C++/Java 的方法调用差异很大，却与 Rust 的 method call desugaring 有些相似：表面上像方法，底层仍可以理解为普通函数调用加名称解析。

点号语法适合数据流：

1
2
3

#eval [1, 2, 3, 4]
  |>.filter (fun n => n % 2 == 0)
  |>.map (fun n => n * 10)

其中 |> 再把上一步结果传给下一步函数，避免括号嵌套。

运算优先级与括号

函数应用的优先级很高：

f x + g y

会解析为：

1	(f x) + (g y)

箭头向右结合：

1	#check (Nat → Nat → String)

等价于：

1	#check (Nat → (Nat → String))

函数应用向左结合：

f x y

等价于：

(f x) y

这两个结合规则正好解释了柯里化调用。遇到复杂的 tactic 参数、类型类参数和高阶函数时，不要吝啬括号，清楚比最短更重要。

不可变数据

Lean 的普通值具有不可变语义：

def original := #[1, 2, 3]
def updated := original.setIfInBounds 0 99

#eval original
#eval updated

不可变语义不代表底层每次更新都完整复制。Lean 编译器可以利用引用计数判断对象是否唯一：若没有其他引用，就地复用底层对象仍然不会改变程序可观察语义。

这类优化称为 functional but in-place。它与 Rust 所有权有相似目标：尽量确认某个对象没有别名后安全修改。区别是 Rust 把大部分规则暴露在静态借用检查中，Lean 更多依赖运行时引用计数和编译器优化，源码仍保持纯函数接口。

错误诊断

面对很长的错误信息，可以按下面顺序排查：

找最先出现的源码位置，不要先看后续级联错误；
用 #check 查看被调用函数的完整类型；
给关键字面量、空列表和匿名函数参数补类型；
检查是普通隐式参数失败，还是类型类实例失败；
检查期望类型是否把表达式解释成了另一套重载；
把长表达式拆成几个带类型的 let 或 have；
必要时用 set_option pp.all true 查看更完整表达式，但不要长期保留。

例如空列表没有元素可供推断：

1 2	#check ([] : List Nat) #check ([] : List String)

匿名函数也可能需要参数标注：

1	#check (fun n : Nat => n + 1)

拆开长表达式后，许多报错只剩下局部的类型不一致，例如 Nat 与 Int 混用。

语言对比

特性	Lean	Haskell	Rust	Python
类型检查	静态、依赖类型	静态、高阶 kind	静态、所有权类型	动态为主
函数	默认柯里化	默认柯里化	多参数调用	多参数调用
副作用	通过 `IO` 等类型表达	通过 Monad	普通语句，所有权约束	普通语句
多态	universe + 隐式参数	parametric polymorphism	泛型与 trait	duck typing
重载	类型类	类型类	trait	运行时方法
数据	归纳类型	ADT	enum/struct	class/对象
证明	核心功能	通常不做	通常不做	不支持

Lean 与普通函数式语言的主要差别是：值可以出现在类型中，类型检查可能触发计算，省略的信息由 elaborator 补全，证明和程序共用项与类型。遇到报错时，先检查期望类型、隐式参数和类型类实例，往往比按动态语言的运行时模型猜测更有效。