Lean 표준 라이브러리에는 List라는 표준 연결 리스트 데이터 타입과 이를 더 편리하게 사용할 수 있게 해 주는 특별한 문법이 포함되어 있습니다. 리스트는 대괄호로 감싸서 작성합니다. 예를 들어, 10보다 작은 소수들을 담은 리스트는 다음과 같이 작성할 수 있습니다:

def primesUnder10 : List Nat := [2, 3, 5, 7]

내부적으로 List는 다음과 같이 정의된 귀납적 데이터 타입입니다:

inductive List (α : Type) where | nil : List α | cons : α → List α → List α

표준 라이브러리의 실제 정의는 아직 소개하지 않은 기능을 사용하기 때문에 조금 다르지만, 본질적으로는 비슷합니다. 이 정의는 PPoint와 마찬가지로 List가 하나의 타입을 인자로 받는다는 것을 나타냅니다. 이 타입은 리스트에 저장되는 항목의 타입입니다. 생성자에 따르면 List α는 nil이나 cons 중 하나로 만들 수 있습니다. 생성자 nil은 빈 리스트를 나타내고, 생성자 cons는 비어 있지 않은 리스트에 사용됩니다. cons의 첫 번째 인자는 리스트의 머리(head)이고, 두 번째 인자는 꼬리(tail)입니다. n개의 항목을 담은 리스트에는 n개의 cons 생성자가 들어 있으며, 그중 마지막 생성자는 nil을 꼬리로 가집니다.

primesUnder10 예제는 List의 생성자를 직접 사용하여 더 명시적으로 작성할 수 있습니다:

def explicitPrimesUnder10 : List Nat := List.cons 2 (List.cons 3 (List.cons 5 (List.cons 7 List.nil)))

이 두 정의는 완전히 동등하지만, primesUnder10이 explicitPrimesUnder10보다 훨씬 읽기 쉽습니다.

List를 입력으로 받는 함수는 Nat을 입력으로 받는 함수와 거의 같은 방식으로 정의할 수 있습니다. 실제로 연결 리스트는 각 succ 생성자마다 추가 데이터 필드가 하나씩 매달려 있는 Nat으로 생각할 수 있습니다. 이 관점에서 보면, 리스트의 길이를 계산하는 것은 각 cons를 succ로, 마지막 nil을 zero로 바꾸는 과정입니다. replaceX가 점의 필드 타입을 인자로 받았던 것처럼, length는 리스트 원소의 타입을 인자로 받습니다. 예를 들어 리스트에 문자열이 들어 있다면 첫 번째 인자는 String입니다: length String ["Sourdough", "bread"]. 이는 다음과 같이 계산되어야 합니다:

length의 정의는 리스트 항목의 타입을 인자로 받으므로 다형적이며, 자기 자신을 참조하므로 재귀적이기도 합니다. 일반적으로 함수는 데이터의 형태를 따릅니다. 재귀적 데이터 타입에서는 재귀 함수가, 다형적 데이터 타입에서는 다형 함수가 나옵니다.

def length (α : Type) (xs : List α) : Nat := match xs with | List.nil => Nat.zero | List.cons y ys => Nat.succ (length α ys)

리스트를 다루는 함수를 더 읽기 쉽게 작성할 수 있도록, 대괄호 표기법 []를 사용하여 nil에 대해 패턴 매칭할 수 있고, cons 대신 중위 연산자 ::를 사용할 수 있습니다:

def length (α : Type) (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length α ys)

replaceX와 length는 둘 다 사용하기가 다소 번거롭습니다. 타입 인자는 대개 뒤에 오는 값들에 의해 유일하게 결정되기 때문입니다. 실제로 대부분의 언어에서 컴파일러는 타입 인자를 스스로 충분히 결정할 수 있으며, 사용자의 도움이 필요한 경우는 가끔뿐입니다. 이는 Lean에서도 마찬가지입니다. 함수를 정의할 때 인자를 소괄호 대신 중괄호로 감싸면 암시적으로 선언할 수 있습니다. 예를 들어, 암시적 타입 인자를 사용하는 replaceX는 다음과 같습니다:

def replaceX {α : Type} (point : PPoint α) (newX : α) : PPoint α := { point with x := newX }

Lean은 뒤따르는 인자들로부터 α의 값을 추론할 수 있으므로, Nat을 명시적으로 제공하지 않고도 natOrigin과 함께 사용할 수 있습니다:

{ x := 5, y := 0 }#eval replaceX natOrigin 5

{ x := 5, y := 0 }

마찬가지로, length도 항목 타입을 암묵적으로 받도록 다시 정의할 수 있습니다:

def length {α : Type} (xs : List α) : Nat := match xs with | [] => 0 | y :: ys => Nat.succ (length ys)

이 length 함수는 primesUnder10에 바로 적용할 수 있습니다:

4#eval length primesUnder10

4

표준 라이브러리에서 Lean은 이 함수를 List.length라고 부릅니다. 즉, 구조체 필드에 접근할 때 쓰는 점(dot) 문법으로 리스트의 길이도 구할 수 있습니다:

4#eval primesUnder10.length

4

C#과 Java에서 때때로 타입 인자를 명시적으로 제공해야 하는 것처럼, Lean도 암시적 인자를 항상 찾아낼 수 있는 것은 아닙니다. 이러한 경우에는 인자의 이름을 사용하여 제공할 수 있습니다. 예를 들어, 정수 리스트에만 동작하는 List.length 버전은 α를 Int로 설정하여 지정할 수 있습니다:

List.length : List Int → Nat#check List.length (α := Int)

List.length : List Int → Nat

정의할 수 있는 구조체나 귀납적 타입이 모두 Type 타입을 가질 수 있는 것은 아닙니다. 특히 생성자가 임의의 타입을 인자로 받는다면, 그 귀납적 타입은 다른 타입을 가져야 합니다. 이러한 오류는 대개 “유니버스 레벨”에 관한 내용을 언급합니다. 예를 들어, 다음 귀납적 타입을 봅시다:

inductive MyType : Type where Invalid universe level in constructor `MyType.ctor`: Parameter `α` has type Type at universe level 2 which is not less than or equal to the inductive type's resulting universe level 1| ctor : (α : Type) → α → MyType

Lean은 다음과 같은 오류를 표시합니다:

Invalid universe level in constructor `MyType.ctor`: Parameter `α` has type
  Type
at universe level
  2
which is not less than or equal to the inductive type's resulting universe level
  1

그 이유와 정의를 어떻게 수정해야 제대로 동작하는지는 이후의 장에서 설명합니다. 지금은 타입을 생성자의 인자가 아니라 귀납적 타입 전체의 인자로 만들어 보십시오.

마찬가지로, 생성자의 인자가 현재 정의 중인 데이터 타입을 인자로 받는 함수이면 그 정의는 거부됩니다. 예를 들면 다음과 같습니다.

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declaredinductive MyType : Type where | ctor : (MyType → Int) → MyType

다음 메시지를 출력합니다:

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared

기술적인 이유로, 이러한 데이터 타입을 허용하면 Lean의 내부 논리를 무너뜨릴 수 있게 되어 Lean을 정리 증명기로 사용하기에 적합하지 않게 될 수 있습니다.

매개변수를 두 개 받는 재귀 함수는 두 매개변수를 쌍으로 묶어 매칭하지 말고, 각 매개변수를 독립적으로 매칭해야 합니다. 그렇지 않으면 재귀 호출이 더 작은 값에 대해 이루어지는지 검사하는 Lean의 메커니즘이 입력값과 재귀 호출의 인자 사이의 연관성을 파악하지 못합니다. 예를 들어, 두 리스트의 길이가 같은지 판별하는 다음 함수는 거부됩니다:

def fail to show termination for sameLength with errors failed to infer structural recursion: Not considering parameter α of sameLength: it is unchanged in the recursive calls Not considering parameter β of sameLength: it is unchanged in the recursive calls Cannot use parameter xs: failed to eliminate recursive application sameLength xs' ys' Cannot use parameter ys: failed to eliminate recursive application sameLength xs' ys' Could not find a decreasing measure. The basic measures relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) xs ys 1) 1816:28-46 ? ? Please use `termination_by` to specify a decreasing measure.sameLength (xs : List α) (ys : List β) : Bool := match (xs, ys) with | ([], []) => true | (x :: xs', y :: ys') => sameLength xs' ys' | _ => false

오류 메시지는 다음과 같습니다:

fail to show termination for
  sameLength
with errors
failed to infer structural recursion:
Not considering parameter α of sameLength:
  it is unchanged in the recursive calls
Not considering parameter β of sameLength:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    sameLength xs' ys'
Cannot use parameter ys:
  failed to eliminate recursive application
    sameLength xs' ys'


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              xs ys
1) 1816:28-46  ?  ?
Please use `termination_by` to specify a decreasing measure.

이 문제는 중첩 패턴 매칭으로 해결할 수 있습니다:

def sameLength (xs : List α) (ys : List β) : Bool := match xs with | [] => match ys with | [] => true | _ => false | x :: xs' => match ys with | y :: ys' => sameLength xs' ys' | _ => false

다음 절에서 설명할 동시 매칭은 이 문제를 해결하는 또 다른 방법이며, 대개 더 우아합니다.

귀납적 타입에 인자를 빠뜨려도 혼란스러운 메시지가 나올 수 있습니다. 예를 들어, ctor의 타입에서 MyType에 인자 α를 전달하지 않으면 다음과 같습니다:

inductive MyType (α : Type) : Type where | ctor : α → type expected, got (MyType : Type → Type)MyType

Lean은 다음과 같은 오류를 출력합니다:

type expected, got
  (MyType : Type → Type)

이 오류 메시지는 MyType의 타입인 Type → Type은 그 자체로는 타입을 기술하지 않는다는 뜻입니다. MyType이 진짜 제대로 된 타입이 되려면 인자가 필요합니다.

정의의 타입 시그니처와 같이 다른 맥락에서 타입 인자를 생략한 경우에도 같은 메시지가 나타날 수 있습니다:

inductive MyType (α : Type) : Type where | ctor : α → MyType αdef ofFive : type expected, got (MyType : Type → Type)MyType := ctor 5

type expected, got
  (MyType : Type → Type)

다형 타입을 사용하는 표현식을 평가하면 Lean이 값을 표시할 수 없는 상황이 생길 수 있습니다. #eval 명령은 주어진 표현식을 평가하며, 결과를 어떻게 표시할지 결정할 때 그 표현식의 타입을 사용합니다. 함수와 같은 일부 타입에서는 이 과정이 실패하지만, 그 밖의 대부분의 타입에 대해서는 Lean이 표시 코드를 충분히 자동으로 생성할 수 있습니다. 예를 들어, WoodSplittingTool을 위한 별도의 표시 코드를 Lean에 제공할 필요가 없습니다:

inductive WoodSplittingTool where | axe | maul | froeWoodSplittingTool.axe#eval WoodSplittingTool.axe

WoodSplittingTool.axe

하지만 여기서 Lean이 사용하는 자동화에는 한계가 있습니다. allTools는 세 가지 도구를 모두 담은 리스트입니다:

def allTools : List WoodSplittingTool := [ WoodSplittingTool.axe, WoodSplittingTool.maul, WoodSplittingTool.froe ]

이를 평가하면 오류가 발생합니다:

Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type List WoodSplittingTool#eval allTools

Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
  List WoodSplittingTool

이는 Lean이 리스트를 표시하기 위해 내장 테이블에 있는 코드를 사용하려 하는데, 이 코드는 WoodSplittingTool을 표시하는 코드가 이미 존재해야 하기 때문입니다. 이 오류는 데이터 타입의 정의에 deriving Repr를 추가하여 우회할 수 있습니다. 이렇게 하면 Lean은 #eval의 일부로 마지막 순간에 표시 코드를 생성하는 대신, 데이터 타입이 정의될 때 표시 코드를 생성합니다:

inductive Firewood where | birch | pine | beech deriving Repr

Firewood의 리스트를 평가하면 성공합니다:

def allFirewood : List Firewood := [ Firewood.birch, Firewood.pine, Firewood.beech ][Firewood.birch, Firewood.pine, Firewood.beech]#eval allFirewood

[Firewood.birch, Firewood.pine, Firewood.beech]