写给一般计算机人的Lean4安利

本文主要给有计算机背景(起码懂一门强类型编程语言, 如果读者懂函数式编程或者 Rust 就更好了)的人介绍一下 Lean4 (作为一个编程语言而不是证明助手).

环境配置不在本文介绍范围内, 请参考https://lean-lang.org/lean4/doc/setup.html或者参考这里https://zhuanlan.zhihu.com/p/656770107.

另外由于 Markdown 缺少 Lean 的高亮, 我们会借用 Haskell 的高亮, 文中的代码除特殊注明外全部为 Lean4代码

Lean4 是什么

Lean 是微软研究院推出的一款定理证明器, 它同时也是一款极其先进的通用编程语言, 如今已到第四个大版本. 在此文中我们忽略 Lean 在前沿数学中的突出贡献, 而只介绍作为编程语言的 Lean4.

Lean4 是一个函数式语言

Lean4 程序由一系列定义构成, 最顶层的定义可以为函数或者是类型, 我们这里先介绍函数, 如下是一个简单的函数定义(这里借用了 Haskell 的高亮):

def addOne(x : Int) : Int := x + 1

这里用到的语法几乎是显然的, 我们定义了一个函数 addOne, 它接受一个类型为 Int 的变量 x, 返回一个Int, 返回值类型可以省略交由 Lean 来推导

def addOne(x : Int) := x + 1

可以在 vscode 里快速测试这个函数(如果你配置好了Lean4的环境的话)

#eval addOne 2

当光标放在这一行的时候, Lean Infoview 窗口会显示 3. 这里调用函数直接使用空格分割函数和实参, 而不像一般语言中常见的 addOne(2), 如果您不了解函数式编程的话, 我们马上能看出为什么要如此设计.

多参数函数

在一些常见的编程语言中, 我们可能会如此定义一个多参函数:

# 这是 Python 代码
def add1(x : Int , y : Int):
  return x + y

这可以看作是一个从两个整数到一个整数的映射, 我们记作 Int × Int → Int. 给它两个整数x y, 它才还你一个整数x + y. 描述这个函数还有另一个思路:

# 这是 Python 代码
def add2(x : Int):
  return lambda y : x + y

对于这个函数, 如果你只给它一个整数x, 它会变成另一个函数, 这个函数会要求你再给一个整数y, 然后才还你一个整数x+y. 这样这个函数可以看作一个从整数到一个函数的映射, 我们记作 Int → (Int → Int), 或者省略括号直接记作 Int → Int → Int. 我们默认给函数箭头加括号的规则是从右往左, 注意这个箭头→并不满足结合律, 即, Int → (Int → Int) 和 (Int → Int) → Int 显然不是一回事.

相比于大多数人熟悉的第一种写法, Lean(和一大票函数式语言)更倾向于第二种写法, 这样我们可以写一个 Lean4 版本的 add 函数.

def add (x : Int) (y : Int) := x + y

如果两个(或多个)参数的类型一样, 它们可以被合并写作

def add (x y : Int) := x + y

使用 #eval add 2 3 可以测试一下这个函数, 使用 #check add 可以看一看这个函数的类型. 然后我们可以更简单地定义 addOne 函数

def addOne := add 1

lambda 表达式

def add := fun (x y : Int) => x + y

或者在上下文类型明确时不去标注参数类型

def add : Int → Int → Int := fun x y => x + y

在 vscode 中依次按下 空格] 可以打出符号→, 如果不喜欢unicode, 也可以使用 -> 代替.

Lean4 是一个强类型语言

强类型语言意味着这个语言中的所有表达式都有一个所属的类型, 并且这些类型会在编译期确定并检查, 有效的类型检查是程序安全性的重要保障, 强大的类型系统是语言抽象能力的重要体现.

我们已经见识到了两种类型, 一个整数类型 Int 一个是函数类型 →, 后者其实是我们常说的泛型, 这点我们稍后再谈.

一些常用类型

我们列举出一些常用的类型和它们对应的值(-- 是 Lean 的行注释的起始符)

3  : Int -- 整数
-2 : Int 

0 : Nat -- 自然数
1 : Nat
2 : Nat

3.14 : Float -- 浮点数
3.00 : Float

'c' : Char -- 字符

"Hello" : String -- 字符串

true : Bool -- 布尔
false : Bool 

() : Unit -- 单元类型, 这个类型只有一个元素 ()

fun (x : Int) => x + 1 : Int → Int

定义类型

我们可以用如下语法定义一个结构体

structure Point2D where
  x : Float
  y : Float
deriving Repr

Pointe2D 是我们定义的新类型的名字, x y 是两个分量的名字, 后面的: Float说明了分量的类型, 如果你熟悉Rust, 那么最后一行的作用就是 #[derive(Display)]的作用; 如果你熟悉 Haskell , 那么最后一行的作用与 deriving Show 无异. 那些不熟悉这些语言的读者也不必担心, 这句话的作用就是让 Lean 帮我们生成一个可以输出 Point2D 的函数.这样我们就能 #eval 一个类型为 Point2D 的表达式.

我们可以使用 Point2D.mk 函数构造一个 Point2D

def origin : Point2D := Point2D.mk 0.0 0.0

Point2D.mk 是一个由 Lean 自动生成的函数, 称为构造子, 用来构造一个值. 在上下文类型明确的情况下, 也可以使用如下语法构造 Point2D

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

如果我们想给构造子命名, 我们可以这样定义 Point2D

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

#check Point2D.point -- Point2D.point (x y : Float) : Point2D

(#check 用来获取一个表达式的类型)

我们可以用句点来访问分量

#eval origin.x -- 0
#eval origin.y -- 0

归纳类型

我们现在来介绍归纳类型, 在别的语言中, 这也常称为代数数据类型, 我们可以看一下 Lean 中的布尔型是如何定义的

inductive Bool where
  | false : Bool
  | true : Bool

其中 Bool 是定义的类型的名字, true 和 false 是两个构造子, 构造子指明了如何构造一个 Bool, 在这里有两个构造子, 意味着有两个方法来构造 Bool 类型. 如下

Bool.true : Bool
Bool.false : Bool

不用我说, Haskell 用户就知道这是什么; Rust 用户可能会记起他们的 enum

// 这是 Rust
enum Bool {
  True, 
  False,
}

为了和归纳类型一起工作, Lean 和大多数语言一样都提供了模式匹配的语法, 比如我们可以这样来写一个 not 函数

def myNot (b : Bool) :=
  match b with
  | Bool.true => Bool.false
  | Bool.false => Bool.true

或

def myNot : Bool → Bool 
| Bool.true => Bool.false
| Bool.false => Bool.true

为了适配不同人群的需求, Lean 经常会对同一个功能定义不同的语法, 上面两种定义实际没有区别, 我们以第一种为例来说明, 此句使用了 match 语句, 对 b 匹配, 提供两条通路, 如果 b 可以被 Bool.true 匹配就会走第一条路, 通向 Bool.false, 如果第一条不匹配, 就去匹配Bool.false, 匹配成功就会通向 Bool.true. Bool 的定义只有两种构造子, 这表明这两种构造子一定可以覆盖 b 的所有情况.

---

现在我们考虑一个 Shape 类型, 我们可能会有这种需求: 一个形状可能是确定长和宽的矩形, 也可能是给定半径的圆形. 我们可以构造如下类型来表示这个需求

inductive Shape where
  | rect (a b : Float) : Shape
  | circ (r : Float)   : Shape
deriving Repr

然后定义一个计算面积的函数来展示我们如何进行模式匹配

def area (s : Shape) := match s with
  | Shape.rect a b => a * b
  | Shape.circ r => 3.14 * r * r

#eval area (Shape.rect 2 3) -- 6.000000
#eval area (Shape.circ 1)   -- 3.140000

归纳的类型和递归

我们可以归纳地定义一个类型, 比如标准库里的自然数是这样定义的

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

这个类型令人惊奇的地方在于第二个构造子 succ 的参数居然是 Nat 类型本身, 而我们现在正在定义 Nat, 这样我们可以这样构造类型

open Nat -- 打开Nat命名空间, 这样我们就可以直接写 zero 和 succ 而不是 Nat.zero ...

#check zero -- 这代表 0
#check succ zero -- 这代表 1
#check succ (succ zero) -- 这代表 2
...

现在我们可以递归地定义如下函数

def myAdd (m n : Nat) := match m with
  | zero    => n
  | succ pm => succ (myAdd pm n)

Lean 和其他的证明助手一样, 都要求你的递归必须是显然能够终止的, 即, 你每次递归调用的参数必须在一步步"减小", 比如这里定义的 myAdd, 每次递归的时候, 它的第一个参数就在不断地减小, 此时 Lean 就能看出来它是明显终止的, 倘若一个函数终止的并不明显, 比如下面的函数

def checkCollatz (n : Nat) : Unit :=
  if n == 1 || n == 0 then
    ()
  else if Nat.mod n 2 == 0 then
    checkCollatz (Nat.div n 2)
  else
    checkCollatz (3 * n + 1)

如果角谷猜想成立, 那么这个函数必然在有限步内终止, Lean 当然看不出来, 不允许你编译此函数. 但我们确实需要这个函数, 这时候我们只需要在 def 前面加一个 partial 告诉 Lean 这个函数有可能是不完全的(在一些数值上没有良好定义).

partial def checkCollatz (n : Nat) : Unit :=
  if n == 1 || n == 0 then
    ()
  else if Nat.mod n 2 == 0 then
    checkCollatz (Nat.div n 2)
  else
    checkCollatz (3 * n + 1)

不完全的函数是通用编程的客观需要, 比如我们的一个服务器程序, 我们需要它主动进入一个死循环, 而很多函数的终止性很难证明, 所以与其花时间证明它终止, 不如直接写个 partial.

Lean 中的列表定义如下

inductive List α where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

其中 α 是一个类型参数, 在其他语言里, 可能写作 List<α>, 这个列表的定义和自然数异曲同工, 不再赘述.

然后这里还有两个常用类型

inductive Sum (α : Type _) (β : Type _) where
  | inl (val : α) : Sum α β
  | inr (val : β) : Sum α β

structure Prd (α : Type _) (β : Type _) where
  fst : α
  snd : β

其中 (α : Type _) (β : Type _) 表明 α β 是两个类型, 在前面的例子中我们省略了这个标注(Lean可以推出来), 下划线意味着这里省略了一个类型层级的标注, 一般编程无需关注.

第一个类型是 Rust 人熟悉的 Result, Haskell中叫做 Either, 第二个是我们大家都熟悉的二元组, 可以用 (x,y) 快速构造一个二元组, 多元组就是二元组的嵌套, 即 (x, (y, z)), Lean 允许我们简记作 (x,y,z).

Lean4 是一个"命令式语言"

正如很多纯函数式语言做的那样, Lean4 将输入输出功能放在一个称为 IO 的上下文里, 得益于 do notation, 你不必了解任何单子相关知识也能使用 IO 操作.

如下是一个简单的计算 a + b 的程序

def main : IO Unit := do
  let stdin ← IO.getStdin
  if let [some a,some b] := Functor.map String.toNat? ((←stdin.getLine).split (· == ' ')) then
    IO.println (a + b)
  else
    IO.println "Read Error"

IO α 可以看作一个装着一个 α 的箱子, 这个箱子只能在 IO 的上下文(比如这里的do之后的上下文)内打开, 打开的方法就是使用 ←. 比如这里的 IO.getStdin , 它的类型是 IO Stream, 所以我们可以用 ← 把里面的 Stream 取出来放到变量 stdin 里.

do 可以出现在任何需要用到类型为 IO α 的地方(实际上它有更广泛的适用条件), 写下 do 之后就可以想写命令式语言一样写程序. 我们甚至可以定义可变量

-- 计算 1 + 2 + ... + 100
def main : IO Unit := do
  let mut sum := 0
  for i in List.range 101 do
    sum := sum + i
  IO.println sum

令 Haskell 用户惊奇的是 Lean4 可以使用 break 跳出循环

-- 从一数到一百
def main : IO Unit := do
  let mut i := 1
  while True do
    if i > 100 then
      break
    IO.println i
    i := i + 1

同样 Lean4 可以使用 continue 和 early return.

Lean4 是一个依值类型语言

一般的语言中允许像是 List α 这样的类型, 这个类型依赖于类型参数 α. 那么一个自然的想法是一个类型可不可以依赖于一个值? 答案是肯定的, 比如如下的类型

inductive Vec : Nat → Type _ → Type _ where
  | nil : Vec 0 α
  | cons : α → Vec n α → Vec (Nat.succ n) α

Vec 就包含一个自然数参数, 并且归纳的规则正好可以限制列表的长度为这个自然数. 利用 Vec 类型, 我们可以保证不会触发越界问题.

我们现在提一个实际编程中的常见问题来展示依值类型的实际作用, API的设计者可能对此感兴趣.

假如你在使用一个比较复杂的API, 比如 OpenGL, 在你开始在屏幕上画图之前需要做很多初始化工作, 比如初始化缓冲区, 初始化顶点数据等等, 如果在初始化上做错了些步骤, 编译器不会抱怨, 但却会在运行时产生令人迷惑的错误. 如果我们想让编译器检查这类错误该怎么办呢? 下面通过一个例子展示依值类型是如何解决这个问题的, 这个例子修改自 "Type-driven Development with Idris (Edwin Brady)".

考虑有一扇门, 门有三种状态, 开着, 关着(未锁), 锁着. 然后你可以对门做一系列操作, 比如开, 关, 开锁, 上锁. 有一些操作是不合理的, 比如试图打开一个开着的门. 我们可以定义如下的类型来描述一个对门的操作

structure Key where
  user : String

inductive DoorState where 
  | SOpen (key : Key) | SClosed (key : Key) | SLocked
open DoorState

inductive DoorCmd : (before after : DoorState) -> Type _ → Type _ where
  | Open   : DoorCmd (SClosed key) (SOpen key) Unit
  | Close  : DoorCmd (SOpen key) (SClosed key) Unit
  | Lock   : DoorCmd (SClosed key) SLocked Unit
  | Unlock : (key : Key) → DoorCmd SLocked (SClosed key) Unit
  | GenKey : String → DoorCmd α α Key
  | pure   : α → DoorCmd β β α
  | bind   : DoorCmd α β T → (T → DoorCmd β γ S) → DoorCmd α γ S
open DoorCmd

其中参数 key 表示插在门上的钥匙.

DoorCmd before after α 表示一个关于门的过程, 这个过程要求起始状态为 before, 并且完成过程之后的状态为 after, 然后这个过程可以有返回值, 其类型在这里记作 α. 这个类型的前几个构造器是基本的对门的操作, 剩下的两个构造器, 一个称为 pure, 它的作用是把一个值包装成一个返回这个值的过程, bind 可以用来连接两个过程, 其中第一个过程的返回结果可以在第二个过程中出现(这是类型参数 T 的作用).

熟悉 Haskell 的人可以认出来我们实际在写 Free Monad, 软件工程人能看出来我们在试图捏一个 EDLS, 但一般语言里的 EDLS 没法保证我们这里所谓的语序安全(实际上 Haskell 可以用一些非常的技巧做到这点).

我们可以组合一个过程

def proc : DoorCmd SLocked SLocked Unit :=
  bind (GenKey "admin") fun key =>
  bind (Unlock key) fun _ =>
  bind Open  fun _ =>
  bind Close fun _ =>
  bind Lock  fun _ =>
  pure ()

这个过程可以理解作: "一个人使用'admin'作为名字申请了一个钥匙, 用它开了锁, 然后打开了门, 又关上了门, 最后锁上了门",我们看一下如果他忘记了关门而直接在开门后锁门会发生什么,

def proc : DoorCmd SLocked SLocked Unit :=
  bind (GenKey "admin") fun key =>
  bind (Unlock key) fun _ =>
  bind Open fun _ =>
  bind Lock fun _ =>
  pure ()

-- application type mismatch
--   DoorCmd.bind Lock
-- argument
--   Lock
-- has type
--   DoorCmd (SClosed ?m.21251) SLocked Unit : Type 1
-- but is expected to have type
--   DoorCmd (SOpen key) ?m.21247 ?m.21248 : Type 1

Lean 提示了如上注释中的错误, 这个错误提示告诉我们: Lock 是一个从关着的门到锁着的门的一个过程, 但这里需要的是一个从开着的门到某个状态的过程.

这只是我们要做的事情的一半, 另一半是要去执行这个过程, 我们可以定义一个输出执行器:

def interpret : DoorCmd α β T → IO T
| Open (key := key) => IO.println s!"Door opened with {key.user}'s key."
| Close => IO.println "Door closed."
| Lock => IO.println "Door locked."
| Unlock ⟨ user ⟩ => IO.println s!"Door unlocked by {user}."
| GenKey user => do
    IO.println s!"Generated a key for {user}."
    return (Key.mk user);
| DoorCmd.pure x => do return x
| DoorCmd.bind m f => do
    let x <- interpret m
    interpret (f x)

这个解释器可以把每一步的过程打印出来

#eval interpret proc
-- print:
--  Generated a key for admin.
--  Door unlocked by admin.
--  Door opened with admin's key.
--  Door closed.
--  Door locked.

如果你是在写一个类型安全的 OpenGL API包装, 那你就要为你的 API 设计一个状态类型, 然后考虑如何构造每一个过程, 并把你的 interpret 函数和实际的底层操作联系起来.

实际上 Lean4 有极强的宏功能, 我们可以通过自定义语法让我们的 EDSL 用起来更舒服

notation "let " e " <- " exp "in" other => DoorCmd.bind exp (fun e => other)
notation e1 ";" e2 => (let _ <- e1 in e2)
notation e ";" => e ; pure ()

def proc' : DoorCmd SLocked SLocked Unit :=
  let key <- GenKey "admin" in
  Unlock key;
  Open;
  Close;
  Lock;

Lean 的宏非常强大, Lean 的 if, while, do, 等等语句, 甚至包含改变运算级的小括号都不是 Lean 语言本身的一部分, 而是用宏实现的.

这种通过类型系统保证顺序安全的API其实更适合调库侠使用.

Lean4 是一个定理证明器

Lean4 可以用来表达和证明数学命题, 这是 Lean 的初衷, 即, 用来严格地验证数学定理. 它拥有一个庞大的数学定理库 Mathlib, 并已在数学界发挥了作用. 作为定理证明器的 Lean 不在本文介绍范围内, 请参见 https://lean-lang.org/theorem_proving_in_lean4/.

结

如果读者对这款新的编程语言感兴趣, 这里有一本详细介绍 Lean4 的编程语言特性的在线教程 https://lean-lang.org/functional_programming_in_lean/, 它包含了本文没有介绍的内容, 比如类型类(Rust 和 Scala 用户会叫它 Trait) 和单子及其变换, 还有关于依值类型的更多细节的用途.

由于刚刚起步, Lean作为编程语言的生态很差, 但是正如一位伟人说的那样，面包会有的，牛奶会有的，一切都会有的.