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은 타입이 Nat이고 값이 1인 새로운 상수 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는 타입 레벨을 범위로 하는 변수입니다. #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은 표현식 if not y then x + 1 else x + 2로부터 x와 y의 타입을 추론합니다.
수학에서 흔히 볼 수 있는 함수 연산의 몇 가지 예는 람다 추상화 항으로 기술할 수 있습니다:
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는 여러 개의 입력 매개변수를 받을 수 있습니다. 두 자연수를 더하는 함수를 만들어 봅시다:
매개변수 목록은 다음과 같이 나눌 수 있습니다:
여기서 add의 첫 번째 매개변수를 만들기 위해 double 함수를 호출했다는 점에 주목하십시오.
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)와 같은 것으로 간주하지만, 모든 이름이 모든 맥락에서 전개되는 것은 아닙니다. Natural을 Nat의 다른 이름으로 정의하는 다음 예를 살펴봅시다:
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 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 : α) → β에 대한 표기법일 뿐입니다.
리스트 예제로 돌아가서, #check 명령을 사용하면 다음 List 함수들의 타입을 확인할 수 있습니다. @ 기호와 소괄호와 중괄호의 차이는 잠시 후에 설명하겠습니다.
의존 함수 타입 (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 α 타입의 원소를 기대하는 함수 Lst.cons에 이것이 인자로 전달된다는 사실로부터 추론됩니다.
이는 의존 타입 이론의 핵심적인 특징입니다. 항은 많은 정보를 담고 있으며, 그 정보 중 일부는 문맥으로부터 추론할 수 있는 경우가 많습니다. 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의 타입을 제공한다는 점에 주목하십시오. 또한 출력은 첫 번째 인수가 암시적임을 보여 줍니다.