最高分

說明

管理遊戲玩家的高分陣列。

你的任務是為經典遊戲《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 記法只能用在單子裡面。 若想撰寫保持純粹、沒有可觀察副作用的命令式風格程式碼，一個方便的作法是使用恆等單子：

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