ハイスコア

説明

ゲームプレイヤーのハイスコアリストを管理します。

古典的なアーケードゲームであるFroggerのハイスコアを扱うコンポーネントを作ることが課題です。Froggerは、史上最も売れた、そして最も中毒性の高いゲームのひとつであり、アーケード時代の名作です。 さらに、リストから最高スコア、最後に追加されたスコア、上位3つのスコアを返すメソッドを書くことも課題です。

この演習では、リストと配列を扱います。 どちらもLeanにおいて非常に重要なデータ構造です。

リスト

ほとんどの関数型言語と同様に、リストはLeanの基本的なデータ構造です。

リストには2つのコンストラクタがあります。1つは空のリスト（[]）用で、もう1つは1つの要素（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はこの欠点を軽減するために参照カウントを使用しています。 配列への参照が常に1つ以下である限り（つまり、_線形_に使用されている場合）、コピーは行われず、更新を破壊的に実行できます。

ArrayAPIの多くの関数は、共有されていないデータの場合に破壊的な更新を行います。例えば、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