2. 의존 타입 이론
의존 타입 이론은 강력하고 표현력이 풍부한 언어로, 복잡한 수학적 주장을 표현하고, 복잡한 하드웨어와 소프트웨어 명세를 작성하며, 이 둘에 대해 자연스럽고 통일된 방식으로 추론할 수 있게 해줍니다. Lean은 구성 계산(Calculus of Constructions)이라고 알려진 의존 타입 이론의 한 버전을 기반으로 하며, 가산 개수의 비누적적 유니버스 계층과 귀납적 타입을 가지고 있습니다. 이 장이 끝날 무렵이면, 여러분은 이것이 의미하는 바를 대부분 이해하게 될 것입니다.
2.1. 단순 타입 이론
“타입 이론”이라는 이름은 모든 표현식이 연관된 타입을 갖는다는 사실에서 유래합니다. 예를 들어, 주어진 맥락에서 x + 0은 자연수를 나타낼 수 있고, f는 자연수에 대한 함수를 나타낼 수 있습니다. 정확한 정의를 선호하는 이들을 위해 말하자면, Lean의 자연수는 임의 정밀도 부호 없는 정수입니다.
다음은 Lean에서 객체를 선언하고 그 타입을 확인하는 방법에 대한 몇 가지 예시입니다.
/- Define some constants. -/
def m : Nat := 1 -- m is a natural number
def n : Nat := 0
def b1 : Bool := true -- b1 is a Boolean
def b2 : Bool := false
/- Check their types. -/
#check m#check n#check n + 0#check m * (n + 0)#check b1-- "&&" is the Boolean and
#check b1 && b2-- Boolean or
#check b1 || b2-- Boolean "true"
#check true
/- Evaluate -/
#eval 5 * 4#eval m + 2#eval b1 && b2
/-와 -/ 사이의 모든 텍스트는 Lean이 무시하는 주석 블록을 구성합니다. 이와 마찬가지로, 두 개의 대시 --는 해당 줄의 나머지 부분이 마찬가지로 무시되는 주석임을 나타냅니다. 주석 블록은 중첩될 수 있으며, 이는 많은 프로그래밍 언어에서와 마찬가지로 코드 덩어리를 “주석 처리”하는 것을 가능하게 합니다.
def 키워드는 작업 환경에 새로운 상수 기호를 선언합니다. 위 예시에서 def m : Nat := 1은 값이 1인 타입 Nat의 새로운 상수 m을 정의합니다. #check 명령은 Lean에게 그 타입을 보고하도록 요청합니다. Lean에서 시스템에 정보를 질의하는 보조 명령은 대개 해시(#) 기호로 시작합니다. #eval 명령은 Lean에게 주어진 표현식을 계산하도록 요청합니다. 직접 몇 가지 상수를 선언하고 표현식의 타입을 확인해 보아야 합니다. 이러한 방식으로 새로운 객체를 선언하는 것은 시스템을 실험해 보기에 좋은 방법입니다.
단순 타입 이론을 강력하게 만드는 것은 다른 타입들로부터 새로운 타입을 만들 수 있다는 점입니다. 예를 들어 a와 b가 타입이라면, a -> b는 a에서 b로 가는 함수의 타입을 나타내며, a × b는 a의 원소와 b의 원소로 이루어진 쌍의 타입을 나타내는데, 이는 Cartesian product라고도 불립니다. ×는 유니코드 기호라는 점에 유의하십시오. 유니코드를 신중하게 사용하면 가독성이 향상되며, 모든 최신 편집기가 이를 잘 지원합니다. Lean 표준 라이브러리에서는 타입을 나타내기 위해 그리스 문자를 자주 볼 수 있으며, ->의 더 간결한 형태로 유니코드 기호 →를 사용하는 것도 볼 수 있습니다.
#check Nat → Nat -- type the arrow as “\to” or "\r"#check Nat -> Nat -- alternative ASCII notation
#check Nat × Nat -- type the product as "\times"#check Prod Nat Nat -- alternative notation
#check Nat → Nat → Nat#check Nat → (Nat → Nat) -- same type as above
#check Nat × Nat → Nat#check (Nat → Nat) → Nat -- a "functional"#check Nat.succ#check (0, 1)#check Nat.add
#check Nat.succ 2#check Nat.add 3#check Nat.add 5 2#check (5, 9).1#check (5, 9).2
#eval Nat.succ 2#eval Nat.add 5 2#eval (5, 9).1#eval (5, 9).2다시 한번, 여러분 스스로 몇 가지 예제를 시도해 보아야 합니다.
기본 문법을 몇 가지 살펴봅시다. \to나 \r 또는 \->를 입력하여 유니코드 화살표 →를 입력할 수 있습니다. ASCII 대안인 ->도 사용할 수 있으므로, Nat -> Nat과 Nat → Nat 표현식은 같은 것을 의미합니다. 두 표현식 모두 자연수를 입력으로 받아 자연수를 출력으로 반환하는 함수의 타입을 나타냅니다. 데카르트 곱을 나타내는 유니코드 기호 ×는 \times로 입력합니다. 타입에 대한 범위를 나타낼 때는 일반적으로 α, β, γ와 같은 소문자 그리스 문자를 사용합니다. 이 특정 문자들은 \a, \b, \g로 입력할 수 있습니다.
여기서 몇 가지 더 주목할 점이 있습니다. 첫째, 함수 f를 값 x에 적용하는 것은 f x로 표기합니다(예: Nat.succ 2). 둘째, 타입 표현식을 작성할 때 화살표는 오른쪽으로 결합합니다. 예를 들어, Nat.add의 타입은 Nat → Nat → Nat이며, 이는 Nat → (Nat → Nat)와 동등합니다. 따라서 Nat.add를 자연수 하나를 받아, 자연수를 받아 자연수를 반환하는 또 다른 함수를 반환하는 함수로 볼 수 있습니다. 타입 이론에서는 일반적으로 Nat.add를 자연수 쌍을 입력으로 받아 자연수를 출력으로 반환하는 함수로 작성하는 것보다 이 방식이 더 편리합니다. 예를 들어, 이 방식은 함수 Nat.add를 “부분 적용”할 수 있게 해줍니다. 위 예시는 Nat.add 3의 타입이 Nat → Nat임을 보여주는데, 즉 Nat.add 3은 두 번째 인자 n을 “기다리는” 함수를 반환하며, 이는 Nat.add 3 n을 작성하는 것과 동등합니다.
m : Nat와 n : Nat가 있으면 (m, n)이 m과 n의 순서쌍을 나타내며, 이는 Nat × Nat 타입임을 이미 살펴보았습니다. 이는 자연수의 순서쌍을 만드는 방법을 제공합니다. 반대로 p : Nat × Nat가 있으면 p.1 : Nat과 p.2 : Nat을 쓸 수 있습니다. 이는 순서쌍의 두 구성 요소를 추출하는 방법을 제공합니다.
2.2. 객체로서의 타입
Lean의 의존 타입 이론이 단순 타입 이론을 확장하는 한 가지 방식은, Nat이나 Bool과 같은 개체인 타입 자체가 일급 시민이라는 점인데, 이는 곧 타입 자체도 객체라는 것을 뜻합니다. 그렇게 되려면, 그 각각도 타입을 가져야 합니다.
#check Nat#check Bool#check Nat → Bool#check Nat × Bool#check Nat → Nat#check Nat × Nat → Nat#check Nat → Nat → Nat#check Nat → (Nat → Nat)#check Nat → Nat → Bool#check (Nat → Nat) → Nat
위의 표현들이 각각 Type 타입의 객체임을 확인할 수 있습니다. 타입에 대한 새로운 상수를 선언할 수도 있습니다:
def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod
#check α#check F α#check F Nat#check G α#check G α β#check G α Nat
위의 예에서 알 수 있듯이, 여러분은 이미 Type → Type → Type 타입의 함수의 예를 본 적이 있는데, 바로 데카르트 곱 Prod입니다:
def α : Type := Nat
def β : Type := Bool
#check Prod α β#check α × β
#check Prod Nat Nat#check Nat × Nat
다른 예를 들자면, 임의의 타입 α가 주어졌을 때, 타입 List α는 타입 α의 원소들로 이루어진 리스트의 타입을 나타냅니다.
Lean의 모든 표현식은 타입을 가지므로, Type 자체는 어떤 타입을 가지는지 묻는 것은 자연스럽습니다.
여러분은 실제로 Lean의 타입 시스템에서 가장 미묘한 측면 중 하나를 마주하게 되었습니다. Lean의 기저 토대에는 타입의 무한한 계층이 존재합니다.
Type 0을 “작은” 또는 “일반적인” 타입들의 유니버스라고 생각하십시오. 그러면 Type 1은 Type 0을 원소로 포함하는 더 큰 타입들의 유니버스이며, Type 2는 Type 1을 원소로 포함하는 그보다 더 큰 타입들의 유니버스입니다. 이 목록은 무한합니다: 모든 자연수 n에 대해 Type n이 존재합니다. Type은 Type 0의 축약형입니다:
다음 표는 지금까지 논의된 관계를 구체적으로 이해하는 데 도움이 될 수 있습니다. x축을 따른 이동은 유니버스의 변화를 나타내고, y축을 따른 이동은 흔히 “차수(degree)”라고 불리는 것의 변화를 나타냅니다.
정렬 |
|
|
|
| ... |
|---|---|---|---|---|---|
타입 |
|
| ... | ||
항 |
|
| ... |
그러나 일부 연산은 타입 유니버스에 대해 다형적이어야 합니다. 예를 들어, List α는 α가 어떤 타입 유니버스에 속하든 상관없이 모든 타입 α에 대해 의미가 통해야 합니다. 이는 함수 List의 타입 시그니처를 설명해 줍니다:
여기서 u는 타입 수준(type level)에 걸쳐 변화하는 변수입니다. #check 명령의 출력은 α가 타입 Type u를 가질 때마다 List α 역시 타입 Type u를 가진다는 것을 의미합니다. 함수 Prod 역시 마찬가지로 다형적입니다:
다형적 상수를 정의하기 위해, Lean에서는 universe 명령을 사용하여 유니버스 변수를 명시적으로 선언할 수 있습니다:
F를 정의할 때 유니버스 매개변수를 제공하면 universe 명령을 피할 수 있습니다:
2.3. 함수 추상화와 평가
Lean은 다음과 같이 표현식으로부터 함수를 생성하기 위한 fun (또는 λ) 키워드를 제공합니다:
이 예제에서는 Nat 타입을 추론할 수 있습니다:
필요한 매개변수를 전달하여 람다 함수를 평가할 수 있습니다:
다른 표현식으로부터 함수를 만드는 과정을 람다 추상화라고 합니다. 변수 x : α가 있고 표현식 t : β를 구성할 수 있다고 가정하면, 표현식 fun (x : α) => t, 또는 이와 동등하게 λ (x : α) => t는 타입 α → β의 객체입니다. 이를 α에서 β로 가는 함수로 생각할 수 있는데, 이 함수는 임의의 값 x를 값 t로 사상합니다.
다음은 몇 가지 예시입니다
#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2#check fun x y => if not y then x + 1 else x + 2
Lean은 마지막 세 예제를 같은 표현식으로 해석합니다. 마지막 표현식에서 Lean은 x와 y의 타입을 표현식 if not y then x + 1 else x + 2로부터 추론합니다.
함수의 연산에 대한 수학적으로 흔한 몇 가지 예시는 람다 추상화의 관점에서 다음과 같이 기술할 수 있습니다:
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check fun x : Nat => x#check fun x : Nat => true#check fun x : Nat => g (f x)#check fun x => g (f x)
이 표현들이 무엇을 의미하는지 생각해 봅시다. 표현 fun x : Nat => x는 Nat에 대한 항등 함수를 나타내고, 표현 fun x : Nat => true는 항상 true를 반환하는 상수 함수를 나타내며, fun x : Nat => g (f x)는 f와 g의 합성을 나타냅니다. 일반적으로 타입 표기를 생략하고 Lean이 이를 추론하도록 할 수 있습니다. 그래서 예를 들어 fun x : Nat => g (f x) 대신 fun x => g (f x)라고 쓸 수 있습니다.
함수를 매개변수로 전달할 수 있으며, f와 g라는 이름을 부여하면 구현부에서 이 함수들을 사용할 수 있습니다.
타입도 매개변수로 전달할 수 있습니다:
예를 들어 마지막 표현식은 세 개의 타입 α, β, γ와 두 개의 함수 g : β → γ, f : α → β를 받아 g와 f의 합성을 반환하는 함수를 나타냅니다. (이 함수의 타입을 이해하려면 아래에서 설명할 의존 곱에 대한 이해가 필요합니다.)
람다 표현식의 일반적인 형태는 fun (x : α) => t이며, 여기서 변수 x는 “구속 변수(bound variable)”입니다. 즉, 이는 실제로는 자리표시자일 뿐이며, 그 “범위(scope)”는 표현식 t를 벗어나지 않습니다. 예를 들어, 표현식 fun (b : β) (x : α) => b에서의 변수 b는 앞서 선언된 상수 b와는 아무런 관련이 없습니다. 실제로 이 표현식은 fun (u : β) (z : α) => u와 동일한 함수를 나타냅니다.
형식적으로, 묶인 변수의 이름 바꾸기까지 고려했을 때 동일한 표현식은 알파 동치라고 부르며, “같은 것”으로 간주됩니다. Lean은 이 동치 관계를 인식합니다.
항 t : α → β를 항 s : α에 적용하면 표현식 t s : β가 나온다는 점에 유의하십시오. 이전 예제로 돌아가서 명확성을 위해 바인딩된 변수의 이름을 바꾸어, 다음 표현식들의 타입에 유의하십시오.
#check (fun x : Nat => x) 1#check (fun x : Nat => true) 1
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check
(fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
예상대로, 식 (fun x : Nat => x) 1은 Nat 타입을 가집니다. 사실, 더 강한 사실이 성립해야 합니다. 식 (fun x : Nat => x)를 1에 적용하면 값 1을 “반환”해야 합니다. 그리고 실제로 그러합니다:
이 항들이 어떻게 평가되는지는 나중에 살펴보겠습니다. 지금은 이것이 의존 타입 이론의 중요한 특징이라는 점만 짚어 두겠습니다. 모든 항은 계산적 동작을 가지며, 정규화라는 개념을 지원합니다. 원칙적으로 동일한 값으로 축약되는 두 항은 정의적으로 동치라고 불립니다. 이들은 Lean의 타입 검사기에 의해 “같은 것”으로 간주되며, Lean은 이러한 동일시를 인식하고 지원하기 위해 최선을 다합니다.
Lean은 완전한 프로그래밍 언어입니다. Lean에는 바이너리 실행 파일을 생성하는 컴파일러와 대화형 인터프리터가 있습니다. #eval 명령을 사용하여 표현식을 실행할 수 있으며, 이는 함수를 테스트하는 데 선호되는 방법입니다.
2.4. 정의
def 키워드가 새로운 이름 있는 객체를 선언하는 중요한 방법 중 하나를 제공한다는 점을 상기하십시오.
다른 프로그래밍 언어에서 함수가 어떻게 동작하는지 알고 있다면 이 방식이 더 익숙하게 느껴질 수 있습니다. 이름 double은 Nat 타입의 입력 매개변수 x를 받는 함수로 정의되며, 호출 결과는 x + x이므로 반환 타입은 Nat입니다. 이 함수는 다음과 같이 호출할 수 있습니다:
이 경우 def를 이름이 붙은 fun의 일종으로 생각할 수 있습니다. 다음은 같은 결과를 냅니다:
Lean이 타입을 추론하기에 충분한 정보를 가지고 있을 때는 타입 선언을 생략할 수 있습니다. 타입 추론은 Lean의 중요한 부분입니다.
def double :=
fun (x : Nat) => x + x
정의의 일반적인 형태는 def foo : α := bar이며, 여기서 α는 표현식 bar가 반환하는 타입입니다. Lean은 대개 타입 α를 추론할 수 있지만, 이를 명시적으로 작성하는 것이 좋은 경우가 많습니다. 이렇게 하면 의도가 명확해지며, 정의의 우변이 일치하는 타입을 갖지 않을 경우 Lean이 오류를 표시합니다.
우변 bar는 람다뿐만 아니라 어떤 식이든 될 수 있습니다. 따라서 def는 다음과 같이 값에 단순히 이름을 붙이는 데에도 사용할 수 있습니다:
def pi := 3.141592654
def는 여러 입력 매개변수를 받을 수 있습니다. 두 자연수를 더하는 것을 만들어 봅시다:
매개변수 목록은 다음과 같이 분리할 수 있습니다.
여기서는 double 함수를 호출하여 add의 첫 번째 매개변수를 생성했다는 점에 유의하십시오.
def 안에서 더 흥미로운 다른 표현식도 사용할 수 있습니다:
이 코드가 무엇을 할지는 아마 짐작하실 수 있을 것입니다.
다른 함수를 입력으로 받는 함수를 정의할 수도 있습니다. 다음은 주어진 함수를 두 번 호출하되, 첫 번째 호출의 출력을 두 번째 호출에 전달하는 예입니다:
이제 조금 더 추상적으로 들어가서, 타입 매개변수와 같은 인자를 지정할 수도 있습니다:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
이는 compose가 각각 하나의 입력만 받는 함수라면, 어떤 두 함수든 입력 인자로 받는 함수라는 것을 의미합니다. 타입 대수 β → γ와 α → β는 두 번째 함수의 출력 타입이 첫 번째 함수의 입력 타입과 일치해야 한다는 요구 사항을 의미합니다—그렇지 않으면 두 함수를 합성할 수 없을 것이므로 이는 당연한 것입니다.
compose는 α 타입의 세 번째 인자도 받는데, 이 인자를 사용하여 두 번째 함수(지역적으로 f라고 이름 붙임)를 호출하며, 그 함수의 결과(타입은 β)를 첫 번째 함수(지역적으로 g라고 이름 붙임)에 입력으로 전달합니다. 첫 번째 함수는 γ 타입을 반환하므로, 이것이 compose 함수의 반환 타입이기도 합니다.
compose는 임의의 타입 α β γ에 대해 작동한다는 점에서도 매우 일반적입니다. 이는 각각 하나의 매개변수를 받고, 두 번째 함수의 출력 타입이 첫 번째 함수의 입력과 일치하기만 하면 compose가 거의 모든 두 함수를 합성할 수 있다는 것을 의미합니다. 예를 들면 다음과 같습니다:
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def double (x : Nat) : Nat :=
x + x
def square (x : Nat) : Nat :=
x * x
#eval compose Nat Nat Nat double square 3
Lean은 근본적으로 정의된 이름을 그 전개(unfolding)와 동일하게 간주하지만, 모든 이름이 모든 맥락에서 전개되는 것은 아닙니다. Nat의 대체 이름으로 Natural을 정의하는 다음 예를 살펴봅시다:
def Natural := Nat
def를 사용하여 이름을 정의하면 이를 semireducible이라 부릅니다. Lean은 두 항이 정의적으로 같다는 것을 확립하는 데 반드시 필요할 때에만 이를 전개하지만, 대부분의 자동화 기능은 정의된 이름에 대한 참조를 건드리지 않은 채로 둡니다.
2.5. 지역 정의
Lean에서는 let 키워드를 사용하여 “지역적” 정의를 도입할 수도 있습니다. let a := t1; t2 표현식은 t2에 나오는 모든 a를 t1로 치환한 결과와 정의적으로 같습니다.
#check let y := 2 + 2; y * y#eval let y := 2 + 2; y * y
def twice_double (x : Nat) : Nat :=
let y := x + x; y * y
#eval twice_double 2
여기서 twice_double x는 항 (x + x) * (x + x)와 정의적으로 같습니다.
let 문을 연달아 사용하여 여러 대입을 결합할 수 있습니다:
줄바꿈을 사용하면 ;을 생략할 수 있습니다.
표현식 let a := t1; t2의 의미는 (fun a => t2) t1의 의미와 매우 유사하지만, 이 둘은 서로 같지 않다는 점에 유의하십시오. 첫 번째 표현식에서는 t2 안에 있는 모든 a의 인스턴스를 t1에 대한 구문적 축약으로 생각해야 합니다. 두 번째 표현식에서 a는 변수이며, fun a => t2라는 표현식은 a의 값과 무관하게 의미가 통해야 합니다. let 구문은 더 강력한 축약 수단이며, let a := t1; t2 형태의 표현식 중에는 (fun a => t2) t1로 표현할 수 없는 것도 있습니다. 연습 삼아, 아래 foo의 정의는 타입 검사를 통과하지만 bar의 정의는 그렇지 않은 이유를 이해해 보십시오.
def foo := let a := Nat; fun x : a => x + 2
/-
def bar := (fun a => fun x : a => x + 2) Nat
-/
2.6. 변수와 섹션
다음 세 가지 함수 정의를 살펴봅시다.
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (α : Type) (h : α → α) (x : α) : α :=
h (h x)
def doThrice (α : Type) (h : α → α) (x : α) : α :=
h (h (h x))
Lean은 이러한 선언을 더 간결하게 만들 수 있도록 variable 명령을 제공합니다:
variable (α β γ : Type)
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
def doTwice (h : α → α) (x : α) : α :=
h (h x)
def doThrice (h : α → α) (x : α) : α :=
h (h (h x))
Type 자체뿐만 아니라, 임의의 타입을 가진 변수도 선언할 수 있습니다:
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
#print compose#print doTwice#print doThrice이를 출력해 보면 세 그룹의 정의가 모두 정확히 동일한 효과를 낸다는 것을 알 수 있습니다.
variable 명령은 Lean에게 이름으로 참조하는 정의에 선언된 변수를 바운드 변수로 삽입하도록 지시합니다. Lean은 정의에서 어떤 변수가 명시적으로 또는 암묵적으로 사용되는지 파악할 만큼 충분히 똑똑합니다. 따라서 정의를 작성할 때 α, β, γ, g, f, h, x가 고정된 객체인 것처럼 진행하고, Lean이 자동으로 정의를 추상화하도록 할 수 있습니다.
이런 식으로 선언된 변수는 작업 중인 파일이 끝날 때까지 범위 내에 유지됩니다. 하지만 때로는 변수의 범위를 제한하는 것이 유용할 때가 있습니다. 이를 위해 Lean은 section이라는 개념을 제공합니다.
section useful
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
end useful
절이 닫히면 변수는 범위를 벗어나며, 더 이상 참조할 수 없습니다.
섹션 내부의 줄을 들여 쓸 필요는 없습니다. 또한 섹션에 이름을 붙일 필요도 없으므로, 익명의 section / end 쌍을 사용할 수 있습니다. 하지만 섹션에 이름을 붙인 경우에는, 같은 이름을 사용하여 닫아야 합니다. 섹션은 중첩될 수도 있으며, 이를 통해 새로운 변수를 점진적으로 선언할 수 있습니다.
2.7. 네임스페이스
Lean은 정의를 중첩된 계층적 namespace로 그룹화할 수 있는 기능을 제공합니다:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
def ffa : Nat := f (f a)
#check a #check f #check fa #check ffa #check Foo.faend Foo
-- #check a -- error
-- #check f -- error
#check Foo.a#check Foo.f#check Foo.fa#check Foo.ffa
open Foo
#check a#check f#check fa#check Foo.fa
Foo 이름공간에서 작업하고 있다고 선언하면, 선언하는 모든 식별자는 “Foo.” 접두사가 붙은 완전한 이름을 갖게 됩니다. 이름공간 안에서는 더 짧은 이름으로 식별자를 참조할 수 있지만, 이름공간을 끝내고 나면 더 긴 이름을 사용해야 합니다. section과 달리, 이름공간에는 이름이 필요합니다. 최상위 수준에는 익명 이름공간이 오직 하나만 존재합니다.
open 명령은 더 짧은 이름들을 현재 컨텍스트로 가져옵니다. 흔히 모듈을 임포트할 때, 짧은 식별자에 접근하기 위해 그 모듈에 포함된 하나 이상의 네임스페이스를 열고 싶을 것입니다. 하지만 때로는 이 정보를 완전히 정규화된 이름으로 보호된 채로 남겨두고 싶을 때도 있는데, 예를 들어 사용하고자 하는 다른 네임스페이스의 식별자와 충돌하는 경우가 그렇습니다. 따라서 네임스페이스는 작업 환경에서 이름을 관리할 수 있는 방법을 제공합니다.
예를 들어, Lean은 리스트와 관련된 정의와 정리를 List 네임스페이스로 묶습니다.
open List 명령을 사용하면 더 짧은 이름을 사용할 수 있습니다:
섹션과 마찬가지로, 네임스페이스도 중첩될 수 있습니다:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
namespace Bar
def ffa : Nat := f (f a)
#check fa #check ffa end Bar
#check fa #check Bar.ffaend Foo
#check Foo.fa#check Foo.Bar.ffa
open Foo
#check fa#check Bar.ffa닫힌 네임스페이스는 나중에, 심지어 다른 파일에서도 다시 열 수 있습니다:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
def fa : Nat := f a
end Foo
#check Foo.a#check Foo.f
namespace Foo
def ffa : Nat := f (f a)
end Foo
섹션과 마찬가지로, 중첩된 네임스페이스는 열린 순서의 역순으로 닫아야 합니다. 네임스페이스와 섹션은 서로 다른 목적을 가집니다. 네임스페이스는 데이터를 조직화하고, 섹션은 정의에 삽입할 변수를 선언합니다. 섹션은 또한 set_option, open과 같은 명령의 범위를 한정하는 데도 유용합니다.
그러나 여러 면에서 namespace ... end 블록은 section ... end 블록과 동일하게 동작합니다. 특히 네임스페이스 내에서 variable 명령을 사용하면 그 범위는 해당 네임스페이스로 제한됩니다. 마찬가지로 네임스페이스 내에서 open 명령을 사용하면 그 효과는 네임스페이스가 닫힐 때 사라집니다.
2.8. 무엇이 의존 타입 이론을 의존적이게 만듭니까?
간단히 설명하자면, 타입은 매개변수에 의존할 수 있습니다. 이에 대한 좋은 예시를 이미 보셨습니다: List α 타입은 인자 α에 의존하며, 이러한 의존성이 바로 List Nat과 List Bool을 구별짓는 요소입니다. 다른 예로, α의 원소로 이루어진 길이 n인 벡터의 타입인 Vector α n 타입을 생각해 보십시오. 이 타입은 두 개의 매개변수에 의존합니다: 벡터 내 원소의 타입(α : Type)과 벡터의 길이 n : Nat입니다.
리스트의 맨 앞에 새 원소를 삽입하는 함수 cons를 작성하고자 한다고 가정해 봅시다. cons는 어떤 타입을 가져야 할까요? 이러한 함수는 다형적입니다: Nat, Bool, 혹은 임의의 타입 α에 대한 cons 함수가 동일한 방식으로 동작하기를 기대할 것입니다. 따라서 타입을 cons의 첫 번째 인자로 삼는 것이 합리적이며, 이렇게 하면 임의의 타입 α에 대해 cons α가 타입 α의 리스트에 대한 삽입 함수가 됩니다. 다시 말해, 모든 α에 대해 cons α는 원소 a : α와 리스트 as : List α를 받아 새로운 리스트를 반환하는 함수이므로, cons α a as : List α가 성립합니다.
cons α가 α → List α → List α 타입을 가져야 함은 분명합니다. 하지만 cons는 어떤 타입을 가져야 할까요? 첫 번째 추측으로는 Type → α → List α → List α를 떠올릴 수 있지만, 다시 생각해 보면 이는 말이 되지 않습니다. 이 표현에서 α는 아무것도 참조하지 않는 반면, 실제로는 Type 타입의 인자를 참조해야 하기 때문입니다. 다시 말해, α : Type가 함수의 첫 번째 인자라고 가정하면, 다음 두 요소의 타입은 각각 α와 List α입니다. 이 타입들은 첫 번째 인자인 α에 따라 달라집니다.
def cons (α : Type) (a : α) (as : List α) : List α :=
List.cons a as
#check cons Nat#check cons Bool#check cons
이는 의존 함수 타입, 즉 의존 화살표 타입의 한 예시입니다. α : Type과 β : α → Type이 주어졌을 때, β를 α 위의 타입들의 모임, 즉 각 a : α에 대한 타입 β a로 생각하십시오. 이 경우, 타입 (a : α) → β a는 각 a : α에 대해 f a가 β a의 원소가 된다는 성질을 갖는 함수 f의 타입을 나타냅니다. 다시 말해, f가 반환하는 값의 타입은 그 입력에 의존합니다.
(a : α) → β는 임의의 표현식 β : Type에 대해 의미가 성립함에 유의하십시오. β의 값이 a에 의존하는 경우(예를 들어 앞 문단의 표현식 β a가 그러합니다), (a : α) → β는 의존 함수 타입을 나타냅니다. β가 a에 의존하지 않는 경우, (a : α) → β는 타입 α → β와 다르지 않습니다. 실제로 의존 타입 이론에서(그리고 Lean에서), β가 a에 의존하지 않을 때 α → β는 (a : α) → β에 대한 표기법일 뿐입니다.
목록의 예로 돌아가서, 다음 List 함수들의 타입을 확인하는 데 #check 명령어를 사용할 수 있습니다. @ 기호와 소괄호·중괄호의 차이는 곧 설명하겠습니다.
의존 함수 타입 (a : α) → β a가 β가 a에 의존하도록 허용함으로써 함수 타입 α → β의 개념을 일반화하는 것과 마찬가지로, 의존 데카르트 곱 타입 (a : α) × β a도 같은 방식으로 데카르트 곱 α × β를 일반화합니다. 의존 곱은 시그마 타입이라고도 불리며, Σ a : α, β a로도 쓸 수 있습니다. 의존 쌍을 만들려면 ⟨a, b⟩ 또는 Sigma.mk a b를 사용할 수 있습니다. ⟨와 ⟩ 문자는 각각 \langle와 \rangle 또는 \<와 \>로 입력할 수 있습니다.
universe u v
def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a b
def h1 (x : Nat) : Nat :=
(f Type (fun α => α) Nat x).2
#eval h1 5
def h2 (x : Nat) : Nat :=
(g Type (fun α => α) Nat x).2
#eval h2 5
위의 함수 f와 g는 동일한 함수를 나타냅니다.
2.9. 암시적 인자
리스트가 다음과 같이 구현되어 있다고 가정합시다:
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst#check Lst.cons#check Lst.nil#check Lst.append
그러면 다음과 같이 Nat의 리스트를 구성할 수 있습니다:
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst.cons Nat 0 (Lst.nil Nat)
def as : Lst Nat := Lst.nil Nat
def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat)
#check Lst.append Nat as bs
생성자는 타입에 대해 다형적이므로, Nat 타입을 인자로 반복해서 삽입해야 합니다. 하지만 이 정보는 중복됩니다. Lst.cons Nat 5 (Lst.nil Nat)에서 인자 α는 두 번째 인자인 5가 Nat 타입을 가진다는 사실로부터 추론할 수 있습니다. 마찬가지로 Lst.nil Nat에 있는 인자도, 그 표현식 안의 다른 무언가로부터가 아니라, 그것이 함수 Lst.cons에 인자로 전달된다는 사실로부터 추론할 수 있습니다. 이 함수는 해당 위치에 Lst α 타입의 원소를 기대하기 때문입니다.
이는 의존 타입 이론의 핵심적인 특징입니다. 항은 많은 정보를 담고 있으며, 종종 그 정보 중 일부는 맥락으로부터 추론될 수 있습니다. Lean에서는 밑줄 _을 사용하여 시스템이 그 정보를 자동으로 채워 넣도록 지정합니다. 이를 “암시적 인자(implicit argument)”라고 합니다.
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst
#check Lst.cons
#check Lst.nil
#check Lst.append
#check Lst.cons _ 0 (Lst.nil _)
def as : Lst Nat := Lst.nil _
def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)
#check Lst.append _ as bs하지만 이 모든 밑줄을 타이핑하는 것은 여전히 번거롭습니다. 함수가 일반적으로 문맥에서 추론될 수 있는 인자를 받을 때, Lean은 이 인자를 기본적으로 암묵적으로 남겨두도록 지정할 수 있게 해 줍니다. 이는 다음과 같이 인자를 중괄호 안에 넣음으로써 이루어집니다:
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil {α : Type u} : Lst α := List.nil
def Lst.append {α : Type u} (as bs : Lst α) : Lst α := List.append as bs
#check Lst.cons 0 Lst.nil
def as : Lst Nat := Lst.nil
def bs : Lst Nat := Lst.cons 5 Lst.nil
#check Lst.append as bs
변한 것은 변수 선언에서 α : Type u를 감싸는 중괄호뿐입니다. 이 방법은 함수 정의에서도 사용할 수 있습니다.
ident의 타입을 확인하려면 시그니처가 표시되지 않도록 괄호로 감싸야 합니다:
universe u
def ident {α : Type u} (x : α) := x
#check (ident)#check ident 1#check ident "hello"#check @ident
이는 ident의 첫 번째 인자를 암묵적으로 만듭니다. 표기법상 이는 타입 명시를 숨겨서, 마치 ident가 그저 임의의 타입을 인자로 받는 것처럼 보이게 합니다. 실제로 표준 라이브러리에 정의된 함수 id가 정확히 이런 방식으로 정의되어 있습니다. 여기서 관례를 따르지 않는 이름을 선택한 것은 오직 이름 충돌을 피하기 위해서일 뿐입니다.
변수는 variable 명령으로 선언될 때도 암묵적으로 지정될 수 있습니다:
universe u
section
variable {α : Type u}
variable (x : α)
def ident := x
end
#check ident#check ident 4#check ident "hello"
여기서의 이 ident 정의는 위의 것과 동일한 효과를 가집니다.
Lean은 암시적 인자를 인스턴스화하기 위한 매우 복잡한 메커니즘을 가지고 있으며, 이러한 메커니즘이 함수 타입, 술어, 심지어 증명을 추론하는 데에도 사용될 수 있음을 살펴볼 것입니다. 항 안에서 이러한 “구멍” 또는 “자리 표시자”를 인스턴스화하는 과정은 흔히 정교화라고 알려져 있습니다. 암시적 인자의 존재는 때로는 표현식의 의미를 정확하게 확정하기에 정보가 충분하지 않을 수 있음을 의미합니다. id나 List.nil과 같은 표현식은 서로 다른 맥락에서 서로 다른 의미를 가질 수 있기 때문에 다형적이라고 합니다.
(e : T)와 같이 작성하여 표현식 e의 타입 T를 언제나 명시적으로 지정할 수 있습니다. 이는 Lean의 정교화기가 암시적 인자를 해석하려 할 때 T 값을 e의 타입으로 사용하도록 지시합니다. 아래의 두 번째 예제 쌍에서는 이 메커니즘을 사용하여 표현식 id와 List.nil의 원하는 타입을 지정합니다:
숫자 리터럴은 Lean에서 오버로드되지만, 숫자 리터럴의 타입을 추론할 수 없는 경우 Lean은 기본적으로 그것이 자연수라고 가정합니다. 그래서 아래의 처음 두 #check 명령에 있는 표현식은 같은 방식으로 정교화되는 반면, 세 번째 #check 명령은 2를 정수로 해석합니다.
하지만 때로는 함수의 인자를 암묵적으로 선언해 두었지만 이제는 그 인자를 명시적으로 제공하고 싶은 상황에 놓일 수 있습니다. foo가 그러한 함수라면, @foo라는 표기법은 모든 인자를 명시적으로 만든 동일한 함수를 나타냅니다.
이제 첫 번째 #check 명령은 어떤 자리표시자도 삽입하지 않은 채로 식별자 id의 타입을 제공한다는 점에 유의하십시오. 또한, 출력은 첫 번째 인자가 암묵적임을 나타냅니다.