1.9.1. 표현식 평가하기🔗

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

변수는 한 번 값이 주어지면 결코 변하지 않습니다. 수학과 마찬가지로, 그러나 대부분의 프로그래밍 언어와는 다르게, Lean의 변수는 새로운 값을 기록할 수 있는 주소가 아니라 단순히 값을 위한 자리표시자입니다. 변수의 값은 def를 사용한 전역 정의, let을 사용한 지역 정의, 함수의 이름 붙은 인자, 또는 패턴 매칭으로부터 올 수 있습니다.

1.9.2. 함수🔗

Lean에서 함수는 일급 값(first-class value)이며, 이는 함수를 다른 함수의 인자로 전달하거나 변수에 저장하거나 다른 값과 마찬가지로 사용할 수 있음을 의미합니다. 모든 Lean 함수는 정확히 하나의 인자를 받습니다. 두 개 이상의 인자를 받는 함수를 표현하기 위해, Lean은 커링(currying)이라는 기법을 사용합니다. 이는 첫 번째 인자를 제공하면 나머지 인자를 기다리는 함수를 반환하는 방식입니다. 인자를 받지 않는 함수를 인코딩하기 위해, Lean은 가능한 가장 정보가 적은 인자인 Unit 타입을 사용합니다.

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

1. 익명 함수는 fun을 사용하여 작성합니다. 예를 들어, Point의 필드를 교체하는 함수는 fun (point : Point) => { x := point.y, y := point.x : Point }와 같이 작성할 수 있습니다

2. 매우 간단한 익명 함수는 괄호 안에 하나 이상의 가운뎃점(centered dot) ·를 배치하여 작성합니다. 각 가운데 점(centered dot)은 함수의 인자가 되며, 괄호는 함수 본문의 범위를 나타냅니다. 예를 들어, 인자에서 1을 빼는 함수는 fun x => x - 1 대신 (· - 1)로 작성할 수 있습니다.

3. 함수는 인자 목록을 추가하거나 패턴 매칭 표기법을 사용하여 def 또는 let으로 정의할 수 있습니다.

1.9.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.9.4. 구조체와 귀납적 타입🔗

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

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

1.9.5. 문자열과 슬라이스🔗

문자열은 문자들의 시퀀스이며, 각 문자는 그 자체로 유니코드 코드 포인트입니다. 이들의 실행 시점 표현은 UTF-8 인코딩으로 이루어진 바이트 배열과 캐시된 문자 수 필드로 구성됩니다. Lean은 순수 함수형 언어이므로, 문자열에서 공백을 제거하는 등의 연산은 일반적으로 문자열을 복사해야 합니다. 이는 문자열에 대한 많은 함수가 문자열 슬라이스를 반환하도록 하여 회피되는데, 이는 문자열에 대한 참조와 시작 및 끝 위치를 짝지은 것입니다. 슬라이스는 이러한 시작 위치와 끝 위치를 갱신하는 방식으로 조작할 수 있으며, 이를 통해 복사를 피할 수 있습니다.

1.9.6. 재귀🔗

정의는 정의되는 이름 자체가 그 정의 안에서 사용될 때 재귀적입니다. Lean은 프로그래밍 언어일 뿐만 아니라 대화형 정리 증명기이기도 하므로, 재귀 정의에는 특정한 제약이 있습니다. Lean의 논리적 측면에서, 순환 정의는 논리적 비일관성으로 이어질 수 있습니다.

재귀적 정의가 Lean의 논리적 측면을 훼손하지 않도록 보장하기 위해, Lean은 모든 재귀 함수가 어떤 인자로 호출되든 종료함을 증명할 수 있어야 합니다. 실제로는 재귀 호출이 항상 입력값의 구조적으로 더 작은 부분에 대해 수행됨으로써 기저 사례를 향한 진행이 항상 보장되거나, 그렇지 않다면 사용자가 함수가 항상 종료됨을 보이는 다른 증거를 제공해야 함을 의미합니다. 마찬가지로, 재귀적 귀납적 타입은 해당 타입으로부터 시작하는 함수를 인자로 받는 생성자를 가질 수 없는데, 이는 종료하지 않는 함수를 인코딩할 수 있게 만들기 때문입니다.