타입의 타입: 일반적인 것부터 이색적인 것까지
프로그래밍 언어는 타입 시스템을 통해 데이터를 모델링하는 다양한 방법을 제공합니다. 특히 풍부한 타입 시스템을 갖추어 네 가지 기본 타입, 즉 함수 타입(Pi 타입), 곱 타입, 합 타입(귀납 타입), 몫 타입을 지원하는 Lean을 사용하여 이러한 개념을 살펴봅시다. Lean에서 수학적 대상은 세 단계의 계층 구조 안에 존재합니다.
- 유니버스 (예:
Type,Prop) - 타입 (유니버스의 원소)
- 항 (타입의 원소)
타입은 (Type이나 Prop 같은) 유니버스의 항으로서, 다른 항들을 분류하고 그 항들을 어떻게 사용할 수 있는지에 관한 계산적·논리적 규칙을 강제합니다. 항은 고유한 타입을 가지는 수학적 대상이며, :를 사용하여 표기합니다(예: 37 : ℝ는 37이 실수 타입의 항이라는 뜻입니다). 이는 엄격한 계층 구조를 이룹니다. 항은 타입의 원소이고 타입은 그 자체로 유니버스의 항이지만, 러셀의 역설 같은 역설을 피하기 위해 “모든 타입의 타입“은 존재하지 않으며, 그 대신 무한한 유니버스 계층이 있습니다.
Lean에서 단순 타입은 기초가 되며, 자연수를 위한 nat이나 불리언을 위한 bool 같은 기본 타입을 포함합니다. 이러한 타입은 일급 시민입니다. 즉, 다른 데이터와 마찬가지로 조작하고 전달할 수 있습니다. Lean의 타입 시스템은 이러한 단순 타입으로부터 함수 타입(α → β)이나 곱 타입(α × β) 같은 복잡한 타입을 구성할 수 있게 해 줍니다.
Lean의 #check 명령은 표현식의 타입을 조회하는 데 쓰이는 강력한 도구입니다. 이 명령은 상수, 함수, 표현식의 타입을 확인하여 그것들이 예상한 타입에 부합하는지 검증하는 데 도움을 줍니다. 예를 들면 다음과 같습니다.
constant m : nat -- m is a natural number
constant n : nat -- n is a natural number
#check m -- output: nat
#check n + 0 -- nat
#check tt -- boolean "true"
집합론에서는 소속 관계에 ∈를 사용하는 반면, 타입 이론에서는 항이 특정 타입을 가짐을 나타내기 위해 :를 사용합니다.
-- In set theory: 37 ∈ ℝ
-- In type theory:
#check 37 : ℝ -- 37 is a term of type ℝ
#check ℝ : Type -- ℝ is a term of type Type
러셀의 역설을 피하기 위해 모든 타입의 타입은 존재하지 않습니다. 그 대신 유니버스가 있습니다.
Type: 수학적 대상(예:ℝ,ℕ, 군, 환)을 담는 유니버스Prop: 명제(참/거짓 진술)를 담는 유니버스
타입 X와 Y에 대해, X에서 Y로 가는 함수의 타입은 X → Y로 씁니다.
def square : ℝ → ℝ := λ x, x^2
#check square -- ℝ → ℝ
유명한 커리-하워드 대응은 다음과 같이 말합니다.
- 명제는
Prop에 속한 타입입니다 - 증명은 이러한 타입의 항입니다
- 참인 명제는 정확히 하나의 항을 가집니다
- 거짓인 명제는 항을 하나도 가지지 않습니다
-- P → Q represents both:
-- 1. A function type from proofs of P to proofs of Q
-- 2. The logical implication P implies Q
Pi 타입이라고도 하는 함수 타입은 타입 사이의 사상을 나타냅니다. 함수 타입은 의존적일 수도 있고 비의존적일 수도 있습니다. 예를 들면 다음과 같습니다.
-- Simple function type (non-dependent)
def square : ℝ → ℝ := λ x, x^2
-- Dependent function type (Pi type)
def vector_length : Π (n : Nat), Vector ℝ n → ℝ
| 0 _ := 0
| (n+1) v := real.sqrt (dot_product v v)
Pi 타입 표기 Π (x : A), B x는 반환 타입 B x가 입력값 x에 의존할 수 있는 의존 함수 타입을 나타냅니다. 반환 타입이 입력에 의존하지 않을 때는 더 간단한 화살표 표기 A → B를 사용합니다.
**곱 타입(product type)**은 여러 값의 조합을 나타냅니다:
structure Point :=
(x : Int)
(y : Int)
structure Person :=
(name : String)
(age : Int)
(address : String)
**귀납적 타입(inductive type)**이라고도 하는 **합 타입(sum type)**은 여러 대안 중 하나를 나타냅니다:
inductive Shape
| circle (radius : Float)
| rectangle (width : Float) (height : Float)
| triangle (base : Float) (height : Float)
-- Example of using the equation compiler with sum types
def area : Shape → Float
| Shape.circle r := Float.pi * r * r
| Shape.rectangle w h := w * h
| Shape.triangle b h := b * h / 2
**몫 타입(quotient type)**은 어떤 관계 아래에서 동치인 값들을 나타냅니다:
-- Define an equivalence relation for angles
def angle_equiv (a b : Float) : Prop :=
∃ k : Int, a = b + k * 360
-- Create a quotient type for angles mod 360
def Angle := quotient (setoid.mk angle_equiv)
-- Constructor for angles
def mk_angle (degrees : Float) : Angle :=
quotient.mk degrees
**의존 타입(dependent type)**은 타입이 값에 의존할 수 있게 합니다:
-- A vector type whose length is part of its type
inductive Vector (α : Type) : Nat → Type
| nil : Vector α 0
| cons : α → {n : Nat} → Vector α n → Vector α (n + 1)
-- A function whose return type depends on its input
def get_type (b : Bool) : Type :=
if b then Nat else String
**차 타입(difference type)**은 한 타입에서 다른 타입을 “빼는 것“을 나타냅니다. Lean에서 직접 지원하지는 않지만, 의존 타입과 증명 의무(proof obligation)를 사용하여 인코딩할 수 있습니다. 차 타입은 “속성 B를 만족하는 원소를 제외한 타입 A“를 표현하고자 할 때 특히 유용합니다.
-- Non-zero numbers: ℝ "minus" 0
def NonZero := {x : ℝ // x ≠ 0}
-- Non-empty lists: List α "minus" empty list
def NonEmptyList (α : Type) := {l : List α // l ≠ []}
-- Even numbers: ℕ "minus" odd numbers
def Even := {n : ℕ // ∃ k, n = 2 * k}
-- Injective functions: (α → β) "minus" non-injective functions
def Injection (α β : Type) := {f : α → β // ∀ x y, f x = f y → x = y}
{x : A // P x} 구문은 원소가 술어 P를 만족하는 A의 부분 타입(subtype)을 나타냅니다. 이는 Lean이 의존 쌍(Σ-타입이라고도 합니다)을 통해 차 타입을 인코딩하는 방식입니다.
-- Creating terms of difference types
def two_nonzero : NonZero := ⟨2, by norm_num⟩
-- Extracting the underlying value
def get_value (n : NonZero) : ℝ := n.val
-- The proof of the property is also accessible
def get_proof (n : NonZero) : n.val ≠ 0 := n.property
예를 들어, NonZero를 사용하면 나눗셈을 전함수로 만들 수 있습니다(0으로 나누는 경우를 제거합니다):
def safe_div (a : ℝ) (b : NonZero) : ℝ := a / b.val
이 모든 것이 추상적으로 들릴 수 있지만, 이러한 타입은 많은 실제 응용에서 사용되며, 그 용도는 대체로 다음 범주로 나뉩니다:
함수 타입(Pi 타입)
- 고차 함수
- 증명 보조기의 의존 함수
- 타입 族(타입 패밀리)
- 다형 함수
곱 타입
- 설정 레코드
- 자료 구조
- 복잡한 도메인 모델
합 타입
- 오류 처리
- 상태 기계
- 추상 구문 트리
몫 타입
- 모듈러 산술
- 동치류
- 수학적 구조
차 타입
- 컴파일 시점에 불변 조건 강제하기
- 알고리즘에서 경계 사례 제거하기
- 암묵적 가정을 명시적으로 만들기
- 함수 사전 조건 강화하기