高分榜

说明

管理游戏玩家的最高分列表。

你的任务是为经典游戏 Frogger 构建一个最高分组件。Frogger 是有史以来最畅销、最容易让人上瘾的游戏之一，也是街机时代的经典之作。 你的任务是编写方法，返回数组中的最高分、最后添加的分数和三个最高分。

在这个练习中，你将用到列表和数组。它们都是 Lean 中非常重要的数据结构。

列表

和大多数函数式语言一样，列表 是 Lean 中一种基础的数据结构。

列表有两种构造函数，一种构造空列表（[]），另一种构造包含一个元素（head）和另一个列表（tail）的列表。 可以用 :: 把元素添加到列表前面，从而创建出一个新列表：

let list := x :: xs -- prepending x to xs creates a new list where x is the head and xs is the tail

列表本质上是递归的，因此非常适合用于归纳推理。 列表还支持结构共享：你可以把一个新元素添加到列表前面，而不必复制现有的列表：

let list1 := [1, 2]
let list2 := 0 :: list1
-- now both list1 and list2 share [1, 2]

不过，列表上的大多数操作耗时都与列表的长度成正比，因为要到达下一个元素，必须逐个遍历每个元素。

数组

数组 是一块大小可动态变化的连续内存。

在很多操作上，数组都比列表高效得多：

1. 访问数组中的任何元素都很快，耗时是常数时间。
2. 数组以动态数组为蓝本，而动态数组在现代系统上往往特别高效，这得益于缓存局部性。

不过，数组对结构共享并不友好。 一般来说，在函数式环境下更新数组需要复制整个现有数组。

Lean 使用引用计数来缓解这一缺点。 只要一个数组的引用始终不超过一个（也就是说，它是_线性地_使用的），就不会发生复制，更新也可以破坏性地进行。

Array API 中的很多函数在数据未被共享时会执行破坏性更新，例如 set 和 push。

do 记法

Lean 支持 do 记法，这是一种用于以命令式风格编写代码的内嵌语言。

在 do 块中，可以使用 mut 关键字声明可重新赋值的可变局部变量。 当与数组这样的数据结构一起使用时，这让 Lean 的运行时系统能在安全的时候，在底层执行原地破坏性更新。

do 记法只能在单子内部使用。 要想以一种方便的方式编写命令式风格的代码，同时保持纯、没有可观察的副作用，可以使用 Identity 单子：

def sumArray (array : Array Nat) := Id.run do
    let mut sum := 0
    for element in array do
        sum := sum + element
    return sum