최고 점수

지침

게임 플레이어의 최고 점수 목록을 관리해요.

이번 과제는 역사상 가장 많이 팔린, 가장 중독성 있는 게임 중 하나이자 아케이드 시대의 고전인 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