Bestenliste

Anleitung

Verwalte die Highscore-Liste eines Spielers.

Deine Aufgabe ist es, eine Highscore-Komponente für das klassische Spiel Frogger zu bauen, eines der meistverkauften und süchtig machendsten Spiele aller Zeiten und ein Klassiker der Arcade-Ära. Deine Aufgabe ist es, Methoden zu schreiben, die die höchste Punktzahl aus der Liste, die zuletzt hinzugefügte Punktzahl und die drei höchsten Punktzahlen zurückgeben.

In dieser Übung arbeitest du mit Listen und Arrays. Beides sind sehr wichtige Datenstrukturen in Lean.

Listen

Wie in den meisten funktionalen Sprachen sind Listen eine grundlegende Datenstruktur in Lean.

Eine Liste hat zwei Konstruktoren: einen für die leere Liste ([]) und einen für eine Liste, die ein Element (den head) und eine weitere Liste (den tail) enthält. Mit :: kannst du Elemente an den Anfang einer Liste setzen und so eine neue Liste erzeugen:

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

Listen sind von Natur aus rekursiv, was sie besonders für induktives Schließen geeignet macht. Außerdem unterstützen sie strukturelles Teilen: Du kannst ein neues Element an den Anfang einer Liste setzen, ohne die bestehende Liste zu kopieren:

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

Die meisten Operationen auf Listen dauern jedoch proportional zu ihrer Länge, da jedes Element durchlaufen werden muss, um zum nächsten zu gelangen.

Arrays

Ein Array ist ein zusammenhängender Speicherblock, dessen Größe sich dynamisch ändert.

Für viele Operationen sind Arrays deutlich effizienter als Listen:

1. Der Zugriff auf ein beliebiges Element in einem Array ist schnell und läuft in konstanter Zeit.
2. Arrays sind dynamischen Arrays nachempfunden, die auf modernen Systemen wegen der Cache-Lokalität besonders effizient sind.

Allerdings sind Arrays für strukturelles Teilen wenig geeignet. Im Allgemeinen erfordert das Aktualisieren eines Arrays in einem funktionalen Umfeld das Kopieren des gesamten bestehenden Arrays.

Lean verwendet Referenzzählung, um diesen Nachteil abzumildern. Solange es nie mehr als eine Referenz auf ein Array gibt (das heißt, es wird linear verwendet), wird nichts kopiert und Aktualisierungen können destruktiv ausgeführt werden.

Viele Funktionen in der Array-API führen bei nicht geteilten Daten destruktive Aktualisierungen durch, zum Beispiel set und push.

Do-Notation

Lean unterstützt die Do-Notation, eine eingebettete Sprache, um Code in einem imperativen Stil zu schreiben.

Innerhalb eines do-Blocks kannst du mit dem Schlüsselwort mut veränderliche lokale Variablen deklarieren, die neu zugewiesen werden können. In Kombination mit Datenstrukturen wie Arrays ermöglicht das dem Laufzeitsystem von Lean, im Hintergrund destruktive Aktualisierungen an Ort und Stelle durchzuführen, wann immer das gefahrlos möglich ist.

Do-Notation kann nur innerhalb einer Monade verwendet werden. Eine praktische Möglichkeit, Code im imperativen Stil zu schreiben, der rein bleibt und keine beobachtbaren Seiteneffekte hat, ist die Identity-Monade:

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