1. Lean 알아보기

전통적으로 프로그래밍 언어는 콘솔에 "Hello, world!"를 출력하는 프로그램을 컴파일하고 실행함으로써 소개되곤 합니다. 이 간단한 프로그램은 언어 도구가 올바르게 설치되었는지, 그리고 프로그래머가 컴파일된 코드를 실행할 수 있는지를 확인해 줍니다.

하지만 1970년대 이후로 프로그래밍은 변화해 왔습니다. 오늘날 컴파일러는 대개 텍스트 에디터에 통합되어 있으며, 프로그래밍 환경은 프로그램을 작성하는 동안 피드백을 제공합니다. Lean도 예외는 아닙니다. Lean은 언어 서버 프로토콜 의 확장 버전을 구현하여 텍스트 에디터와 통신하고 사용자가 입력하는 동안 피드백을 제공할 수 있도록 합니다.

Python, Haskell, JavaScript와 같이 다양한 언어들은 표현식이나 문장을 입력할 수 있는 REPL, 즉 대화형 톱레벨이나 브라우저 콘솔을 제공합니다. 그러면 언어는 사용자의 입력 결과를 계산하여 표시합니다. 반면 Lean은 이러한 기능들을 에디터와의 상호작용에 통합하여, 텍스트 에디터가 프로그램 텍스트 자체에 통합된 피드백을 표시하도록 하는 명령어를 제공합니다. 이 장에서는 에디터에서 Lean과 상호작용하는 방법을 짧게 소개하며, Hello, World! 장에서는 명령줄에서 배치 모드로 Lean을 사용하는 전통적인 방법을 설명합니다.

에디터에 Lean을 띄워 놓고 각 예제를 직접 입력하며 이 책을 읽는 것이 가장 좋습니다. 예제들을 직접 다루어 보며 어떤 일이 일어나는지 확인해 보세요!

1.1. 표현식 평가하기

Lean을 배우는 프로그래머로서 이해해야 할 가장 중요한 것은 평가가 어떻게 작동하는지입니다. 평가는 산수에서처럼 표현식의 값을 찾는 과정입니다. 예를 들어, 15−615−6의 값은 99이고 2×(3+1)2×(3+1)의 값은 88입니다. 후자의 표현식 값을 찾기 위해, 3+13+1은 먼저 44로 대체되어 2×42×4가 되고, 이는 다시 88로 줄어들 수 있습니다. 때때로 수학적 표현식에는 변수가 포함됩니다. x+1x+1의 값은 xx의 값을 알기 전까지는 계산할 수 없습니다. Lean에서 프로그램은 무엇보다도 표현식이며, 계산에 대해 생각하는 주된 방식은 표현식을 평가하여 그 값을 찾는 것입니다.

대부분의 프로그래밍 언어는 명령형으로, 프로그램은 결과를 찾기 위해 수행되어야 할 일련의 문장들로 구성됩니다. 프로그램은 변경 가능한 메모리에 접근할 수 있으므로, 변수가 참조하는 값은 시간이 지남에 따라 변할 수 있습니다. 변경 가능한 상태 외에도, 프로그램은 파일 삭제, 외부 네트워크 연결, 예외 발생 또는 처리, 데이터베이스에서 데이터 읽기와 같은 다른 부작용을 가질 수 있습니다. "부작용"은 본질적으로 수학적 표현식을 평가하는 모델을 따르지 않는 프로그램에서 일어날 수 있는 일들을 설명하는 포괄적인 용어입니다.

하지만 Lean에서는 프로그램이 수학적 표현식과 동일한 방식으로 작동합니다. 일단 값이 주어지면 변수는 재할당될 수 없습니다. 표현식을 평가하는 것은 부작용을 가질 수 없습니다. 두 표현식이 같은 값을 가지면, 하나를 다른 것으로 대체해도 프로그램이 다른 결과를 계산하게 하지 않습니다. 이것이 Lean으로 콘솔에 Hello, world!를 출력하는 프로그램을 작성할 수 없다는 의미는 아니지만, 입출력을 수행하는 것은 Lean을 사용하는 경험의 핵심적인 부분은 아닙니다. 따라서 이 장에서는 Lean으로 표현식을 대화식으로 평가하는 방법에 초점을 맞추고, 다음 장에서는 Hello, world! 프로그램을 작성, 컴파일 및 실행하는 방법을 설명합니다.

Lean에게 표현식을 평가하도록 요청하려면, 편집기에서 그 앞에 #eval을 작성하면 결과가 다시 보고됩니다. 일반적으로 결과는 #eval 위에 커서나 마우스 포인터를 올려놓으면 찾을 수 있습니다. 예를 들어,

#eval 1 + 2

는 다음 값을 산출합니다.

3

Lean은 산술 연산자에 대한 일반적인 우선순위 및 결합성 규칙을 따릅니다. 즉,

#eval 1 + 2 * 5

는 15가 아닌 11이라는 값을 산출합니다.

일반적인 수학 표기법과 대부분의 프로그래밍 언어가 함수를 인수에 적용하기 위해 괄호(예: f(x))를 사용하는 반면, Lean은 단순히 함수를 인수 옆에 씁니다(예: f x). 함수 적용은 가장 흔한 연산 중 하나이므로 간결하게 유지하는 것이 좋습니다. "Hello, Lean!"을 계산하기 위해

#eval String.append("Hello, ", "Lean!")

라고 쓰는 대신, 다음과 같이 씁니다.

#eval String.append "Hello, " "Lean!"

여기서 함수의 두 인수는 단순히 공백으로 구분하여 옆에 씁니다.

산술의 연산 순서 규칙이 (1 + 2) * 5 표현식에서 괄호를 요구하는 것처럼, 함수의 인수가 다른 함수 호출을 통해 계산되어야 할 때도 괄호가 필요합니다. 예를 들어, 다음 표현식에서는 괄호가 필요합니다.

#eval String.append "great " (String.append "oak " "tree")

그렇지 않으면 두 번째 String.append는 "oak "와 "tree"를 인수로 받는 함수가 아니라 첫 번째 String.append의 인수로 해석될 것이기 때문입니다. 내부 String.append 호출의 값을 먼저 찾아야 하며, 그 후에 "great "에 덧붙여져 최종 값 "great oak tree"를 산출할 수 있습니다.

명령형 언어는 종종 두 종류의 조건문을 가집니다. 하나는 불리언 값에 따라 어떤 명령을 수행할지 결정하는 조건문이고, 다른 하나는 불리언 값에 따라 두 표현식 중 어느 것을 평가할지 결정하는 조건 표현식입니다. 예를 들어, C와 C++에서는 조건문이 if와 else를 사용하여 작성되는 반면, 조건 표현식은 ?와 :가 조건을 분기에서 분리하는 삼항 연산자로 작성됩니다. 파이썬에서는 조건문이 if로 시작하는 반면, 조건 표현식은 if를 중간에 둡니다. Lean은 표현식 중심의 함수형 언어이기 때문에 조건문은 없고 조건 표현식만 있습니다. 이것들은 if, then, else를 사용하여 작성됩니다. 예를 들어, String.append "it is " (if 1 > 2 then "yes" else "no")

는 다음과 같이 평가됩니다. String.append "it is " (if false then "yes" else "no")

이는 다시 다음과 같이 평가됩니다. String.append "it is " "no"

그리고 최종적으로 "it is no"로 평가됩니다.

간결함을 위해, 이와 같은 일련의 평가 단계는 때때로 화살표로 연결하여 작성될 수 있습니다. String.append "it is " (if 1 > 2 then "yes" else "no") String.append "it is " (if false then "yes" else "no") String.append "it is " "no" "it is no"

1.1.1. 마주칠 수 있는 메시지

인수가 누락된 함수 적용을 Lean에게 평가하도록 요청하면 오류 메시지가 발생합니다. 특히, 다음 예제는

#eval String.append "it is "

상당히 긴 오류 메시지를 산출합니다.

could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
  String → String

이 메시지는 Lean 함수가 일부 인수에만 적용될 때 나머지 인수를 기다리는 새로운 함수를 반환하기 때문에 발생합니다. Lean은 함수를 사용자에게 표시할 수 없으므로, 그렇게 하도록 요청받았을 때 오류를 반환합니다.

1.1.2. 연습 문제

다음 표현식들의 값은 무엇일까요? 손으로 풀어본 다음, Lean에 입력하여 답을 확인해 보세요.

• 42 + 19

• String.append "A" (String.append "B" "C")

• String.append (String.append "A" "B") "C"

• if 3 == 3 then 5 else 7

• if 3 == 4 then "equal" else "not equal"

1.2. 타입

타입은 프로그램이 계산할 수 있는 값을 기준으로 프로그램을 분류합니다. 타입은 프로그램에서 여러 역할을 수행합니다.

1. 컴파일러가 값의 메모리 내 표현에 대해 결정할 수 있게 합니다.
2. 프로그래머가 다른 사람에게 자신의 의도를 전달하는 데 도움을 주며, 함수의 입력과 출력에 대한 가벼운 명세 역할을 합니다. 컴파일러는 프로그램이 이 명세를 준수하도록 보장합니다.
3. 숫자에 문자열을 더하는 것과 같은 다양한 잠재적 실수를 방지하여 프로그램에 필요한 테스트의 수를 줄여줍니다.
4. Lean 컴파일러가 상용구 코드를 절약할 수 있는 보조 코드 생성을 자동화하는 데 도움을 줍니다.

Lean의 타입 시스템은 이례적으로 표현력이 풍부합니다. 타입은 "이 정렬 함수는 입력의 순열을 반환한다"와 같은 강력한 명세나 "이 함수는 인수의 값에 따라 다른 반환 타입을 갖는다"와 같은 유연한 명세를 인코딩할 수 있습니다. 타입 시스템은 심지어 수학적 정리를 증명하기 위한 완전한 논리로도 사용될 수 있습니다. 그러나 이러한 최첨단 표현력이 더 간단한 타입을 불필요하게 만드는 것은 아니며, 이러한 더 간단한 타입을 이해하는 것이 더 고급 기능을 사용하기 위한 전제 조건입니다.

Lean의 모든 프로그램은 타입을 가져야 합니다. 특히, 모든 표현식은 평가되기 전에 타입을 가져야 합니다. 지금까지의 예제에서는 Lean이 스스로 타입을 발견할 수 있었지만, 때로는 타입을 제공해야 할 필요가 있습니다. 이는 괄호 안에서 콜론 연산자를 사용하여 수행됩니다.

#eval (1 + 2 : Nat)

여기서 Nat은 자연수의 타입으로, 임의 정밀도의 부호 없는 정수입니다. Lean에서 Nat은 음수가 아닌 정수 리터럴의 기본 타입입니다. 이 기본 타입이 항상 최선의 선택은 아닙니다. C에서는 부호 없는 정수가 뺄셈 결과가 0보다 작아질 경우 표현 가능한 가장 큰 수로 언더플로우됩니다. 그러나 Nat은 임의로 큰 부호 없는 수를 표현할 수 있으므로 언더플로우될 가장 큰 수가 없습니다. 따라서 Nat에서의 뺄셈은 결과가 음수였을 경우 0을 반환합니다. 예를 들어,

#eval (1 - 2 : Nat)

는 -1이 아닌 0으로 평가됩니다. 음의 정수를 표현할 수 있는 타입을 사용하려면 직접 제공하십시오.

#eval (1 - 2 : Int)

이 타입을 사용하면 결과는 예상대로 -1이 됩니다.

표현식을 평가하지 않고 타입을 확인하려면 #eval 대신 #check를 사용하십시오. 예를 들어:

#check (1 - 2 : Int)

는 실제로 뺄셈을 수행하지 않고 1 - 2 : Int를 보고합니다.

프로그램에 타입을 부여할 수 없을 때는 #check와 #eval 모두에서 오류가 반환됩니다. 예를 들어:

#check String.append ["hello", " "] "world"

는 다음과 같이 출력합니다.

Application type mismatch: The argument
  ["hello", " "]
has type
  List String
but is expected to have type
  String
in the application
  String.append ["hello", " "]

String.append의 첫 번째 인수는 문자열이어야 하는데 문자열 리스트가 대신 제공되었기 때문입니다.

1.3. 함수와 정의

Lean에서는 def 키워드를 사용하여 정의를 도입합니다. 예를 들어, hello라는 이름을 문자열 "Hello"를 참조하도록 정의하려면 다음과 같이 작성합니다.

def hello := "Hello"

Lean에서는 새로운 이름을 정의할 때 = 대신 콜론-등호 연산자 :=를 사용합니다. 이는 =가 기존 표현식 간의 동등성을 설명하는 데 사용되기 때문이며, 두 개의 다른 연산자를 사용하면 혼동을 방지하는 데 도움이 됩니다.

hello의 정의에서, 표현식 "Hello"는 Lean이 정의의 타입을 자동으로 결정할 수 있을 만큼 충분히 간단합니다. 그러나 대부분의 정의는 그렇게 간단하지 않으므로, 보통 타입을 추가해야 합니다. 이는 정의되는 이름 뒤에 콜론을 사용하여 수행됩니다.

def lean : String := "Lean"

이제 이름이 정의되었으므로 사용할 수 있습니다. 따라서

#eval String.append hello (String.append " " lean)

은 다음과 같이 출력됩니다.

"Hello Lean"

Lean에서는 정의된 이름은 정의된 이후에만 사용할 수 있습니다.

많은 언어에서 함수 정의는 다른 값의 정의와 다른 구문을 사용합니다. 예를 들어, 파이썬 함수 정의는 def 키워드로 시작하는 반면, 다른 정의는 등호로 정의됩니다. Lean에서는 함수를 다른 값과 동일한 def 키워드를 사용하여 정의합니다. 그럼에도 불구하고, hello와 같은 정의는 호출될 때마다 동등한 결과를 반환하는 인수가 없는 함수가 아니라, 그 값 자체를 직접 참조하는 이름을 도입합니다.

1.3.1. 함수 정의하기

Lean에서 함수를 정의하는 방법은 다양합니다. 가장 간단한 방법은 함수의 인수를 정의의 타입 앞에 공백으로 구분하여 배치하는 것입니다. 예를 들어, 인수에 1을 더하는 함수는 다음과 같이 작성할 수 있습니다.

def add1 (n : Nat) : Nat := n + 1

#eval로 이 함수를 테스트하면 예상대로 8이 나옵니다.

#eval add1 7

함수가 각 인수 사이에 공백을 써서 여러 인수에 적용되는 것처럼, 여러 인수를 받는 함수는 인수의 이름과 타입 사이에 공백을 두어 정의됩니다. maximum 함수는 두 인수 n과 k 중 더 큰 값과 같은 결과를 내며, 두 개의 Nat 인수를 받아 Nat를 반환합니다.

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

마찬가지로, spaceBetween 함수는 두 문자열 사이에 공백을 넣어 결합합니다.

def spaceBetween (before : String) (after : String) : String :=
  String.append before (String.append " " after)

maximum과 같은 정의된 함수에 인수가 제공되면, 결과는 먼저 본문에서 인수 이름을 제공된 값으로 바꾼 다음, 결과 본문을 평가하여 결정됩니다. 예를 들면 다음과 같습니다.

maximum (5 + 8) (2 * 7)

  ⟹  \implies

maximum 13 14

  ⟹  \implies

if 13 < 14 then 14 else 13

  ⟹  \implies

14

자연수, 정수, 문자열로 평가되는 표현식은 이를 나타내는 타입(Nat, Int, String 등)을 가집니다. 이는 함수에도 마찬가지입니다. Nat를 받아 Bool을 반환하는 함수는 Nat → Bool 타입을 가지며, 두 개의 Nat를 받아 Nat를 반환하는 함수는 Nat → Nat → Nat 타입을 가집니다.

특별한 경우로, Lean은 #check와 함께 이름이 직접 사용될 때 함수의 시그니처를 반환합니다. #check add1을 입력하면 add1 (n : Nat) : Nat가 나옵니다. 그러나 함수의 이름을 괄호 안에 써서 함수를 일반 표현식으로 취급하게 함으로써 Lean을 "속여" 함수의 타입을 표시하게 할 수 있습니다. 따라서 #check (add1)은 add1 : Nat → Nat를, #check (maximum)은 maximum : Nat → Nat → Nat를 산출합니다. 이 화살표는 ASCII 대체 화살표 ->로도 쓸 수 있으므로, 앞선 함수 타입은 각각 example : Nat -> Nat := add1과 example : Nat -> Nat -> Nat := maximum으로 쓸 수 있습니다.

내부적으로 모든 함수는 실제로는 정확히 하나의 인수를 기대합니다. maximum처럼 여러 인수를 받는 것처럼 보이는 함수는 사실 하나의 인수를 받고 새로운 함수를 반환하는 함수입니다. 이 새로운 함수는 다음 인수를 받고, 더 이상 기대되는 인수가 없을 때까지 이 과정이 계속됩니다. 이는 여러 인수를 받는 함수에 하나의 인수를 제공함으로써 확인할 수 있습니다. #check maximum 3은 maximum 3 : Nat → Nat를, #check spaceBetween "Hello "는 spaceBetween "Hello " : String → String을 산출합니다. 함수를 반환하는 함수를 사용하여 다중 인수 함수를 구현하는 것을 수학자 하스켈 커리의 이름을 따서 커링(currying)이라고 합니다. 함수 화살표는 오른쪽으로 결합하므로, Nat → Nat → Nat는 Nat → (Nat → Nat)로 괄호를 쳐야 합니다.

1.3.1.1. 연습 문제

• String → String → String → String 타입의 joinStringsWith 함수를 정의하세요. 이 함수는 첫 번째 인수를 두 번째와 세 번째 인수 사이에 넣어 새로운 문자열을 만듭니다. joinStringsWith ", " "one" "and another"는 "one, and another"로 평가되어야 합니다.

• joinStringsWith ": "의 타입은 무엇일까요? Lean으로 답을 확인해 보세요.

• 주어진 높이, 너비, 깊이로 직육면체의 부피를 계산하는 Nat → Nat → Nat → Nat 타입의 volume 함수를 정의하세요.

1.3.2. 타입 정의하기

대부분의 타입이 있는 프로그래밍 언어에는 C의 typedef와 같이 타입에 대한 별칭을 정의하는 수단이 있습니다. 그러나 Lean에서는 타입이 언어의 일급(first-class) 구성 요소입니다. 즉, 타입은 다른 표현식과 마찬가지입니다. 이는 정의가 다른 값뿐만 아니라 타입도 참조할 수 있음을 의미합니다.

예를 들어, String을 입력하기가 너무 길다면, 더 짧은 약어 Str을 정의할 수 있습니다.

def Str : Type := String

그러면 String 대신 Str을 정의의 타입으로 사용할 수 있습니다.

def aStr : Str := "This is a string."

이것이 작동하는 이유는 타입이 Lean의 나머지 부분과 동일한 규칙을 따르기 때문입니다. 타입은 표현식이며, 표현식에서 정의된 이름은 그 정의로 대체될 수 있습니다. Str이 String을 의미하도록 정의되었기 때문에 aStr의 정의는 타당합니다.

1.3.2.1. 마주칠 수 있는 메시지

타입에 대한 정의를 사용하는 실험은 Lean이 오버로드된 정수 리터럴을 지원하는 방식 때문에 더 복잡해집니다. Nat이 너무 짧다면, 더 긴 이름 NaturalNumber를 정의할 수 있습니다. def NaturalNumber : Type := Nat

그러나 Nat 대신 NaturalNumber를 정의의 타입으로 사용하는 것은 예상대로 작동하지 않습니다. 특히, 다음 정의는: def thirtyEight : NaturalNumber := 38

다음과 같은 오류를 발생시킵니다.

failed to synthesize
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

이 오류는 Lean이 숫자 리터럴을 오버로드할 수 있도록 허용하기 때문에 발생합니다. 타당할 경우, 자연수 리터럴은 마치 해당 타입이 시스템에 내장된 것처럼 새로운 타입에 사용될 수 있습니다. 이것은 수학을 편리하게 표현하려는 Lean의 목표의 일부이며, 수학의 다른 분야에서는 숫자 표기법을 매우 다른 목적으로 사용합니다. 이 오버로딩을 허용하는 특정 기능은 오버로딩을 찾기 전에 모든 정의된 이름을 그 정의로 대체하지 않기 때문에 위와 같은 오류 메시지가 발생합니다.

이 제한을 해결하는 한 가지 방법은 정의의 오른쪽에 Nat 타입을 제공하여 38에 대해 Nat의 오버로딩 규칙이 사용되도록 하는 것입니다.

def thirtyEight : NaturalNumber := (38 : Nat)

NaturalNumber는 정의에 따라 Nat와 동일한 타입이므로 이 정의는 여전히 타입이 올바릅니다!

또 다른 해결책은 Nat에 대한 오버로딩과 동등하게 작동하는 NaturalNumber에 대한 오버로딩을 정의하는 것입니다. 그러나 이를 위해서는 Lean의 더 고급 기능이 필요합니다.

마지막으로, def 대신 abbrev를 사용하여 Nat에 대한 새 이름을 정의하면 오버로딩 해결 과정에서 정의된 이름이 그 정의로 대체될 수 있습니다. abbrev를 사용하여 작성된 정의는 항상 전개(unfold)됩니다. 예를 들어, 다음은 문제없이 받아들여집니다.

abbrev N : Type := Nat
def thirtyNine : N := 39

내부적으로 일부 정의는 오버로딩 해결 중에 전개 가능하도록 표시되는 반면, 다른 정의는 그렇지 않습니다. 전개될 정의를 축약 가능(reducible)하다고 합니다. 축약 가능성에 대한 제어는 Lean이 확장성을 갖추기 위해 필수적입니다. 모든 정의를 완전히 전개하면 기계가 처리하기에 느리고 사용자가 이해하기 어려운 매우 큰 타입이 될 수 있습니다. abbrev로 생성된 정의는 축약 가능으로 표시됩니다.

1.4. 구조체

프로그램을 작성하는 첫 단계는 보통 문제 영역의 개념을 파악한 다음, 코드에서 이를 적절하게 표현하는 방법을 찾는 것입니다. 때로는 도메인 개념이 다른 더 간단한 개념들의 집합일 수 있습니다. 이 경우, 이러한 더 간단한 구성 요소들을 하나의 "패키지"로 묶어 의미 있는 이름을 부여하는 것이 편리할 수 있습니다. Lean에서는 이를 구조체(structure)를 사용하여 수행하며, 이는 C나 Rust의 struct, C#의 record와 유사합니다.

구조체를 정의하면 Lean에 완전히 새로운 타입이 도입되며, 이 타입은 다른 어떤 타입으로도 환원될 수 없습니다. 이는 여러 구조체가 동일한 데이터를 포함하더라도 서로 다른 개념을 나타낼 수 있기 때문에 유용합니다. 예를 들어, 한 점은 직교좌표계나 극좌표계를 사용하여 표현될 수 있으며, 각각은 한 쌍의 부동소수점 숫자로 이루어집니다. 별도의 구조체를 정의하면 API 클라이언트가 하나를 다른 것으로 혼동하는 것을 방지할 수 있습니다.

Lean의 부동소수점 숫자 타입은 Float이라고 하며, 부동소수점 숫자는 일반적인 표기법으로 작성됩니다.

#check 1.2

1.2 : Float

#check -454.2123215

-454.2123215 : Float

#check 0.0

0.0 : Float

부동소수점 숫자를 소수점과 함께 작성하면 Lean은 Float 타입을 추론합니다. 소수점 없이 작성하면 타입 명시가 필요할 수 있습니다.

#check 0

0 : Nat

#check (0 : Float)

0 : Float

직교좌표계의 점은 x와 y라는 두 개의 Float 필드를 가진 구조체입니다. 이는 structure 키워드를 사용하여 선언됩니다.

structure Point where
  x : Float
  y : Float

이 선언 이후, Point는 새로운 구조체 타입이 됩니다. 구조체 타입의 값을 만드는 일반적인 방법은 중괄호 안에 모든 필드에 대한 값을 제공하는 것입니다. 데카르트 평면의 원점은 x와 y가 모두 0인 곳입니다.

def origin : Point := { x := 0.0, y := 0.0 }

#eval origin의 결과는 origin의 정의와 매우 유사하게 보입니다.

{ x := 0.000000, y := 0.000000 }

구조체는 데이터 모음을 "묶어서" 이름을 붙이고 단일 단위로 취급하기 위해 존재하므로, 구조체의 개별 필드를 추출할 수 있는 것도 중요합니다. 이는 C, Python, Rust 또는 JavaScript에서처럼 점 표기법(dot notation)을 사용하여 수행됩니다.

#eval origin.x

0.000000

#eval origin.y

0.000000

이를 사용하여 구조체를 인수로 받는 함수를 정의할 수 있습니다. 예를 들어, 점의 덧셈은 기본 좌표 값을 더하여 수행됩니다. 다음과 같아야 합니다.

#eval addPoints { x := 1.5, y := 32 } { x := -8, y := 0.2 }

결과는 다음과 같습니다.

{ x := -6.500000, y := 32.200000 }

함수 자체는 p1과 p2라는 두 개의 Point를 인수로 받습니다. 결과 점은 p1과 p2의 x 및 y 필드를 기반으로 합니다.

def addPoints (p1 : Point) (p2 : Point) : Point :=
  { x := p1.x + p2.x, y := p1.y + p2.y }

마찬가지로, 두 점 사이의 거리, 즉 x와 y 성분 차이의 제곱의 합의 제곱근은 다음과 같이 작성할 수 있습니다.

def distance (p1 : Point) (p2 : Point) : Float :=
  Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))

예를 들어, (1,2)와 (5,−1) 사이의 거리는 5입니다.

#eval distance { x := 1.0, y := 2.0 } { x := 5.0, y := -1.0 }

5.000000

여러 구조체가 같은 이름의 필드를 가질 수 있습니다. 3차원 점 데이터 타입은 x와 y 필드를 공유할 수 있으며, 같은 필드 이름으로 인스턴스화될 수 있습니다.

structure Point3D where
  x : Float
  y : Float
  z : Float
def origin3D : Point3D := { x := 0.0, y := 0.0, z := 0.0 }

이는 중괄호 구문을 사용하기 위해 구조체의 예상 타입을 알아야 함을 의미합니다. 타입을 알 수 없는 경우 Lean은 구조체를 인스턴스화할 수 없습니다. 예를 들어, 이 코드는:

#check { x := 0.0, y := 0.0 }

다음과 같은 오류가 발생합니다.

invalid {...} notation, expected type is not known

보통 그렇듯이, 타입 명시를 제공하여 이 상황을 해결할 수 있습니다.

#check ({ x := 0.0, y := 0.0 } : Point)

{ x := 0.0, y := 0.0 } : Point

프로그램을 더 간결하게 만들기 위해, Lean은 중괄호 안에 구조체 타입 명시를 허용하기도 합니다.

#check { x := 0.0, y := 0.0 : Point}

{ x := 0.0, y := 0.0 } : Point

1.4.1. 구조체 업데이트

Point의 x 필드를 0으로 바꾸는 zeroX라는 함수를 상상해 보세요. 대부분의 프로그래밍 언어 커뮤니티에서 이 문장은 x가 가리키는 메모리 위치를 새 값으로 덮어써야 한다는 의미일 것입니다. 하지만 Lean은 함수형 프로그래밍 언어입니다. 함수형 프로그래밍 커뮤니티에서 이런 종류의 진술은 거의 항상 x 필드는 새 값을 가리키고 다른 모든 필드는 입력의 원래 값을 가리키는 새로운 Point가 할당된다는 것을 의미합니다. zeroX를 작성하는 한 가지 방법은 이 설명을 문자 그대로 따라, x에 대한 새 값을 채우고 y를 수동으로 옮기는 것입니다.

def zeroX (p : Point) : Point :=
  { x := 0, y := p.y }

그러나 이 프로그래밍 스타일에는 단점이 있습니다. 첫째, 구조체에 새 필드가 추가되면 어떤 필드든 업데이트하는 모든 곳을 업데이트해야 하므로 유지 관리가 어려워집니다. 둘째, 구조체에 같은 타입의 필드가 여러 개 포함된 경우, 복사-붙여넣기 코딩으로 인해 필드 내용이 중복되거나 바뀌는 실제 위험이 있습니다. 마지막으로, 프로그램이 길고 관료적으로 변합니다.

Lean은 구조체의 일부 필드는 바꾸고 나머지는 그대로 두는 편리한 구문을 제공합니다. 이는 구조체 초기화에서 with 키워드를 사용하여 수행됩니다. 변경되지 않은 필드의 소스는 with 앞에 오고, 새 필드는 뒤에 옵니다. 예를 들어, zeroX는 새로운 x 값만으로 작성할 수 있습니다.

def zeroX (p : Point) : Point :=
  { p with x := 0 }

이 구조체 업데이트 구문은 기존 값을 수정하지 않고, 이전 값과 일부 필드를 공유하는 새 값을 생성한다는 점을 기억하세요. fourAndThree라는 점이 주어졌을 때:

def fourAndThree : Point :=
  { x := 4.3, y := 3.4 }

이를 평가한 다음, zeroX를 사용하여 업데이트한 것을 평가하고, 다시 평가하면 원래 값이 나옵니다.

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

#eval zeroX fourAndThree

{ x := 0.000000, y := 3.400000 }

#eval fourAndThree

{ x := 4.300000, y := 3.400000 }

구조체 업데이트가 원본 구조체를 수정하지 않는다는 사실의 한 가지 결과는, 새 값이 이전 값으로부터 계산되는 경우에 대해 추론하기가 더 쉬워진다는 것입니다. 이전 구조체에 대한 모든 참조는 제공된 모든 새 값에서 계속 동일한 필드 값을 참조합니다.

1.4.2. 내부 동작

모든 구조체에는 생성자(constructor)가 있습니다. 여기서 "생성자"라는 용어는 혼란의 원인이 될 수 있습니다. Java나 Python과 같은 언어의 생성자와 달리, Lean의 생성자는 데이터 타입이 초기화될 때 실행되는 임의의 코드가 아닙니다. 대신, 생성자는 새로 할당된 데이터 구조에 저장될 데이터를 단순히 모으는 역할을 합니다. 데이터를 전처리하거나 유효하지 않은 인수를 거부하는 사용자 정의 생성자를 제공하는 것은 불가능합니다. 이는 "생성자"라는 단어가 두 맥락에서 서로 관련은 있지만 다른 의미를 갖는 경우입니다.

기본적으로, S라는 이름의 구조체에 대한 생성자는 S.mk라는 이름이 붙습니다. 여기서 S는 네임스페이스 한정자이고, mk는 생성자 자체의 이름입니다. 중괄호 초기화 구문 대신 생성자를 직접 적용할 수도 있습니다.

#check Point.mk 1.5 2.8

그러나 이것은 일반적으로 좋은 Lean 스타일로 간주되지 않으며, Lean조차도 표준 구조체 초기화 구문을 사용하여 피드백을 반환합니다.

{ x := 1.5, y := 2.8 } : Point

생성자는 함수 타입을 가지므로, 함수가 예상되는 모든 곳에서 사용할 수 있습니다. 예를 들어, Point.mk는 두 개의 Float(각각 x와 y)를 받아 새로운 Point를 반환하는 함수입니다.

#check (Point.mk)

Point.mk : Float → Float → Point

구조체의 생성자 이름을 재정의하려면, 이름 앞에 콜론 두 개를 붙여 작성합니다. 예를 들어, Point.mk 대신 Point.point를 사용하려면 다음과 같이 작성합니다.

structure Point where
  point ::
  x : Float
  y : Float

생성자 외에도, 구조체의 각 필드에 대해 접근자(accessor) 함수가 정의됩니다. 이들은 구조체의 네임스페이스 내에서 필드와 동일한 이름을 가집니다. Point의 경우, 접근자 함수 Point.x와 Point.y가 생성됩니다.

#check (Point.x)

Point.x : Point → Float

#check (Point.y)

Point.y : Point → Float

사실, 중괄호 구조체 생성 구문이 내부적으로 구조체의 생성자 호출로 변환되는 것처럼, 이전 addPoints 정의의 x 구문은 x 접근자 호출로 변환됩니다. 즉, #eval origin.x와 #eval Point.x origin은 모두 다음을 산출합니다.

0.000000

접근자 점 표기법은 구조체 필드뿐만 아니라 더 많은 것과 함께 사용할 수 있습니다. 임의의 수의 인수를 받는 함수에도 사용할 수 있습니다. 더 일반적으로, 접근자 표기법은 TARGET.f ARG1 ARG2 ... 형식을 가집니다. TARGET의 타입이 T이면, T.f라는 이름의 함수가 호출됩니다. TARGET은 타입이 T인 가장 왼쪽 인수가 되며(항상 첫 번째는 아님), ARG1 ARG2 ...는 나머지 인수로 순서대로 제공됩니다. 예를 들어, String은 append 필드를 가진 구조체가 아니지만, 접근자 표기법으로 문자열에서 String.append를 호출할 수 있습니다.

#eval "one string".append " and another"

"one string and another"

이 예에서 TARGET은 "one string"을 나타내고 ARG1은 " and another"를 나타냅니다.

Point.modifyBoth 함수(즉, Point 네임스페이스에 정의된 modifyBoth)는 Point의 두 필드 모두에 함수를 적용합니다.

def Point.modifyBoth (f : Float → Float) (p : Point) : Point :=
  { x := f p.x, y := f p.y }

Point 인수가 함수 인수 뒤에 오더라도, 점 표기법으로 사용할 수 있습니다.

#eval fourAndThree.modifyBoth Float.floor

{ x := 4.000000, y := 3.000000 }

이 경우, TARGET은 fourAndThree를 나타내고, ARG1은 Float.floor입니다. 이는 접근자 표기법의 대상이 반드시 첫 번째 인수가 아니라, 타입이 일치하는 첫 번째 인수로 사용되기 때문입니다.

1.4.3. 연습 문제

• 직육면체의 높이, 너비, 깊이를 각각 Float으로 포함하는 RectangularPrism이라는 이름의 구조체를 정의하세요.

• 직육면체의 부피를 계산하는 volume : RectangularPrism → Float라는 이름의 함수를 정의하세요.

• 끝점으로 선분을 나타내는 Segment라는 이름의 구조체를 정의하고, 선분의 길이를 계산하는 length : Segment → Float라는 함수를 정의하세요. Segment는 최대 두 개의 필드를 가져야 합니다.

• RectangularPrism의 선언으로 어떤 이름들이 도입되나요?

• 다음 Hamster와 Book 선언으로 어떤 이름들이 도입되나요? 그들의 타입은 무엇인가요?

  structure Hamster where
    name : String
    fluffy : Bool
  
  structure Book where
    makeBook ::
    title : String
    author : String
    price : Float

1.5. 자료형과 패턴

구조체는 여러 독립적인 데이터를 조합하여 새로운 타입으로 표현되는 일관된 전체로 만들 수 있습니다. 구조체처럼 값의 모음을 그룹화하는 타입을 곱 타입(product type)이라고 합니다. 하지만 많은 도메인 개념은 구조체로 자연스럽게 표현될 수 없습니다. 예를 들어, 어떤 애플리케이션은 사용자 권한을 추적해야 할 수 있는데, 일부 사용자는 문서 소유자이고, 일부는 문서를 편집할 수 있으며, 다른 사용자는 읽기만 가능할 수 있습니다. 계산기에는 덧셈, 뺄셈, 곱셈과 같은 여러 이항 연산자가 있습니다. 구조체는 여러 선택지를 인코딩하는 쉬운 방법을 제공하지 않습니다.

마찬가지로, 구조체는 고정된 수의 필드를 추적하는 훌륭한 방법이지만, 많은 애플리케이션은 임의의 수의 요소를 포함할 수 있는 데이터가 필요합니다. 트리나 리스트와 같은 대부분의 고전적인 자료 구조는 재귀적인 구조를 가집니다. 리스트의 꼬리가 그 자체로 리스트이거나, 이진 트리의 왼쪽과 오른쪽 가지가 그 자체로 이진 트리인 경우처럼 말입니다. 앞서 언급한 계산기에서 표현식 자체의 구조가 재귀적입니다. 예를 들어, 덧셈 표현식의 피가산수는 그 자체가 곱셈 표현식일 수 있습니다.

선택을 허용하는 자료형을 합 타입(sum type)이라고 하고, 자기 자신의 인스턴스를 포함할 수 있는 자료형을 재귀 자료형(recursive datatype)이라고 합니다. 재귀적인 합 타입은 귀납적 자료형(inductive datatype)이라고 불리는데, 수학적 귀납법을 사용하여 이에 대한 명제를 증명할 수 있기 때문입니다. 프로그래밍할 때, 귀납적 자료형은 패턴 매칭과 재귀 함수를 통해 사용됩니다.

많은 내장 타입은 사실 표준 라이브러리에 있는 귀납적 자료형입니다. 예를 들어, Bool은 귀납적 자료형입니다.

inductive Bool where
  | false : Bool
  | true : Bool

이 정의는 두 가지 주요 부분으로 구성됩니다. 첫 번째 줄은 새로운 타입의 이름(Bool)을 제공하고, 나머지 줄들은 각각 생성자(constructor)를 설명합니다. 구조체의 생성자와 마찬가지로, 귀납적 자료형의 생성자는 임의의 초기화 및 유효성 검사 코드를 삽입하는 곳이 아니라, 다른 데이터를 수신하고 담는 단순하고 비활성적인 컨테이너일 뿐입니다. 구조체와 달리, 귀납적 자료형은 여러 생성자를 가질 수 있습니다. 여기에는 true와 false라는 두 개의 생성자가 있으며, 둘 다 인자를 받지 않습니다. 구조체 선언이 선언된 타입의 이름을 딴 네임스페이스에 자신의 이름을 넣는 것처럼, 귀납적 자료형도 생성자의 이름을 네임스페이스에 넣습니다. Lean 표준 라이브러리에서는 true와 false가 이 네임스페이스에서 다시 익스포트되어 Bool.true와 Bool.false가 아닌, 단독으로 작성될 수 있습니다.

데이터 모델링 관점에서, 귀납적 자료형은 다른 언어에서 봉인된 추상 클래스(sealed abstract class)가 사용될 수 있는 많은 맥락에서 사용됩니다. C#이나 Java와 같은 언어에서는 Bool을 다음과 같이 유사하게 정의할 수 있습니다.

abstract class Bool {}
class True extends Bool {}
class False extends Bool {}

하지만, 이러한 표현의 구체적인 내용은 상당히 다릅니다. 특히, 각각의 비추상 클래스는 새로운 타입과 데이터를 할당하는 새로운 방법을 모두 만듭니다. 객체 지향 예제에서 True와 False는 모두 Bool보다 더 구체적인 타입인 반면, Lean 정의는 Bool이라는 새로운 타입만 도입합니다.

음이 아닌 정수 타입인 Nat은 귀납적 자료형입니다.

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

여기서 zero는 0을 나타내고, succ는 다른 어떤 수의 다음 수(successor)를 나타냅니다. succ의 선언에 언급된 Nat은 바로 정의되고 있는 Nat 타입 그 자체입니다. 다음 수란 "1 더 큰 수"를 의미하므로, 5의 다음 수는 6이고 32,185의 다음 수는 32,186입니다. 이 정의를 사용하면, 4는 Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))로 표현됩니다. 이 정의는 이름이 약간 다른 것을 제외하면 Bool의 정의와 거의 같습니다. 유일한 실질적인 차이점은 succ 뒤에 (n : Nat)가 온다는 것인데, 이는 succ 생성자가 n이라는 이름을 가진 Nat 타입의 인자를 받는다는 것을 명시합니다. zero와 succ라는 이름은 그들의 타입을 딴 네임스페이스에 있으므로, 각각 Nat.zero와 Nat.succ로 참조되어야 합니다.

n과 같은 인자 이름은 Lean의 오류 메시지나 수학적 증명을 작성할 때 제공되는 피드백에 나타날 수 있습니다. Lean에는 이름으로 인자를 제공하는 선택적 구문도 있습니다. 그러나 일반적으로 인자 이름의 선택은 구조체 필드 이름의 선택보다 덜 중요한데, API의 큰 부분을 차지하지 않기 때문입니다.

C# 이나 Java에서 Nat은 다음과 같이 정의될 수 있습니다.

abstract class Nat {}
class Zero extends Nat {}
class Succ extends Nat {
    public Nat n;
    public Succ(Nat pred) {
        n = pred;
    }
}

위의 Bool 예제에서처럼, 이는 Lean의 등가물보다 더 많은 타입을 정의합니다. 또한, 이 예제는 Lean 자료형 생성자가 C# 이나 Java의 생성자라기보다는 추상 클래스의 서브클래스와 훨씬 더 유사하다는 점을 강조합니다. 여기에 표시된 생성자는 실행될 초기화 코드를 포함하고 있기 때문입니다.

합 타입은 TypeScript에서 구별된 유니온(discriminated union)을 인코딩하기 위해 문자열 태그를 사용하는 것과도 유사합니다. TypeScript에서 Nat은 다음과 같이 정의될 수 있습니다.

interface Zero {
    tag: "zero";
}

interface Succ {
    tag: "succ";
    predecessor: Nat;
}

type Nat = Zero | Succ;

C# 및 Java와 마찬가지로, 이 인코딩은 Lean에서보다 더 많은 타입을 가지게 되는데, Zero와 Succ가 각각 독립적인 타입이기 때문입니다. 또한 이는 Lean 생성자가 내용물을 식별하는 태그를 포함하는 JavaScript나 TypeScript의 객체에 해당한다는 것을 보여줍니다.

1.5.1. 패턴 매칭

많은 언어에서 이러한 종류의 데이터는 먼저 인스턴스-오브(instance-of) 연산자를 사용하여 어떤 서브클래스를 받았는지 확인한 다음, 해당 서브클래스에서 사용 가능한 필드의 값을 읽는 방식으로 소비됩니다. 인스턴스-오브 확인은 어떤 코드를 실행할지 결정하여 이 코드에 필요한 데이터가 사용 가능하도록 보장하는 반면, 필드 자체는 데이터를 제공합니다. Lean에서는 이 두 가지 목적이 모두 패턴 매칭에 의해 동시에 수행됩니다.

패턴 매칭을 사용하는 함수의 예는 isZero로, 이 함수는 인자가 Nat.zero일 때 true를, 그렇지 않으면 false를 반환합니다.

def isZero (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => false

match 표현식에는 함수의 인자 n이 구조 분해를 위해 제공됩니다. 만약 n이 Nat.zero에 의해 생성되었다면, 패턴 매칭의 첫 번째 분기가 선택되어 결과는 true가 됩니다. 만약 n이 Nat.succ에 의해 생성되었다면, 두 번째 분기가 선택되어 결과는 false가 됩니다.

단계별로, isZero Nat.zero의 평가는 다음과 같이 진행됩니다.

isZero Nat.zero

  ⟹  \implies

match Nat.zero with

  ⟹  \implies

| Nat.zero => true

  ⟹  \implies

| Nat.succ k => false

  ⟹  \implies

true

isZero 5의 평가도 비슷하게 진행됩니다.

isZero 5

  ⟹  \implies

isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))

  ⟹  \implies

match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
| Nat.zero => true
| Nat.succ k => false

  ⟹  \implies

false

isZero의 패턴 두 번째 분기에 있는 k는 장식이 아닙니다. 이는 Nat.succ의 인자인 Nat을 제공된 이름으로 보이게 만듭니다. 그러면 그 더 작은 숫자를 사용하여 표현식의 최종 결과를 계산할 수 있습니다.

어떤 숫자 n의 다음 수가 n보다 1 큰 수(즉, n+1)인 것처럼, 어떤 수의 이전 수(predecessor)는 그 수보다 1 작은 수입니다. 만약 pred가 Nat의 이전 수를 찾는 함수라면, 다음 예제들은 예상된 결과를 찾아야 합니다.

#eval pred 5

4

#eval pred 839

838

Nat은 음수를 표현할 수 없기 때문에, Nat.zero는 약간의 난제입니다. 보통 Nat으로 작업할 때, 음수를 생성할 수 있는 연산자들은 0 자체를 생성하도록 재정의됩니다.

#eval pred 0

0

Nat의 이전 수를 찾기 위해, 첫 번째 단계는 어떤 생성자가 그것을 만드는 데 사용되었는지 확인하는 것입니다. 만약 Nat.zero였다면, 결과는 Nat.zero입니다. 만약 Nat.succ였다면, k라는 이름이 그 아래의 Nat을 참조하는 데 사용됩니다. 그리고 이 Nat이 원하는 이전 수이므로, Nat.succ 분기의 결과는 k입니다.

def pred (n : Nat) : Nat :=
  match n with
  | Nat.zero => Nat.zero
  | Nat.succ k => k

이 함수를 5에 적용하면 다음 단계들이 나옵니다.

pred 5

  ⟹  \implies

pred (Nat.succ 4)

  ⟹  \implies

match Nat.succ 4 with
| Nat.zero => Nat.zero
| Nat.succ k => k

  ⟹  \implies

4

패턴 매칭은 합 타입뿐만 아니라 구조체와도 함께 사용될 수 있습니다. 예를 들어, Point3D에서 세 번째 차원을 추출하는 함수는 다음과 같이 작성할 수 있습니다.

def depth (p : Point3D) : Float :=
  match p with
  | { x:= h, y := w, z := d } => d

이 경우, Point3D.z 접근자를 사용하는 것이 훨씬 간단했겠지만, 구조체 패턴은 때때로 함수를 작성하는 가장 간단한 방법이 될 수 있습니다.

1.5.2. 재귀 함수

정의되고 있는 이름을 참조하는 정의를 재귀 정의(recursive definition)라고 합니다. 귀납적 자료형은 재귀적일 수 있습니다. 실제로, Nat은 succ가 또 다른 Nat을 요구하기 때문에 그러한 자료형의 예입니다. 재귀 자료형은 사용 가능한 메모리와 같은 기술적 요인에 의해서만 제한되는, 임의로 큰 데이터를 나타낼 수 있습니다. 자료형 정의에서 각 자연수에 대해 하나의 생성자를 모두 적는 것이 불가능한 것처럼, 각 가능성에 대한 패턴 매칭 케이스를 모두 적는 것도 불가능합니다.

재귀 자료형은 재귀 함수와 잘 어울립니다. Nat에 대한 간단한 재귀 함수는 인자가 짝수인지 확인하는 것입니다. 이 경우, Nat.zero는 짝수입니다. 이와 같은 코드의 비재귀적인 분기를 베이스 케이스(base case)라고 합니다. 홀수의 다음 수는 짝수이고, 짝수의 다음 수는 홀수입니다. 이는 Nat.succ로 만들어진 숫자가 짝수라는 것은 그 인자가 짝수가 아닐 때와 같다는 것을 의미합니다.

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

이러한 사고 패턴은 Nat에 대한 재귀 함수를 작성할 때 전형적입니다. 먼저, Nat.zero에 대해 무엇을 할지 식별합니다. 그런 다음, 임의의 Nat에 대한 결과를 그 다음 수에 대한 결과로 변환하는 방법을 결정하고, 이 변환을 재귀 호출의 결과에 적용합니다. 이 패턴을 구조적 재귀(structural recursion)라고 합니다.

많은 언어와 달리, Lean은 기본적으로 모든 재귀 함수가 결국 베이스 케이스에 도달하도록 보장합니다. 프로그래밍 관점에서 이는 우발적인 무한 루프를 배제합니다. 그러나 이 기능은 정리를 증명할 때 특히 중요한데, 무한 루프는 큰 어려움을 야기하기 때문입니다. 이로 인한 결과 중 하나는 Lean이 원래 숫자에 대해 재귀적으로 자신을 호출하려는 even 버전을 받아들이지 않는다는 것입니다.

def evenLoops (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (evenLoops n)

오류 메시지의 중요한 부분은 Lean이 재귀 함수가 항상 베이스 케이스에 도달한다는 것을 결정할 수 없었다는 것입니다(실제로 그렇지 않기 때문입니다).

fail to show termination for
  evenLoops
with errors
failed to infer structural recursion:
Not considering parameter n of evenLoops:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, `evenLoops` does not take any (non-fixed) arguments

덧셈은 두 개의 인자를 받지만, 그 중 하나만 검사하면 됩니다. 숫자 n에 0을 더하려면, 그냥 n을 반환하면 됩니다. k의 다음 수를 n에 더하려면, k를 n에 더한 결과의 다음 수를 취하면 됩니다.

def plus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => Nat.succ (plus n k')

plus의 정의에서, k'라는 이름은 인자 k와 연결되어 있지만 동일하지는 않다는 것을 나타내기 위해 선택되었습니다. 예를 들어, plus 3 2의 평가를 따라가 보면 다음 단계들이 나옵니다.

plus 3 2

  ⟹  \implies

plus 3 (Nat.succ (Nat.succ Nat.zero))

  ⟹  \implies

match Nat.succ (Nat.succ Nat.zero) with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')

  ⟹  \implies

Nat.succ (plus 3 (Nat.succ Nat.zero))

  ⟹  \implies

Nat.succ (match Nat.succ Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k'))

  ⟹  \implies

Nat.succ (Nat.succ (plus 3 Nat.zero))

  ⟹  \implies

Nat.succ (Nat.succ (match Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')))

  ⟹  \implies

Nat.succ (Nat.succ 3)

  ⟹  \implies

5

덧셈에 대해 생각하는 한 가지 방법은 n+kn+k가 Nat.succ를 n에 k번 적용하는 것이라는 점입니다. 비슷하게, 곱셈 n×kn\times k는 n을 자신에게 k번 더하는 것이고, 뺄셈 n−kn−k는 n의 이전 수를 k번 취하는 것입니다.

def times (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => Nat.zero
  | Nat.succ k' => plus n (times n k')

def minus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => pred (minus n k')

모든 함수가 구조적 재귀를 사용하여 쉽게 작성될 수 있는 것은 아닙니다. 덧셈을 반복된 Nat.succ로, 곱셈을 반복된 덧셈으로, 뺄셈을 반복된 이전 수로 이해하는 것은 나눗셈을 반복된 뺄셈으로 구현할 수 있음을 시사합니다. 이 경우, 피제수가 제수보다 작으면 결과는 0입니다. 그렇지 않으면, 결과는 피제수에서 제수를 뺀 값을 제수로 나눈 값의 다음 수입니다.

def div (n : Nat) (k : Nat) : Nat :=
  if n < k then
    0
  else Nat.succ (div (n - k) k)

두 번째 인자가 0이 아닌 한, 이 프로그램은 항상 베이스 케이스를 향해 진행하므로 종료됩니다. 그러나 이는 구조적으로 재귀적이지 않은데, 0에 대한 결과를 찾고 더 작은 Nat에 대한 결과를 그 다음 수에 대한 결과로 변환하는 패턴을 따르지 않기 때문입니다. 특히, 함수의 재귀적 호출이 입력 생성자의 인자가 아닌 다른 함수 호출의 결과에 적용됩니다. 따라서 Lean은 다음 메시지와 함께 이를 거부합니다.

fail to show termination for
  div
with errors
failed to infer structural recursion:
Not considering parameter k of div:
  it is unchanged in the recursive calls
Cannot use parameter k:
  failed to eliminate recursive application
    div (n - k) k


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
k n:Nath✝:¬n < k
⊢ n - k < n

이 메시지는 div가 수동으로 종료 증명을 요구한다는 것을 의미합니다. 이 주제는 마지막 장에서 탐구됩니다.

1.6. 다형성(Polymorphism)

대부분의 언어에서처럼, Lean에서도 타입은 인자를 가질 수 있습니다. 예를 들어, List Nat 타입은 자연수의 리스트를, List String은 문자열의 리스트를, 그리고 List (List Point)는 Point로 이루어진 리스트로 이루어진 리스트를 나타냅니다. 이는 C#이나 Java 같은 언어의 List<Nat>, List<String>, 또는 List<List<Point>>와 매우 유사합니다. Lean이 함수에 인자를 전달할 때 공백을 사용하는 것처럼, 타입에 인자를 전달할 때도 공백을 사용합니다.

함수형 프로그래밍에서 다형성이라는 용어는 일반적으로 타입을 인자로 받는 데이터 타입과 정의를 가리킵니다. 이는 객체 지향 프로그래밍 커뮤니티에서 일반적으로 슈퍼클래스의 일부 동작을 재정의(override)할 수 있는 서브클래스를 가리키는 것과는 다릅니다. 이 책에서 "다형성"은 항상 전자의 의미로 사용됩니다. 이러한 타입 인자들은 데이터 타입이나 정의 내에서 사용될 수 있으며, 이를 통해 동일한 데이터 타입이나 정의를 인자의 이름을 다른 타입으로 대체하여 얻어지는 모든 타입과 함께 사용할 수 있습니다.

Point 구조체는 x와 y 필드가 모두 Float이어야 합니다. 하지만 점에 대해 각 좌표에 특정 표현을 요구하는 본질적인 이유는 없습니다. Point의 다형적 버전인 PPoint는 타입을 인자로 받아 두 필드에 모두 그 타입을 사용할 수 있습니다.

structure PPoint (α : Type) where
  x : α
  y : α

함수 정의의 인자들이 정의되는 이름 바로 뒤에 쓰이는 것처럼, 구조체의 인자들도 구조체 이름 바로 뒤에 쓰입니다. Lean에서는 더 구체적인 이름이 떠오르지 않을 때 타입 인자의 이름으로 그리스 문자를 사용하는 것이 관례입니다. Type은 다른 타입을 설명하는 타입이므로, Nat, List String, PPoint Int는 모두 Type이라는 타입을 가집니다.

List와 마찬가지로, PPoint도 특정 타입을 인자로 제공하여 사용할 수 있습니다.

def natOrigin : PPoint Nat :=
  { x := Nat.zero, y := Nat.zero }

이 예제에서는 두 필드 모두 Nat 타입일 것으로 예상됩니다. 함수가 인자 변수를 인자 값으로 대체하여 호출되는 것처럼, PPoint에 Nat 타입을 인자로 제공하면 x와 y 필드가 Nat 타입을 갖는 구조체가 생성됩니다. 이는 인자 이름 α가 인자 타입 Nat으로 대체되었기 때문입니다. Lean에서 타입은 일반적인 표현식이므로, PPoint와 같은 다형적 타입에 인자를 전달하는 데 특별한 문법이 필요하지 않습니다.

정의 또한 타입을 인자로 받을 수 있으며, 이를 통해 다형적이 됩니다. replaceX 함수는 PPoint의 x 필드를 새로운 값으로 대체합니다. replaceX가 모든 다형적 Point에 대해 작동하도록 하려면, 함수 자체가 다형적이어야 합니다. 이는 첫 번째 인자를 점 필드의 타입으로 하고, 이후의 인자들이 첫 번째 인자의 이름을 참조하도록 함으로써 달성됩니다.

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

즉, 인자 point와 newX의 타입이 α를 언급할 때, 이는 첫 번째 인자로 제공된 타입을 참조하는 것입니다. 이는 함수 인자 이름이 함수 본문에서 사용될 때 제공된 값을 참조하는 방식과 유사합니다.

이는 Lean에게 replaceX의 타입을 확인하도록 요청한 다음, replaceX Nat의 타입을 확인하도록 요청함으로써 볼 수 있습니다.

#check (replaceX)

replaceX : (α : Type) → PPoint α → α → PPoint α

이 함수 타입은 첫 번째 인자의 이름을 포함하며, 타입 내의 이후 인자들은 이 이름을 다시 참조합니다. 함수 적용의 값이 함수 본문에서 인자 이름을 제공된 인자 값으로 대체하여 찾아지는 것처럼, 함수 적용의 타입은 함수의 반환 타입에서 인자 이름을 제공된 값으로 대체하여 찾아집니다. 첫 번째 인자인 Nat을 제공하면, 타입의 나머지 부분에 있는 모든 α가 Nat으로 대체됩니다.

#check replaceX Nat

replaceX Nat : PPoint Nat → Nat → PPoint Nat

나머지 인자들은 명시적으로 이름이 지정되지 않았기 때문에, 더 많은 인자가 제공되어도 추가적인 치환은 발생하지 않습니다.

#check replaceX Nat natOrigin

replaceX Nat natOrigin : Nat → PPoint Nat

#check replaceX Nat natOrigin 5

replaceX Nat natOrigin 5 : PPoint Nat

전체 함수 적용 표현식의 타입이 타입을 인자로 전달함으로써 결정되었다는 사실은 그것을 평가하는 능력에 아무런 영향을 미치지 않습니다.

#eval replaceX Nat natOrigin 5

{ x := 5, y := 0 }

다형적 함수는 이름이 지정된 타입 인자를 받고, 이후의 타입들이 그 인자의 이름을 참조함으로써 작동합니다. 하지만 타입 인자만이 이름을 가질 수 있는 특별한 것은 아닙니다. 양수 또는 음수 부호를 나타내는 데이터 타입을 가정해 봅시다.

inductive Sign where
  | pos
  | neg

인자가 부호인 함수를 작성할 수 있습니다. 인자가 양수이면 함수는 Nat을 반환하고, 음수이면 Int를 반환합니다.

def posOrNegThree (s : Sign) :
    match s with | Sign.pos => Nat | Sign.neg => Int :=
  match s with
  | Sign.pos => (3 : Nat)
  | Sign.neg => (-3 : Int)

타입은 일급 객체이며 Lean 언어의 일반적인 규칙을 사용하여 계산될 수 있으므로, 데이터 타입에 대한 패턴 매칭을 통해 계산될 수 있습니다. Lean이 이 함수를 확인할 때, 함수 본문의 match 표현식이 타입의 match 표현식과 일치한다는 사실을 이용하여 pos 케이스의 예상 타입을 Nat으로, neg 케이스의 예상 타입을 Int로 만듭니다.

posOrNegThree를 pos에 적용하면 함수 본문과 반환 타입 모두에서 인자 이름 s가 pos로 대체됩니다. 평가는 표현식과 그 타입 모두에서 발생할 수 있습니다.

(posOrNegThree Sign.pos :
 match Sign.pos with | Sign.pos => Nat | Sign.neg => Int)

  ⟹  \implies

((match Sign.pos with
  | Sign.pos => (3 : Nat)
  | Sign.neg => (-3 : Int)) :
 match Sign.pos with | Sign.pos => Nat | Sign.neg => Int)

  ⟹  \implies

((3 : Nat) : Nat)

  ⟹  \implies

3

1.6.1. 연결 리스트(Linked Lists)

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의 첫 번째 인자는 리스트의 head이고, 두 번째 인자는 tail입니다. nn개의 항목을 포함하는 리스트는 nn개의 cons 생성자를 포함하며, 마지막 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을 0으로 바꾸는 과정입니다. replaceX가 점 필드의 타입을 인자로 받았던 것처럼, length는 리스트 항목의 타입을 인자로 받습니다. 예를 들어, 리스트가 문자열을 포함한다면 첫 번째 인자는 String입니다: length String ["Sourdough", "bread"]. 이는 다음과 같이 계산되어야 합니다.

length String ["Sourdough", "bread"]

  ⟹  \implies

length String (List.cons "Sourdough" (List.cons "bread" List.nil))

  ⟹  \implies

Nat.succ (length String (List.cons "bread" List.nil))

  ⟹  \implies

Nat.succ (Nat.succ (length String List.nil))

  ⟹  \implies

Nat.succ (Nat.succ Nat.zero)

  ⟹  \implies

2

length의 정의는 리스트 항목 타입을 인자로 받기 때문에 다형적이면서 자신을 참조하기 때문에 재귀적입니다. 일반적으로 함수는 데이터의 형태를 따릅니다. 재귀적 데이터 타입은 재귀 함수로 이어지고, 다형적 데이터 타입은 다형적 함수로 이어집니다.

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

xs와 ys와 같은 이름은 관례적으로 알 수 없는 값들의 리스트를 나타내는 데 사용됩니다. 이름의 s는 복수형임을 나타내므로, "x s"와 "y s"가 아닌 "엑시즈(exes)"와 "와이즈(whys)"로 발음됩니다.

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

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

1.6.2. 암시적 인자(Implicit Arguments)

replaceX와 length는 모두 사용하기에 다소 번거로운데, 왜냐하면 타입 인자는 보통 이후의 값들에 의해 유일하게 결정되기 때문입니다. 실제로 대부분의 언어에서 컴파일러는 타입 인자를 스스로 완벽하게 결정할 수 있으며, 사용자로부터 가끔씩만 도움이 필요합니다. 이는 Lean에서도 마찬가지입니다. 함수를 정의할 때 인자를 괄호 대신 중괄호로 감싸서 암시적으로 선언할 수 있습니다. 예를 들어, 암시적 타입 인자를 가진 replaceX 버전은 다음과 같습니다.

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

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

#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에 직접 적용될 수 있습니다.

#eval length primesUnder10

4

표준 라이브러리에서 Lean은 이 함수를 List.length라고 부르는데, 이는 구조체 필드 접근에 사용되는 점(dot) 문법이 리스트의 길이를 찾는 데에도 사용될 수 있음을 의미합니다.

#eval primesUnder10.length

4

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

#check List.length (α := Int)

List.length : List Int → Nat

1.6.3. 더 많은 내장 데이터 타입

Lean의 표준 라이브러리에는 리스트 외에도 다양한 맥락에서 사용할 수 있는 여러 다른 구조체와 귀납적 데이터 타입이 포함되어 있습니다.

1.6.3.1. Option

모든 리스트에 첫 번째 항목이 있는 것은 아닙니다. 어떤 리스트는 비어 있습니다. 컬렉션에 대한 많은 연산은 찾고 있는 것을 찾지 못할 수 있습니다. 예를 들어, 리스트에서 첫 번째 항목을 찾는 함수는 그러한 항목을 찾지 못할 수 있습니다. 따라서 첫 번째 항목이 없었음을 알리는 방법이 있어야 합니다.

많은 언어에는 값의 부재를 나타내는 null 값이 있습니다. Lean은 기존 타입에 특별한 null 값을 부여하는 대신, Option이라는 데이터 타입을 제공하여 다른 타입에 누락된 값을 나타내는 표시자를 부여합니다. 예를 들어, 널 허용 Int는 Option Int로 표현되고, 널 허용 문자열 리스트는 Option (List String) 타입으로 표현됩니다. 널 허용성을 나타내기 위해 새로운 타입을 도입한다는 것은, Option Int가 Int가 예상되는 맥락에서 사용될 수 없기 때문에 타입 시스템이 null 검사를 잊지 않도록 보장한다는 것을 의미합니다.

Option에는 some과 none이라는 두 개의 생성자가 있으며, 각각 기본 타입의 널이 아닌 버전과 널 버전을 나타냅니다. 널이 아닌 생성자인 some은 기본 값을 포함하고, none은 인자를 받지 않습니다:

inductive Option (α : Type) : Type where
  | none : Option α
  | some (val : α) : Option α

Option 타입은 C#이나 Kotlin과 같은 언어의 널 허용 타입과 매우 유사하지만, 동일하지는 않습니다. 이들 언어에서는 만약 어떤 타입(예: Boolean)이 항상 해당 타입의 실제 값(true와 false)을 참조한다면, Boolean? 또는 Nullable<Boolean> 타입은 추가적으로 null 값을 허용합니다. 이를 타입 시스템에서 추적하는 것은 매우 유용합니다. 타입 검사기와 다른 도구들은 프로그래머가 null 검사를 기억하도록 도울 수 있고, 타입 시그니처를 통해 널 허용성을 명시적으로 설명하는 API는 그렇지 않은 것보다 더 많은 정보를 제공합니다. 그러나 이러한 널 허용 타입은 Lean의 Option과 한 가지 매우 중요한 점에서 다릅니다. 바로 여러 계층의 선택성을 허용하지 않는다는 점입니다. Option (Option Int)는 none, some none, 또는 some (some 360)으로 구성될 수 있습니다. 반면에 Kotlin은 T??를 T?와 동일하게 취급합니다. 이 미묘한 차이는 실제로는 거의 관련이 없지만, 때때로 중요할 수 있습니다.

리스트의 첫 번째 항목을 (존재한다면) 찾으려면 List.head?를 사용합니다. 물음표는 이름의 일부이며, C#이나 Kotlin에서 널 허용 타입을 나타내는 데 사용되는 물음표와는 관련이 없습니다. List.head?의 정의에서 밑줄은 리스트의 나머지 부분을 나타내는 데 사용됩니다. 패턴에서 밑줄은 무엇이든 일치시키지만, 일치된 데이터를 참조하기 위한 변수를 도입하지는 않습니다. 이름 대신 밑줄을 사용하는 것은 입력의 일부가 무시된다는 것을 독자에게 명확하게 전달하는 방법입니다.

def List.head? {α : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | y :: _ => some y

Lean의 명명 규칙은 실패할 수 있는 연산을 접미사를 사용하여 그룹으로 정의하는 것입니다. ?는 Option을 반환하는 버전에, !는 유효하지 않은 입력을 제공했을 때 충돌하는 버전에, D는 연산이 실패할 경우 기본값을 반환하는 버전에 사용됩니다. 이 패턴에 따라, List.head는 호출자가 리스트가 비어 있지 않다는 수학적 증거를 제공하도록 요구하고, List.head?는 Option을 반환하며, List.head!는 빈 리스트를 전달받으면 프로그램을 충돌시키고, List.headD는 리스트가 비어 있을 경우 반환할 기본값을 받습니다. 물음표와 느낌표는 특별한 구문이 아니라 이름의 일부인데, 이는 Lean의 명명 규칙이 많은 언어보다 더 자유롭기 때문입니다.

head?는 List 네임스페이스에 정의되어 있으므로, 접근자 표기법으로 사용할 수 있습니다:

#eval primesUnder10.head?

some 2

그러나 빈 리스트에 대해 테스트하려고 하면 두 개의 오류가 발생합니다:

#eval [].head?

don't know how to synthesize implicit argument `α`
  @List.nil ?m.3
context:
⊢ Type ?u.71735

don't know how to synthesize implicit argument `α`
  @_root_.List.head? ?m.3 []
context:
⊢ Type ?u.71735

이는 Lean이 표현식의 타입을 완전히 결정할 수 없었기 때문입니다. 특히, List.head?에 대한 암시적 타입 인자와 List.nil에 대한 암시적 타입 인자를 모두 찾지 못했습니다. Lean의 출력에서 ?m.XYZ는 추론할 수 없었던 프로그램의 일부를 나타냅니다. 이러한 알 수 없는 부분을 메타변수라고 하며, 일부 오류 메시지에 나타납니다. 표현식을 평가하기 위해 Lean은 그 타입을 찾을 수 있어야 하는데, 빈 리스트에는 타입을 찾을 수 있는 항목이 없기 때문에 타입을 사용할 수 없었습니다. 명시적으로 타입을 제공하면 Lean이 진행할 수 있습니다:

#eval [].head? (α := Int)

none

타입은 타입 주석으로도 제공될 수 있습니다:

#eval ([] : List Int).head?

none

오류 메시지는 유용한 단서를 제공합니다. 두 메시지 모두 누락된 암시적 인자를 설명하기 위해 동일한 메타변수를 사용하는데, 이는 Lean이 해결책의 실제 값을 결정할 수는 없었지만 두 누락된 부분이 동일한 해결책을 공유할 것이라고 결정했음을 의미합니다.

1.6.3.2. Prod

"Product"의 약자인 Prod 구조체는 두 값을 함께 묶는 일반적인 방법입니다. 예를 들어, Prod Nat String은 Nat과 String을 포함합니다. 즉, PPoint Nat은 Prod Nat Nat으로 대체될 수 있습니다. Prod는 C#의 튜플, Kotlin의 Pair 및 Triple 타입, C++의 tuple과 매우 유사합니다. 많은 애플리케이션에서는 Point와 같은 간단한 경우에도 자체 구조체를 정의하는 것이 가장 좋습니다. 왜냐하면 도메인 용어를 사용하면 코드를 읽기 쉽게 만들 수 있기 때문입니다. 또한, 구조체 타입을 정의하면 다른 도메인 개념에 다른 타입을 할당하여 서로 섞이는 것을 방지함으로써 더 많은 오류를 잡는 데 도움이 됩니다.

반면에, 새로운 타입을 정의하는 오버헤드가 가치가 없는 경우도 있습니다. 또한, 일부 라이브러리는 "쌍"보다 더 구체적인 개념이 없을 정도로 충분히 일반적입니다. 마지막으로, 표준 라이브러리에는 내장된 쌍 타입을 더 쉽게 다룰 수 있게 해주는 다양한 편의 함수가 포함되어 있습니다.

Prod 구조체는 두 개의 타입 인자로 정의됩니다:

structure Prod (α : Type) (β : Type) : Type where
  fst : α
  snd : β

리스트는 매우 자주 사용되므로 가독성을 높이기 위한 특별한 구문이 있습니다. 같은 이유로, 프로덕트 타입과 그 생성자 모두 특별한 구문을 가지고 있습니다. Prod α β 타입은 일반적으로 α × β로 쓰이며, 이는 집합의 데카르트 곱에 대한 일반적인 표기법을 반영합니다. 마찬가지로, 쌍에 대한 일반적인 수학적 표기법을 Prod에 사용할 수 있습니다. 즉, 다음과 같이 쓰는 대신에:

def fives : String × Int := { fst := "five", snd := 5 }

다음과 같이 쓰는 것으로 충분합니다:

def fives : String × Int := ("five", 5)

두 표기법 모두 오른쪽 결합입니다. 이는 다음 정의들이 동일하다는 것을 의미합니다:

def sevens : String × Int × Nat := ("VII", 7, 4 + 3)
def sevens : String × (Int × Nat) := ("VII", (7, 4 + 3))

즉, 세 개 이상의 타입으로 이루어진 모든 프로덕트와 그에 해당하는 생성자들은 실제로는 내부적으로 중첩된 프로덕트와 중첩된 쌍입니다.

1.6.3.3. Sum

Sum 데이터 타입은 두 가지 다른 타입의 값 사이에서 선택을 허용하는 일반적인 방법입니다. 예를 들어, Sum String Int는 String이거나 Int입니다. Prod와 마찬가지로, Sum은 매우 일반적인 코드를 작성할 때, 합리적인 도메인 특정 타입이 없는 매우 작은 코드 섹션에 대해, 또는 표준 라이브러리에 유용한 함수가 포함되어 있을 때 사용해야 합니다. 대부분의 상황에서는 사용자 정의 귀납적 타입을 사용하는 것이 더 가독성이 좋고 유지보수하기 쉽습니다.

Sum α β 타입의 값은 α 타입의 값에 적용된 생성자 inl이거나 β 타입의 값에 적용된 생성자 inr입니다:

inductive Sum (α : Type) (β : Type) : Type where
  | inl : α → Sum α β
  | inr : β → Sum α β

이 이름들은 각각 "왼쪽 사상(left injection)"과 "오른쪽 사상(right injection)"의 약어입니다. Prod에 데카르트 곱 표기법이 사용되는 것처럼, Sum에는 "동그라미 안의 더하기" 표기법이 사용되므로, α ⊕ β는 Sum α β를 쓰는 또 다른 방법입니다. Sum.inl과 Sum.inr에 대한 특별한 구문은 없습니다.

예를 들어, 애완동물 이름이 개 이름이거나 고양이 이름일 수 있다면, 그들을 위한 타입은 문자열의 합으로 도입될 수 있습니다:

def PetName : Type := String ⊕ String

실제 프로그램에서는, 유익한 생성자 이름을 가진 사용자 정의 귀납적 데이터 타입을 이 목적으로 정의하는 것이 보통 더 좋습니다. 여기서는, Sum.inl은 개 이름에, Sum.inr은 고양이 이름에 사용됩니다. 이 생성자들을 사용하여 동물 이름 목록을 작성할 수 있습니다:

def animals : List PetName :=
  [Sum.inl "Spot", Sum.inr "Tiger", Sum.inl "Fifi",
   Sum.inl "Rex", Sum.inr "Floof"]

패턴 매칭을 사용하여 두 생성자를 구별할 수 있습니다. 예를 들어, 동물 이름 목록에서 개의 수(즉, Sum.inl 생성자의 수)를 세는 함수는 다음과 같습니다:

def howManyDogs (pets : List PetName) : Nat :=
  match pets with
  | [] => 0
  | Sum.inl _ :: morePets => howManyDogs morePets + 1
  | Sum.inr _ :: morePets => howManyDogs morePets

함수 호출은 중위 연산자보다 먼저 평가되므로, howManyDogs morePets + 1은 (howManyDogs morePets) + 1과 같습니다. 예상대로, #eval howManyDogs animals는 3을 산출합니다.

1.6.3.4. Unit

Unit은 unit이라는 단 하나의 인자 없는 생성자를 가진 타입입니다. 즉, 그것은 단 하나의 값만을 설명하며, 이 값은 아무 인자에도 적용되지 않은 해당 생성자로 구성됩니다. Unit은 다음과 같이 정의됩니다:

inductive Unit : Type where
  | unit : Unit

그 자체로 Unit은 특별히 유용하지 않습니다. 그러나 다형성 코드에서는 누락된 데이터를 위한 자리 표시자로 사용될 수 있습니다. 예를 들어, 다음 귀납적 데이터 타입은 산술 표현식을 나타냅니다:

inductive ArithExpr (ann : Type) : Type where
  | int : ann → Int → ArithExpr ann
  | plus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | minus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | times : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann

타입 인자 ann은 주석을 의미하며, 각 생성자는 주석이 달려 있습니다. 파서에서 오는 표현식은 소스 위치로 주석이 달릴 수 있으므로, 반환 타입이 ArithExpr SourcePos이면 파서가 각 하위 표현식에 SourcePos를 넣었음을 보장합니다. 그러나 파서에서 오지 않은 표현식은 소스 위치가 없으므로, 그 타입은 ArithExpr Unit이 될 수 있습니다.

또한, 모든 Lean 함수는 인자를 가지므로, 다른 언어의 인자 없는 함수는 Unit 인자를 받는 함수로 표현될 수 있습니다. 반환 위치에서 Unit 타입은 C에서 파생된 언어의 void와 유사합니다. C 계열에서 void를 반환하는 함수는 호출자에게 제어를 반환하지만, 흥미로운 값을 반환하지는 않습니다. 의도적으로 흥미롭지 않은 값이 됨으로써, Unit은 타입 시스템에 특수 목적의 void 기능이 필요 없이 이를 표현할 수 있게 합니다. Unit의 생성자는 다음과 같이 빈 괄호로 쓸 수 있습니다: () : Unit.

1.6.3.5. Empty

Empty 데이터 타입은 생성자가 전혀 없습니다. 따라서, 어떤 일련의 호출도 Empty 타입의 값으로 끝날 수 없기 때문에 도달할 수 없는 코드를 나타냅니다.

Empty는 Unit만큼 자주 사용되지는 않습니다. 그러나 일부 특수한 맥락에서 유용합니다. 많은 다형성 데이터 타입은 모든 생성자에서 모든 타입 인자를 사용하지는 않습니다. 예를 들어, Sum.inl과 Sum.inr는 각각 Sum의 타입 인자 중 하나만 사용합니다. Sum의 타입 인자 중 하나로 Empty를 사용하면 프로그램의 특정 지점에서 생성자 중 하나를 배제할 수 있습니다. 이를 통해 추가적인 제약이 있는 맥락에서 일반 코드를 사용할 수 있습니다. 1.6.3.6. 이름 짓기: 합, 곱, 그리고 유닛 🔗

일반적으로, 여러 생성자를 제공하는 타입을 합 타입(sum type)이라고 하고, 단일 생성자가 여러 인자를 받는 타입을 곱 타입(product type)이라고 합니다. 이 용어들은 일반 산술에서 사용되는 합과 곱과 관련이 있습니다. 이 관계는 관련된 타입들이 유한한 수의 값을 포함할 때 가장 쉽게 볼 수 있습니다. 만약 α와 β가 각각 n개와 k개의 서로 다른 값을 포함하는 타입이라면, α ⊕ β는 n+k개의 서로 다른 값을 포함하고 α × β는 n×k개의 서로 다른 값을 포함합니다. 예를 들어, Bool은 true와 false 두 개의 값을 가지고, Unit은 Unit.unit이라는 하나의 값을 가집니다. 곱 Bool × Unit은 (true, Unit.unit)과 (false, Unit.unit) 두 개의 값을 가지고, 합 Bool ⊕ Unit은 Sum.inl true, Sum.inl false, Sum.inr Unit.unit 세 개의 값을 가집니다. 마찬가지로, 2×1=2이고, 2+1=3입니다.

1.6.4. 마주칠 수 있는 메시지들

정의 가능한 모든 구조체나 귀납적 타입이 Type 타입을 가질 수 있는 것은 아닙니다. 특히, 생성자가 임의의 타입을 인자로 받는 경우, 귀납적 타입은 다른 타입을 가져야 합니다. 이러한 오류는 보통 "유니버스 레벨"에 대한 무언가를 명시합니다. 예를 들어, 이 귀납적 타입에 대해:

inductive MyType : Type where
  | 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

이것이 왜 그런지, 그리고 정의를 수정하여 작동하게 만드는 방법은 나중 장에서 설명합니다. 지금은 타입을 생성자에 대한 인자가 아닌 귀납적 타입 전체에 대한 인자로 만들어 보세요.

마찬가지로, 생성자의 인자가 정의되고 있는 데이터 타입을 인자로 받는 함수인 경우, 정의는 거부됩니다. 예를 들어:

inductive 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 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 : α → MyType

Lean은 다음 오류로 응답합니다:

type expected, got
  (MyType : Type → Type)

오류 메시지는 MyType의 타입인 Type → Type이 그 자체로는 타입을 설명하지 않는다고 말하고 있습니다. MyType은 실제 정직한 타입이 되기 위해 인자가 필요합니다.

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

inductive MyType (α : Type) : Type where
  | ctor : α → MyType α
def ofFive : MyType := ctor 5

type expected, got
  (MyType : Type → Type)

다형성 타입을 사용하는 표현식을 평가하면 Lean이 값을 표시할 수 없는 상황이 발생할 수 있습니다. #eval 명령어는 제공된 표현식을 평가하고, 표현식의 타입을 사용하여 결과를 표시하는 방법을 결정합니다. 함수와 같은 일부 타입의 경우 이 과정이 실패하지만, Lean은 대부분의 다른 타입에 대해 표시 코드를 자동으로 생성할 수 있습니다. 예를 들어, WoodSplittingTool에 대해 Lean에 특정 표시 코드를 제공할 필요가 없습니다:

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

WoodSplittingTool.axe

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

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

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

#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
]
#eval allFirewood

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

1.6.5. 연습 문제

• 리스트의 마지막 항목을 찾는 함수를 작성하세요. 이 함수는 Option을 반환해야 합니다.
• 주어진 술어를 만족하는 리스트의 첫 번째 항목을 찾는 함수를 작성하세요. 정의는 다음처럼 시작해야합니다:

  def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α :=

• 쌍의 두 필드를 서로 바꾸는 Prod.switch 함수를 작성하세요. 정의는 다음처럼 시작해야합니다:

  def Prod.switch {α β : Type} (pair : α × β) : β × α :=

• PetName 예제를 사용자 정의 데이터 타입을 사용하도록 다시 작성하고 Sum을 사용한 버전과 비교해 보세요.
• 두 리스트를 쌍의 리스트로 결합하는 zip 함수를 작성하세요. 결과 리스트는 가장 짧은 입력 리스트의 길이와 같아야 합니다. 정의는 다음처럼 시작해야합니다:

  def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=

• 리스트의 첫 n개 항목을 반환하는 다형성 함수 take를 작성하세요. 여기서 n은 Nat입니다. 리스트에 n개 미만의 항목이 포함된 경우, 결과 리스트는 전체 입력 리스트여야 합니다. #eval take 3 ["bolete", "oyster"]는 ["bolete", "oyster"]를 산출해야 하고, #eval take 1 ["bolete", "oyster"]는 ["bolete"]를 산출해야 합니다.
• 타입과 산술 사이의 유추를 사용하여, 곱을 합에 대해 분배하는 함수를 작성하세요. 즉, 이 함수는 α × (β ⊕ γ) → (α × β) ⊕ (α × γ) 타입을 가져야 합니다.
• 타입과 산술 사이의 유추를 사용하여, 2를 곱하는 것을 합으로 바꾸는 함수를 작성하세요. 즉, 이 함수는 Bool × α → α ⊕ α 타입을 가져야 합니다.

1.7. 추가적인 편의 기능

Lean에는 프로그램을 훨씬 더 간결하게 만들어주는 여러 편의 기능이 포함되어 있습니다.

1.7.1. 자동 암시적 매개변수

Lean에서 다형성 함수를 작성할 때, 일반적으로 모든 암시적 매개변수를 나열할 필요는 없습니다. 대신, 그냥 언급하기만 하면 됩니다. Lean이 그 타입을 결정할 수 있다면, 해당 매개변수들은 자동으로 암시적 매개변수로 삽입됩니다. 다시 말해, 이전에 정의했던 length는 다음과 같습니다.

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

이 정의는 {α : Type} 없이도 작성할 수 있습니다.

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

이 기능은 많은 암시적 매개변수를 사용하는 고도로 다형적인 정의를 크게 단순화할 수 있습니다.

1.7.2. 패턴 매칭 정의

def로 함수를 정의할 때, 인자의 이름을 지정한 후 바로 패턴 매칭에 사용하는 것이 매우 흔합니다. 예를 들어, length에서 인자 xs는 match에서만 사용됩니다. 이런 상황에서는 인자의 이름을 전혀 지정하지 않고 match 표현식의 케이스들을 직접 작성할 수 있습니다.

첫 번째 단계는 인자의 타입을 콜론 오른쪽으로 옮겨서 반환 타입이 함수 타입이 되도록 하는 것입니다. 예를 들어, length의 타입은 List α → Nat입니다. 그런 다음, :=를 각 패턴 매칭 케이스로 대체합니다.

def length : List α → Nat
  | [] => 0
  | y :: ys => Nat.succ (length ys)

이 구문은 하나 이상의 인자를 받는 함수를 정의하는 데에도 사용할 수 있습니다. 이 경우, 패턴들은 쉼표로 구분됩니다. 예를 들어, drop은 숫자 nn과 리스트를 받아 처음 nn개의 항목을 제거한 후의 리스트를 반환합니다.

def drop : Nat → List α → List α
  | Nat.zero, xs => xs
  | _, [] => []
  | Nat.succ n, x :: xs => drop n xs

이름이 지정된 인자와 패턴을 같은 정의 안에서 함께 사용할 수도 있습니다. 예를 들어, 기본값과 옵셔널 값을 받아 옵셔널 값이 none일 때 기본값을 반환하는 함수는 다음과 같이 작성할 수 있습니다.

def fromOption (default : α) : Option α → α
  | none => default
  | some x => x

이 함수는 표준 라이브러리에서 Option.getD라고 불리며, 점 표기법으로 호출할 수 있습니다.

#eval (some "salmonberry").getD ""

"salmonberry"

#eval none.getD ""

""

1.7.3. 지역 정의

계산 과정에서 중간 단계를 명명하는 것은 종종 유용합니다. 많은 경우, 중간값들은 그 자체로 유용한 개념을 나타내며, 이를 명시적으로 명명하면 프로그램을 더 읽기 쉽게 만들 수 있습니다. 다른 경우에는 중간값이 두 번 이상 사용됩니다. 대부분의 다른 언어와 마찬가지로, Lean에서 동일한 코드를 두 번 작성하면 두 번 계산되지만, 결과를 변수에 저장하면 계산 결과가 저장되어 재사용됩니다.

예를 들어, unzip은 쌍의 리스트를 리스트의 쌍으로 변환하는 함수입니다. 쌍의 리스트가 비어 있으면, unzip의 결과는 빈 리스트의 쌍입니다. 쌍의 리스트가 머리에 쌍을 가지고 있으면, 그 쌍의 두 필드는 리스트의 나머지 부분을 unzip한 결과에 추가됩니다. 이 unzip의 정의는 그 설명을 정확히 따릅니다.

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    (x :: (unzip xys).fst, y :: (unzip xys).snd)

불행히도, 문제가 있습니다. 이 코드는 필요 이상으로 느립니다. 쌍의 리스트에 있는 각 항목은 두 번의 재귀 호출로 이어져, 이 함수가 지수 시간을 소요하게 만듭니다. 하지만 두 재귀 호출은 모두 같은 결과를 낼 것이므로, 재귀 호출을 두 번 할 이유가 없습니다.

Lean에서는 let을 사용하여 재귀 호출의 결과를 명명하고 저장할 수 있습니다. let을 사용한 지역 정의는 def를 사용한 최상위 정의와 유사합니다. 지역적으로 정의될 이름, 원한다면 인자, 타입 시그니처, 그리고 := 뒤에 오는 본문을 가집니다. 지역 정의 후, 해당 지역 정의가 사용 가능한 표현식(let 표현식의 본문)은 let 키워드의 열보다 작거나 같은 열에서 시작하는 새 줄에 있어야 합니다. unzip에서 let을 사용한 지역 정의는 다음과 같습니다.

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped : List α × List β := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

let을 한 줄에서 사용하려면, 지역 정의와 본문을 세미콜론으로 구분합니다.

let을 사용한 지역 정의는 데이터 타입의 모든 케이스를 하나의 패턴으로 매칭할 수 있을 때 패턴 매칭을 사용할 수도 있습니다. unzip의 경우, 재귀 호출의 결과는 쌍입니다. 쌍은 단 하나의 생성자만 가지므로, unzipped라는 이름을 쌍 패턴으로 대체할 수 있습니다.

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let (xs, ys) : List α × List β := unzip xys
    (x :: xs, y :: ys)

let과 함께 패턴을 적절히 사용하면, 접근자 호출을 직접 작성하는 것보다 코드를 더 읽기 쉽게 만들 수 있습니다.

let과 def의 가장 큰 차이점은 재귀적인 let 정의는 let rec을 작성하여 명시적으로 표시해야 한다는 것입니다. 예를 들어, 리스트를 뒤집는 한 가지 방법은 다음과 같이 재귀적인 헬퍼 함수를 포함합니다.

def reverse (xs : List α) : List α :=
  let rec helper : List α → List α → List α
    | [], soFar => soFar
    | y :: ys, soFar => helper ys (y :: soFar)
  helper xs []

헬퍼 함수는 입력 리스트를 따라 내려가면서 한 번에 하나의 항목을 soFar로 옮깁니다. 입력 리스트의 끝에 도달하면, soFar는 입력의 뒤집힌 버전을 담고 있습니다.

1.7.4. 타입 추론

많은 상황에서 Lean은 표현식의 타입을 자동으로 결정할 수 있습니다. 이런 경우, 명시적인 타입은 최상위 정의(def 사용)와 지역 정의(let 사용) 모두에서 생략될 수 있습니다. 예를 들어, unzip에 대한 재귀 호출은 어노테이션이 필요하지 않습니다.

def unzip : List (α × β) → List α × List β
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

경험적으로, 문자열이나 숫자와 같은 리터럴 값의 타입을 생략하는 것은 보통 잘 작동하지만, Lean이 리터럴 숫자에 대해 의도한 타입보다 더 구체적인 타입을 선택할 수 있습니다. Lean은 함수 적용에 대한 타입을 보통 결정할 수 있는데, 이는 이미 인자 타입과 반환 타입을 알고 있기 때문입니다. 함수 정의의 반환 타입을 생략하는 것은 종종 작동하지만, 함수 매개변수는 일반적으로 어노테이션이 필요합니다. 예제의 unzipped와 같이 함수가 아닌 정의는, 그 본문이 타입 어노테이션을 필요로 하지 않는다면 타입 어노테이션이 필요 없으며, 이 정의의 본문은 함수 적용입니다.

명시적인 match 표현식을 사용할 때 unzip의 반환 타입을 생략하는 것이 가능합니다.

def unzip (pairs : List (α × β)) :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

일반적으로, 타입 어노테이션은 적은 것보다 많은 편이 좋습니다. 첫째, 명시적인 타입은 코드에 대한 가정을 독자에게 전달합니다. Lean이 스스로 타입을 결정할 수 있더라도, Lean에게 반복적으로 타입 정보를 묻지 않고 코드를 읽는 것이 더 쉬울 수 있습니다. 둘째, 명시적인 타입은 오류를 국소화하는 데 도움이 됩니다. 프로그램이 타입에 대해 더 명시적일수록 오류 메시지가 더 유익할 수 있습니다. 이는 Lean과 같이 매우 표현력이 풍부한 타입 시스템을 가진 언어에서 특히 중요합니다. 셋째, 명시적인 타입은 애초에 프로그램을 작성하기 쉽게 만듭니다. 타입은 명세이며, 컴파일러의 피드백은 명세를 충족하는 프로그램을 작성하는 데 유용한 도구가 될 수 있습니다. 마지막으로, Lean의 타입 추론은 최선 노력 시스템입니다. Lean의 타입 시스템이 매우 표현력이 풍부하기 때문에, 모든 표현식에 대해 "최고의" 또는 가장 일반적인 타입을 찾는 것은 불가능합니다. 이는 타입을 얻더라도 주어진 애플리케이션에 맞는 올바른 타입이라는 보장이 없다는 것을 의미합니다. 예를 들어, 14는 Nat 또는 Int가 될 수 있습니다.

#check 14

14 : Nat

#check (14 : Int)

14 : Int

타입 어노테이션이 누락되면 혼란스러운 오류 메시지가 나타날 수 있습니다. unzip 정의에서 모든 타입을 생략하면 다음과 같습니다.

def unzip pairs :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

이는 match 표현식에 대한 메시지로 이어집니다.

Invalid match expression: This pattern contains metavariables:
  []

이는 match가 검사되는 값의 타입을 알아야 하지만, 그 타입이 제공되지 않았기 때문입니다. "메타변수"는 프로그램의 알 수 없는 부분으로, 오류 메시지에서는 ?m.XYZ로 표시되며, 다형성 섹션에서 설명됩니다. 이 프로그램에서는 인자에 대한 타입 어노테이션이 필요합니다.

매우 간단한 프로그램조차도 타입 어노테이션이 필요할 수 있습니다. 예를 들어, 항등 함수는 전달된 인자를 그대로 반환합니다. 인자와 타입 어노테이션을 사용하면 다음과 같습니다.

def id (x : α) : α := x

Lean은 반환 타입을 스스로 결정할 수 있습니다.

def id (x : α) := x

하지만 인자 타입을 생략하면 오류가 발생합니다.

def id x := x

Failed to infer type of binder `x`

일반적으로, "failed to infer"와 같은 메시지나 메타변수를 언급하는 메시지는 더 많은 타입 어노테이션이 필요하다는 신호일 수 있습니다. 특히 Lean을 배우는 동안에는 대부분의 타입을 명시적으로 제공하는 것이 유용합니다.

1.7.5. 동시 매칭

패턴 매칭 표현식은 패턴 매칭 정의와 마찬가지로 여러 값을 한 번에 매칭할 수 있습니다. 검사할 표현식과 그에 대응하는 패턴 모두 정의에 사용된 구문과 유사하게 쉼표로 구분하여 작성됩니다. 다음은 동시 매칭을 사용하는 방식의 drop입니다.

def drop (n : Nat) (xs : List α) : List α :=
  match n, xs with
  | Nat.zero, ys => ys
  | _, [] => []
  | Nat.succ n , y :: ys => drop n ys

동시 매칭은 쌍에 대한 매칭과 유사하지만, 중요한 차이점이 있습니다. Lean은 매칭되는 표현식과 패턴 사이의 연결을 추적하며, 이 정보는 종료 검사 및 정적 타입 정보 전파와 같은 목적에 사용됩니다. 결과적으로, 쌍을 매칭하는 방식의 sameLength은 종료 검사기에 의해 거부됩니다. 왜냐하면 xs와 x :: xs' 사이의 연결이 중간에 있는 쌍에 의해 가려지기 때문입니다.

def 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, ys with
  | [], [] => true
  | x :: xs', y :: ys' => sameLength xs' ys'
  | _, _ => false

1.7.6. 자연수 패턴

데이터 타입과 패턴에 대한 섹션에서, even은 다음과 같이 정의되었습니다:

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

List.cons와 List.nil을 직접 사용하는 것보다 리스트 패턴을 더 읽기 쉽게 만드는 특별한 구문이 있는 것처럼, 자연수도 리터럴 숫자와 +를 사용하여 매칭할 수 있습니다. 예를 들어, even은 다음과 같이 정의할 수도 있습니다:

def even : Nat → Bool
  | 0 => true
  | n + 1 => not (even n)

이 표기법에서 + 패턴의 인자들은 서로 다른 역할을 합니다. 내부적으로 왼쪽 인자(위의 n)는 여러 Nat.succ 패턴의 인자가 되고, 오른쪽 인자(위의 1)는 패턴을 감쌀 Nat.succ의 개수를 결정합니다. Nat을 2로 나누고 나머지를 버리는 halve의 명시적 패턴은 다음과 같습니다:

def halve : Nat → Nat
  | Nat.zero => 0
  | Nat.succ Nat.zero => 0
  | Nat.succ (Nat.succ n) => halve n + 1

이는 숫자 리터럴과 +로 대체될 수 있습니다:

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | n + 2 => halve n + 1

내부적으로 두 정의는 완전히 동일합니다. 기억하세요: halve n + 1은 halve (n + 1)이 아니라 (halve n) + 1과 동일합니다.

이 구문을 사용할 때, +의 두 번째 인자는 항상 리터럴 Nat이어야 합니다. 덧셈은 교환 법칙이 성립하지만, 패턴에서 인자의 순서를 바꾸면 다음과 같은 오류가 발생할 수 있습니다:

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | 2 + n => halve n + 1

Invalid pattern(s): `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching:
  .(Nat.add 2 n)

이 제약 덕분에 Lean은 패턴에서 사용되는 모든 + 표기법을 내부적인 Nat.succ 사용으로 변환할 수 있으며, 이는 언어의 내부를 더 단순하게 유지해 줍니다.

1.7.7. 익명 함수

Lean의 함수는 최상위 수준에서 정의될 필요가 없습니다. 표현식으로서의 함수는 fun 구문을 사용하여 생성됩니다. 함수 표현식은 fun 키워드로 시작하며, 하나 이상의 매개변수가 뒤따르고, =>를 사용하여 반환 표현식과 구분됩니다. 예를 들어, 숫자에 1을 더하는 함수는 다음과 같이 작성할 수 있습니다:

#check fun x => x + 1

fun x => x + 1 : Nat → Nat

타입 주석은 def에서와 같은 방식으로 괄호와 콜론을 사용하여 작성됩니다:

#check fun (x : Int) => x + 1

fun x => x + 1 : Int → Int

마찬가지로, 암시적 매개변수는 중괄호를 사용하여 작성할 수 있습니다:

#check fun {α : Type} (x : α) => x

fun {α} x => x : {α : Type} → α → α

이러한 스타일의 익명 함수 표현식은 종종 람다 표현식이라고 불립니다. 이는 프로그래밍 언어의 수학적 설명에서 사용되는 일반적인 표기법이 Lean의 fun 키워드 자리에 그리스 문자 λ(람다)를 사용하기 때문입니다. Lean이 fun 대신 λ를 사용하는 것을 허용하긴 하지만, fun을 쓰는 것이 가장 일반적입니다.

익명 함수는 def에서 사용되는 다중 패턴 스타일도 지원합니다. 예를 들어, 자연수의 이전 수를 (존재하는 경우) 반환하는 함수는 다음과 같이 작성할 수 있습니다:

#check fun
  | 0 => none
  | n + 1 => some n

fun x =>
  match x with
  | 0 => none
  | n.succ => some n : Nat → Option Nat

Lean이 함수를 설명할 때 이름 있는 인자와 match 표현식을 사용한다는 점에 유의하세요. Lean의 편리한 구문적 축약형 중 다수는 내부적으로 더 간단한 구문으로 확장되며, 때로는 이러한 추상화가 드러나기도 합니다.

인자를 받는 def를 사용한 정의는 함수 표현식으로 다시 작성될 수 있습니다. 예를 들어, 인자를 두 배로 만드는 함수는 다음과 같이 작성할 수 있습니다:

def double : Nat → Nat := fun
  | 0 => 0
  | k + 1 => double k + 2

fun x => x + 1과 같이 익명 함수가 매우 간단할 때, 함수를 만드는 구문은 상당히 장황할 수 있습니다. 이 특정 예에서는 함수를 도입하는 데 6개의 공백이 아닌 문자가 사용되었고, 본문은 3개의 공백이 아닌 문자로만 구성됩니다. 이러한 간단한 경우를 위해 Lean은 축약형을 제공합니다. 괄호로 둘러싸인 표현식에서 ·(MIDDLE DOT)는 매개변수를 나타낼 수 있으며, 괄호 안의 표현식은 함수의 본문이 됩니다. 이 특정 함수는 (· + 1)로도 작성할 수 있습니다.

·은 항상 가장 가까운 괄호 세트로부터 함수를 만듭니다. 예를 들어, (· + 5, 3)은 숫자 쌍을 반환하는 함수인 반면, ((· + 5), 3)은 함수와 숫자로 이루어진 쌍입니다. 여러 개의 점이 사용되면 왼쪽에서 오른쪽 순서로 매개변수가 됩니다:

(· , ·) 1 2
(1, ·) 2
(1, 2)

익명 함수는 def나 let을 사용하여 정의된 함수와 정확히 같은 방식으로 적용될 수 있습니다. #eval (fun x => x + x) 5 명령어는 다음을 결과로 냅니다:

10

반면 #eval (· * 2) 5는 다음을 결과로 냅니다:

10

1.7.8. 네임스페이스

Lean의 각 이름은 이름의 모음인 네임스페이스 안에 존재합니다. 이름은 .을 사용하여 네임스페이스에 배치되므로, List.map은 List 네임스페이스에 있는 map이라는 이름입니다. 서로 다른 네임스페이스에 있는 이름들은 다른 부분이 동일하더라도 서로 충돌하지 않습니다. 이는 List.map과 Array.map이 다른 이름임을 의미합니다. 네임스페이스는 중첩될 수 있으므로, Project.Frontend.User.loginTime은 중첩된 Project.Frontend.User 네임스페이스에 있는 loginTime이라는 이름입니다.

이름은 네임스페이스 내에서 직접 정의될 수 있습니다. 예를 들어, double이라는 이름은 Nat 네임스페이스에 다음과 같이 정의할 수 있습니다:

def Nat.double (x : Nat) : Nat := x + x

Nat은 타입의 이름이기도 하므로, Nat 타입의 표현식에 Nat.double을 호출하기 위해 점 표기법을 사용할 수 있습니다:

#eval (4 : Nat).double

8

네임스페이스에 직접 이름을 정의하는 것 외에도, namespace와 end 명령어를 사용하여 일련의 선언들을 네임스페이스에 배치할 수 있습니다. 예를 들어, 다음은 NewNamespace라는 네임스페이스에 triple과 quadruple을 정의합니다:

namespace NewNamespace
def triple (x : Nat) : Nat := 3 * x
def quadruple (x : Nat) : Nat := 2 * x + 2 * x
end NewNamespace

이들을 참조하려면 이름 앞에 NewNamespace.를 붙입니다:

#check NewNamespace.triple

NewNamespace.triple (x : Nat) : Nat

#check NewNamespace.quadruple

NewNamespace.quadruple (x : Nat) : Nat

네임스페이스는 open할 수 있으며, 이를 통해 네임스페이스 안의 이름들을 명시적인 한정자 없이 사용할 수 있습니다. 표현식 앞에 open MyNamespace in을 작성하면 MyNamespace의 내용이 해당 표현식에서 사용 가능해집니다. 예를 들어, timesTwelve는 NewNamespace를 연 후에 quadruple과 triple을 모두 사용합니다:

def timesTwelve (x : Nat) :=
  open NewNamespace in
  quadruple (triple x)

네임스페이스는 명령어 앞에서도 열 수 있습니다. 이를 통해 단일 표현식뿐만 아니라 명령어의 모든 부분에서 네임스페이스의 내용을 참조할 수 있습니다. 이렇게 하려면 명령어 앞에 open ... in을 배치합니다.

open NewNamespace in
#check quadruple

NewNamespace.quadruple (x : Nat) : Nat

함수 시그니처는 이름의 전체 네임스페이스를 보여줍니다. 네임스페이스는 파일의 나머지 부분에 대해 이후의 모든 명령어에 대해 추가적으로 열릴 수도 있습니다. 이렇게 하려면 최상위 수준에서 open을 사용할 때 in을 생략하면 됩니다.

1.7.9. if let

합 타입을 갖는 값을 사용할 때, 종종 단 하나의 생성자에만 관심이 있는 경우가 많습니다. 예를 들어, 마크다운 인라인 요소의 일부를 나타내는 다음 타입이 주어졌을 때:

inductive Inline : Type where
  | lineBreak
  | string : String → Inline
  | emph : Inline → Inline
  | strong : Inline → Inline

문자열 요소를 인식하고 그 내용을 추출하는 함수는 다음과 같이 작성할 수 있습니다:

def Inline.string? (inline : Inline) : Option String :=
  match inline with
  | Inline.string s => some s
  | _ => none

이 함수의 본문을 작성하는 다른 방법은 if와 let을 함께 사용하는 것입니다:

def Inline.string? (inline : Inline) : Option String :=
  if let Inline.string s := inline then
    some s
  else none

이것은 패턴 매칭 let 구문과 매우 유사합니다. 차이점은 else 경우에 대체 방안이 제공되기 때문에 합 타입과 함께 사용할 수 있다는 것입니다. 일부 문맥에서는 match 대신 if let을 사용하면 코드를 더 읽기 쉽게 만들 수 있습니다.

1.7.10. 위치 기반 구조체 인자

구조체에 대한 섹션에서는 구조체를 생성하는 두 가지 방법을 제시합니다:

1. Point.mk 1 2 같은 생성자 직접 호출.
2. { x := 1, y := 2 } 같은 중괄호 표기법.

어떤 문맥에서는 생성자를 직접 명명하지 않고, 이름 대신 위치에 따라 인자를 전달하는 것이 편리할 수 있습니다. 예를 들어, 다양한 유사한 구조체 타입을 정의하면 도메인 개념을 분리하는 데 도움이 될 수 있지만, 코드를 자연스럽게 읽는 방식은 각각을 본질적으로 튜플로 취급할 수 있습니다. 이러한 문맥에서는 인자를 꺾쇠괄호 ⟨와 ⟩로 묶을 수 있습니다. Point는 ⟨1, 2⟩로 작성할 수 있습니다. 조심하세요! 이 괄호들은 부등호 <와 >처럼 보이지만 다른 문자입니다. 각각 \<와 \>를 사용하여 입력할 수 있습니다.

이름 있는 생성자 인자를 위한 중괄호 표기법과 마찬가지로, 이 위치 기반 구문은 Lean이 타입 주석이나 프로그램의 다른 타입 정보로부터 구조체의 타입을 결정할 수 있는 문맥에서만 사용할 수 있습니다. 예를 들어, #eval ⟨1, 2⟩는 다음과 같은 오류를 발생시킵니다:

Invalid `⟨...⟩` notation: The expected type of this term could not be determined

이 오류는 사용 가능한 타입 정보가 없기 때문에 발생합니다. #eval (⟨1, 2⟩ : Point)와 같이 주석을 추가하면 문제가 해결됩니다:

{ x := 1.000000, y := 2.000000 }

1.7.11. 문자열 보간

Lean에서 문자열 앞에 s!를 붙이면 보간이 활성화되어, 문자열 안의 중괄호에 포함된 표현식이 그 값으로 대체됩니다. 이는 파이썬의 f-string이나 C# 의 $-접두사 문자열과 유사합니다. 예를 들어,

#eval s!"three fives is {NewNamespace.triple 5}"

는 다음을 출력합니다:

"three fives is 15"

모든 표현식이 문자열에 보간될 수 있는 것은 아닙니다. 예를 들어, 함수를 보간하려고 하면 오류가 발생합니다.

#check s!"three fives is {NewNamespace.triple}"

는 다음 오류를 발생시킵니다:

failed to synthesize
  ToString (Nat → Nat)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

이는 함수를 문자열로 변환하는 표준적인 방법이 없기 때문입니다. 컴파일러가 다양한 타입의 표현식 평가 결과를 표시하는 방법을 설명하는 테이블을 유지하는 것처럼, 다양한 타입의 값을 문자열로 변환하는 방법을 설명하는 테이블을 유지합니다. failed to synthesize instance라는 메시지는 Lean 컴파일러가 주어진 타입에 대해 이 테이블에서 항목을 찾지 못했음을 의미합니다. 타입 클래스에 대한 장에서는 테이블에 새 항목을 추가하는 방법을 포함하여 이 메커니즘을 더 자세히 설명합니다.

1.8. 요약

1.8.1. 표현식 평가

Lean에서 계산은 표현식이 평가될 때 발생합니다. 이는 일반적인 수학 표현식의 규칙을 따릅니다. 즉, 전체 표현식이 값이 될 때까지 하위 표현식은 일반적인 연산 순서에 따라 해당 값으로 대체됩니다. if나 match를 평가할 때, 조건이나 match 대상의 값이 발견될 때까지 분기 내의 표현식은 평가되지 않습니다.

변수는 일단 값을 할당받으면 절대 변경되지 않습니다. 수학과 유사하지만 대부분의 프로그래밍 언어와는 달리, Lean의 변수는 새로운 값을 쓸 수 있는 주소라기보다는 단순히 값을 위한 자리 표시자입니다. 변수의 값은 def를 사용한 전역 정의, let을 사용한 지역 정의, 함수의 명명된 인수 또는 패턴 매칭에서 올 수 있습니다.

1.8.2. 함수

Lean에서 함수는 일급 값입니다. 즉, 다른 함수에 인수로 전달되거나, 변수에 저장되거나, 다른 값처럼 사용될 수 있습니다. 모든 Lean 함수는 정확히 하나의 인수를 받습니다. 둘 이상의 인수를 받는 함수를 인코딩하기 위해 Lean은 커링(currying)이라는 기법을 사용하는데, 첫 번째 인수를 제공하면 나머지 인수를 기대하는 함수를 반환합니다. 인수를 받지 않는 함수를 인코딩하기 위해 Lean은 가능한 가장 정보가 적은 인수인 Unit 타입을 사용합니다.

함수를 만드는 주요 방법은 세 가지가 있습니다.

1. 익명 함수는 fun을 사용하여 작성됩니다. 예를 들어, Point의 필드를 바꾸는 함수는 fun (point : Point) => { x := point.y, y := point.x : Point }와 같이 작성할 수 있습니다.
2. 매우 간단한 익명 함수는 괄호 안에 하나 이상의 ·을 배치하여 작성됩니다. 각 가운데 점은 함수의 인수가 되고, 괄호는 함수의 본문을 구분합니다. 예를 들어, 인수에서 1을 빼는 함수는 fun x => x - 1 대신 (· - 1)로 작성할 수 있습니다.
3. 함수는 인수 목록을 추가하거나 패턴 매칭 표기법을 사용하여 def 또는 let으로 정의할 수 있습니다.

1.8.3. 타입

Lean은 모든 표현식에 타입이 있는지 확인합니다. Int, Point, {α : Type} → Nat → α → List α, 그리고 Option (String ⊕ (Nat × String))과 같은 타입은 표현식에 대해 최종적으로 발견될 수 있는 값을 설명합니다. 다른 언어와 마찬가지로 Lean의 타입은 Lean 컴파일러에 의해 확인되는 프로그램의 가벼운 명세를 표현할 수 있어, 특정 종류의 단위 테스트 필요성을 없애줍니다. 대부분의 언어와 달리, Lean의 타입은 임의의 수학도 표현할 수 있어 프로그래밍과 정리 증명의 세계를 통합합니다. 이 책에서는 정리 증명을 위해 Lean을 사용하는 것은 대부분 다루지 않지만, Theorem Proving in Lean 4에서 이 주제에 대한 더 많은 정보를 찾을 수 있습니다.

일부 표현식에는 여러 타입이 주어질 수 있습니다. 예를 들어, 3은 Int 또는 Nat가 될 수 있습니다. Lean에서는 이를 같은 것에 대한 두 가지 다른 타입이 아니라, 우연히 같은 방식으로 작성된, 하나는 Nat 타입이고 다른 하나는 Int 타입인 두 개의 별도 표현식으로 이해해야 합니다.

Lean은 때때로 타입을 자동으로 결정할 수 있지만, 종종 사용자가 타입을 제공해야 합니다. 이는 Lean의 타입 시스템이 매우 표현력이 풍부하기 때문입니다. Lean이 타입을 찾을 수 있더라도 원하는 타입을 찾지 못할 수 있습니다. 예를 들어 3은 Int로 사용될 의도였을 수 있지만, 추가적인 제약 조건이 없다면 Lean은 Nat 타입을 부여할 것입니다. 일반적으로, 대부분의 타입은 명시적으로 작성하고, 아주 명백한 타입만 Lean이 채우도록 하는 것이 좋습니다. 이는 Lean의 오류 메시지를 개선하고 프로그래머의 의도를 더 명확하게 하는 데 도움이 됩니다.

일부 함수나 데이터 타입은 타입을 인수로 받습니다. 이런 특성을 다형성(polymorphic)이라고 합니다. 다형성은 리스트의 항목 타입에 상관없이 리스트의 길이를 계산하는 것과 같은 프로그램을 가능하게 합니다. Lean에서는 타입이 일급 값이기 때문에 다형성은 특별한 구문을 필요로 하지 않으므로, 타입은 다른 인수와 마찬가지로 전달됩니다. 함수 타입에서 인수에 이름을 지정하면 나중의 타입에서 그 이름을 참조할 수 있으며, 함수가 인수에 적용될 때 결과 항의 타입은 인수의 이름이 적용된 실제 값으로 대체되어 찾아집니다.

1.8.4. 구조체와 귀납적 타입

structure 또는 inductive 기능을 사용하여 Lean에 새로운 데이터 타입을 도입할 수 있습니다. 이 새로운 타입은 정의가 동일하더라도 다른 어떤 타입과도 동등하다고 간주되지 않습니다. 데이터 타입에는 해당 값들이 생성될 수 있는 방법을 설명하는 생성자가 있으며, 각 생성자는 여러 개의 인수를 받습니다. Lean의 생성자는 객체 지향 언어의 생성자와 다릅니다. Lean의 생성자는 할당된 객체를 초기화하는 능동적인 코드가 아니라, 데이터를 담고 있는 비활성 홀더입니다.

일반적으로 structure는 곱 타입(즉, 여러 인수를 받는 단 하나의 생성자를 가진 타입)을 도입하는 데 사용되고, inductive는 합 타입(즉, 여러 개의 고유한 생성자를 가진 타입)을 도입하는 데 사용됩니다. structure로 정의된 데이터 타입에는 각 필드에 대한 접근자 함수가 하나씩 제공됩니다. 구조체와 귀납적 데이터 타입 모두 패턴 매칭으로 소비될 수 있으며, 이는 해당 생성자를 호출하는 데 사용된 구문의 일부를 사용하여 생성자 내부에 저장된 값을 노출합니다. 패턴 매칭은 값을 만드는 방법을 아는 것이 곧 그 값을 소비하는 방법을 아는 것을 의미합니다.

1.8.5. 재귀

재귀적이라는 말은 정의되는 이름이 정의 자체에서 사용되는 것을 뜻합니다. Lean은 프로그래밍 언어일 뿐만 아니라 대화형 정리 증명기이기도 하므로, 재귀적 정의에는 특정 제한이 있습니다. Lean의 논리적 측면에서 순환 정의는 논리적 비일관성을 초래할 수 있습니다.

재귀적 정의가 Lean의 논리적 측면을 훼손하지 않도록 하기 위해, Lean은 모든 재귀 함수가 어떤 인수로 호출되든 종료된다는 것을 증명할 수 있어야 합니다. 실제로는 이는 재귀 호출이 모두 입력의 구조적으로 더 작은 부분에 대해 수행되어 항상 기본 사례(base case)로의 진행을 보장하거나, 사용자가 함수가 항상 종료된다는 다른 증거를 제공해야 함을 의미합니다. 마찬가지로, 재귀적 귀납적 타입은 해당 타입의 함수를 인수로 받는 생성자를 가질 수 없습니다. 이는 종료되지 않는 함수를 인코딩할 가능성이 있기 때문입니다.