1.9.1. 표현식 평가하기🔗

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

변수는 한 번 값이 주어지면 절대 변하지 않습니다. 수학과 마찬가지로, 그러나 대부분의 프로그래밍 언어와는 달리, Lean의 변수는 새 값을 쓸 수 있는 주소가 아니라 단순히 값을 나타내는 자리표시자입니다. 변수의 값은 def를 사용한 전역 정의, let을 사용한 지역 정의, 함수에 이름 붙은 인자로 전달된 값, 또는 패턴 매칭에서 올 수 있습니다.

1.9.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.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은 모든 재귀 함수가 어떤 인자로 호출되든 반드시 종료된다는 것을 증명할 수 있어야 합니다. 실제로 이는 모든 재귀 호출이 입력의 구조적으로 더 작은 부분에 대해 수행되어 항상 기저 사례를 향해 진행함이 보장되거나, 그렇지 않으면 사용자가 함수가 항상 종료된다는 다른 근거를 제공해야 한다는 뜻입니다. 마찬가지로, 재귀적 귀납적 타입은 그 타입으로부터의 함수를 인자로 받는 생성자를 가질 수 없습니다. 이를 허용하면 종료되지 않는 함수를 인코딩할 수 있게 되기 때문입니다.