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의 첫 번째 인자는 리스트의 머리이고, 두 번째 인자는 그 꼬리입니다. 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 }

natOrigin과 함께 사용할 때 Nat을 명시적으로 제공하지 않아도 되는데, 이는 Lean이 이후 인자들로부터 α의 값을 추론할 수 있기 때문입니다:

{ 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의 메커니즘이 입력 값과 재귀 호출의 인자 사이의 연관성을 파악하지 못합니다. 예를 들어, 두 리스트의 길이가 같은지 판단하는 다음 함수는 거부됩니다:

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에 대한 표시 코드가 이미 존재할 것을 요구하기 때문입니다. 이 오류는, #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]