6260 notes: option

5 minute read Published: 2026-08-17

8.17

polymorphic-lists.dfy

datatype List1<T> = Single(T) | Cons1(hd: T, tl: List1<T>)

function singleton<T>(v: T): List1<T>
{ // you would never call singleton when you could just write Single(v) anyway
                                                                 
  Single(v)
}

function SquareFirst(v: List1<int>): int
{
  match v
  case Single(n) => n * n
  case Cons1(hd, _) => hd * hd            //功能: 取列表第一个元素, 平方
}

// what about a function to return the **last** element of a List1

一个 List1 要么是 Single(某个元素), 要么是 Cons1(头, 剩下的列表)

注意 tl 的类型又是 List1<T>, 自己引用自己, 靠 Single 这个终点兜底。

所以列表 [1,2,3] 在这个定义下长这样:

Cons1(1, Cons1(2, Single(3)))

读法: "1 接在(2 接在(只有3)前面)前面" 像套娃, 剥开最外层是1, 剩下的还是一条列表, 再剥是2, 最后剥到 Single(3), 到底了。

细节: 文件名里的1和类型名 List1 不是随便起的, 教科书式的列表通常是 Nil | Cons(_) 允许空列表, 这个版本最小单位是 Single(T), 也就是说 List1 至少有一个元素, 不可能为空。

function len<T>(v: List1<T>): nat          //ensures len(v) >= 1
{
  match v          //用到才起名, 用不到写 _
  case Single(_) => 1
  case Cons1(_, tl) => 1 + len(tl)
}

SquareFirst函数

List1<int>: 泛型被填成了具体的 int, 所以这个函数只吃整数列表。

match v: 分情况。列表只有两种可能, 所以两个 case, 一个都不能少。

case Single(n) ⇒ n * n, 如果 v 是单元素列表, 就把里面那个元素起名叫 n。然后返回 n * n。这个拆开并起名的动作叫模式匹配。

case Cons1(hd, _) ⇒ hd * hd: 如果是多元素列表, 把头起名叫 hd, 下划线 _ 的意思是"这个位置有东西(尾巴)", 但我不关心它, 懒得给起名。

注意这个函数没有递归, 第一个元素伸手就够得着, 拆一层就拿到了, 不需要往深处走。

为什么 the last 就难了:

最后一个元素埋在套娃的最里面, 必须一层一层剥进去。而一层一层往里走就是递归。

逻辑:

如果列表是 Single(n)。只有一个元素, 也是最后一个。直接返回 n。
如果列表是 Cons1(hd, tl)。最后一个元素藏在 tl 里, 那在 tl 里找最后一个。这就是同一个问题、换了条更短的列表 —— 调自己。

function last<T>(v: List1<T>): T
{
  match v
  case Single(x) => x
  case Cons1(_, tl) => last(tl)
}

区别是这次不关心头, (_换了位置), 并在第二个 case 里自己调自己。每调一次, 列表短一截。最终必然撞上 Single, 递归停下。

tree-recursion.dfy

1  datatype option<V> = None | Some(V)
2  datatype tree<V> = Lf
3    | Node(k: string, v: V, left: tree<V>, right: tree<V>)

function lookup<V>(t: tree<V>, key: string): option<V>

function insert<V>(t: tree<V>, key: string, value: V): tree<V>

function sz<T>(t: tree<T>): nat

// lemmas?

datatype 是定义"新类型"的方式。读法是, "一个 option<V> 类型的值, 要么是 None, 要么是 Some(V), 没有第三种可能"

把它想象成一个盒子: None 是空盒子, Some(v) 是装了一个东西 v 的盒子, <V> 是泛型参数, 盒子里装什么类型都行。option<int> 装整数, option<string> 装字符串。

为什么需要这个盒子? lookup 去树里找一个 key, 可能找不到。找不到时返回什么? Dafny 的做法是把"可能失败"写进类型里。找到了返回 Some(值), 没找到返回 None, 编译器强迫调用者两种情况都处理。

2-3 行: 树的定义

"一棵树要么是 Lf(Leaf, 空树)。要么是一个 Node(节点)"

一个节点带4样东西: k: 一个字符串 key(这棵树是当字典用的, key 定死为 string)
                  v: 这个 key 对应的值, 类型是泛型 V
                  left、right: 又是两棵树, 左子树和右子树。

注意这个定义是递归的, 树的定义里出现了树自己。这不是循环论证, 因为有 Lf 这个"终点"兜底。任何一棵具体的树, 往下拆, 拆到底一定全是 Lf。

三个空签名:

这三个函数合起来就是一个字典的最小接口:

function lookup<V>(t: tree<V>, key: string): option<V>
{
  match t
  case Lf => None                                     // 空树里什么也查不到
  case Node(k, v, l, r) =>
    if key == k then Some(v)                          //小v, 和 Some(V) 还不一样, 这是树的 v
    else if key < k then lookup(l, key)               // 比当前 key 小 → 去左边找
    else lookup(r, key)                               // 否则去右边找
}

我写的:

function insert<V>(t: tree<V>, key: string, value: V): tree<V>
{
  match t
  case Lf => None
  case Node(k, v, l, r) => Node(k, v, insert(l, key, value), insert(r, key, value))
}

每个 key 只能出现一次

小的在左, 大的在右。

insert 和 lookup 是同一条路。先比较, 选一边, 另一边看都不看。

case Node(k, v, l, r) =>
  if key == k then Node(k, value, l, r)                         // 撞名, 原位换 value, 子树不动
  else if key < k then Node(k, v, insert(l, key, value), r)     // 往左送, 右不动
  else Node(k, v, l, insert(r, key, value))                     // 往右送, 左不动。

insert 的雇主是未来的 lookup
每个岔口的选择都被比大小结果锁死

lemma insertlookup<V>(t: tree<V>, key: string, value: V)
   ensures lookup(insert(t, key, value), key) == Some(value)
{}

ensures里嵌套调用，先insert出一棵新树，再在新树上lookup，右边是Some(value)，option在这里登场，“必然找到”就写成“不是None，而是Some，且盒子里装的是当初存的货。”