Lean 표준 라이브러리에는 List라는 표준 연결 리스트 데이터 타입과 이를 편리하게 사용하는 특별한 문법이 있다. 목록은 대괄호로 쓴다. 예를 들어 10보다 작은 소수를 포함하는 목록은 다음과 같이 쓸 수 있다:

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

이면에서 List는 다음과 같이 정의된 귀납적 데이터 타입이다:

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

표준 라이브러리의 실제 정의는 아직 소개하지 않은 기능을 사용하므로 조금 다르지만 본질적으로 비슷하다. 이 정의는 List가 PPoint와 마찬가지로 하나의 타입을 인수로 받는다는 뜻이다. 이 타입은 목록에 저장되는 원소의 타입이다. 생성자에 따르면 List α는 nil이나 cons로 만들 수 있다. nil 생성자는 빈 목록을 나타내고 cons 생성자는 비어 있지 않은 목록에 사용한다. cons의 첫 번째 인수는 목록의 머리이고 두 번째 인수는 꼬리다. n개의 원소를 가진 목록에는 n개의 cons 생성자가 있으며, 마지막 생성자의 꼬리는 nil이다.

List의 생성자를 직접 사용하면 primesUnder10 예제를 더 명시적으로 쓸 수 있다:

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라고 부르므로, 구조체 필드에 사용하는 점 표기로 목록의 길이도 구할 수 있다:

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의 메커니즘이 입력값과 재귀 호출의 인수 사이 연결을 볼 수 없다. 예를 들어 두 목록의 길이가 같은지 결정하는 다음 함수는 거부된다:

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에 특정 표시 코드를 제공할 필요가 없다:

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의 표시 코드가 이미 존재해야 한다고 요구한다. 정의의 끝에서 #eval의 일부로 표시 코드를 생성하게 하는 대신 데이터 타입을 정의할 때 이 코드를 생성하도록 Lean에 지시하면 이 오류를 우회할 수 있다. 정의에 deriving Repr를 추가하면 된다:

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]