1.9.1. Evaluating Expressions🔗

Lean에서는 표현식을 평가할 때 계산이 일어난다. 이는 수학 표현식의 일반적인 규칙을 따른다. 즉 전체 표현식이 값이 될 때까지 일반적인 연산 순서에 따라 하위 표현식을 그 값으로 바꾼다. if나 match를 평가할 때는 조건이나 매칭 대상의 값을 찾을 때까지 분기의 표현식을 평가하지 않는다.

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

1.9.2. Functions🔗

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. Types🔗

Lean은 모든 표현식에 타입이 있는지 확인한다. Int, Point, {α : Type} → Nat → α → List α, Option (String ⊕ (Nat × String))과 같은 타입은 표현식에서 최종적으로 나올 수 있는 값을 설명한다. 다른 언어와 마찬가지로 Lean의 타입은 Lean 컴파일러가 확인하는 프로그램의 가벼운 명세를 표현할 수 있으므로 특정 종류의 단위 테스트가 필요하지 않게 한다. 대부분의 언어와 달리 Lean의 타입은 임의의 수학도 표현할 수 있어 프로그래밍과 정리 증명의 세계를 하나로 합친다. 정리 증명을 위해 Lean을 사용하는 내용은 이 책의 주된 범위를 벗어나지만, Lean 4에서 정리 증명하기에서 이 주제를 더 자세히 다룬다.

일부 표현식에는 여러 타입을 부여할 수 있다. 예를 들어 3은 Int일 수도 있고 Nat일 수도 있다. Lean에서는 이를 같은 것을 위한 두 가지 타입이 아니라, 우연히 같은 방식으로 쓰인 서로 다른 두 표현식(Nat 타입인 표현식과 Int 타입인 표현식)으로 이해해야 한다.

Lean은 때때로 타입을 자동으로 결정할 수 있지만 사용자가 타입을 제공해야 할 때가 많다. 이는 Lean의 타입 시스템이 매우 표현력이 높기 때문이다. Lean이 타입을 찾을 수 있더라도 원하는 타입을 찾지 못할 수 있다. 3을 Int로 사용하려 했더라도 추가 제약이 없으면 Lean은 Nat 타입을 부여한다. 일반적으로 대부분의 타입은 명시적으로 쓰고, 매우 분명한 타입만 Lean이 채우게 하는 것이 좋다. 이렇게 하면 Lean의 오류 메시지가 개선되고 프로그래머의 의도를 더 명확히 하는 데 도움이 된다.

일부 함수나 데이터 타입은 타입을 인수로 받는다. 이를 다형적(polymorphic)이라고 한다. 다형성은 목록 원소의 타입을 신경 쓰지 않고 목록의 길이를 계산하는 프로그램과 같은 것을 가능하게 한다. Lean에서 타입은 일급이므로 다형성에 특별한 문법이 필요하지 않으며 다른 인수와 마찬가지로 타입을 전달한다. 함수 타입에서 인수에 이름을 붙이면 뒤의 타입에서 그 이름을 언급할 수 있고, 함수에 인수를 적용하면 그 결과 항의 타입은 인수 이름을 실제 적용한 값으로 바꾸어 구한다.

1.9.4. Structures and Inductive Types🔗

structure나 inductive 기능을 사용해 완전히 새로운 데이터 타입을 Lean에 도입할 수 있다. 이 새 타입은 정의가 다른 타입과 완전히 같더라도 다른 어떤 타입과도 동등하다고 보지 않는다. 데이터 타입에는 값을 만들 수 있는 방법을 설명하는 생성자가 있으며 각 생성자는 일정 개수의 인수를 받는다. Lean의 생성자는 객체 지향 언어의 생성자와 같지 않다. Lean의 생성자는 할당된 객체를 초기화하는 실행 코드가 아니라 데이터를 담아 두는 수동적인 저장소다.

일반적으로 structure는 곱 타입(임의 개수의 인수를 받는 생성자가 하나뿐인 타입)을 도입하고, inductive는 합 타입(서로 다른 생성자가 여러 개인 타입)을 도입한다. structure로 정의한 데이터 타입에는 각 필드마다 하나의 접근자 함수가 제공된다. 구조체와 귀납적 데이터 타입은 모두 패턴 매칭으로 소비할 수 있으며, 패턴 매칭은 생성자를 호출할 때 사용하는 문법의 일부를 사용해 생성자 안에 저장된 값을 드러낸다. 패턴 매칭은 값을 만드는 방법을 알면 그 값을 소비하는 방법도 알 수 있다는 뜻이다.

1.9.5. Strings and Slices🔗

문자열은 문자들의 시퀀스이며, 문자 자체는 유니코드 코드 포인트다. 문자열의 실행 시간 표현은 UTF-8 인코딩의 바이트 배열과 캐시된 문자 수 필드로 이루어진다. Lean은 순수 함수형 언어이므로 문자열에서 공백을 제거하는 등의 연산은 보통 문자열을 복사해야 한다. 많은 문자열 함수가 문자열에 대한 참조와 시작·끝 위치를 짝지은 문자열 슬라이스를 반환하게 해 이런 복사를 피한다. 슬라이스는 시작·끝 위치를 갱신해 조작할 수 있으므로 복사가 필요 없다.

1.9.6. Recursion🔗

정의 안에서 정의 중인 이름을 사용하면 그 정의는 재귀적이다. Lean은 프로그래밍 언어인 동시에 대화형 정리 증명기이므로 재귀 정의에는 일정한 제한이 있다. Lean의 논리 측면에서는 순환 정의가 논리적 불일치를 일으킬 수 있다.

재귀 정의가 Lean의 논리 측면을 훼손하지 않게 하려면 어떤 인수로 호출하더라도 모든 재귀 함수가 종료된다는 사실을 Lean이 증명할 수 있어야 한다. 실제로 이는 재귀 호출이 항상 입력에서 구조적으로 더 작은 부분에 대해 이루어져 기본 경우를 향해 반드시 진전되거나, 함수가 항상 종료된다는 다른 증거를 사용자가 제공해야 한다는 뜻이다. 마찬가지로 재귀 귀납 타입은 그 재귀 타입을 인자로 받는 함수를 생성자가 받도록 허용되지 않는다. 그렇게 하면 종료하지 않는 함수를 인코딩할 수 있기 때문이다.