타입 이론(Type Theory)은 값을 타입으로 분류하고 프로그램의 정확성을 수학적으로 보장하는 형식 체계다. 프로그래밍 언어 설계와 형식 증명의 기반이 된다.
단순 타입 람다 대수 (Simply Typed Lambda Calculus)
타입 문법:
τ ::= Base | τ → τ
타이핑 규칙:
Γ ⊢ x : τ (변수)
Γ, x:τ₁ ⊢ e:τ₂
───────────────── (추상)
Γ ⊢ λx:τ₁.e : τ₁→τ₂
Γ ⊢ f:τ₁→τ₂ Γ ⊢ a:τ₁
───────────────────────── (적용)
Γ ⊢ f a : τ₂
힌들리-밀너 타입 시스템 (HM)
Haskell, ML 계열 언어의 기반. 타입 추론이 가능한 가장 표현력 있는 타입 시스템.
haskell
-- 타입 추론 예시 (명시적 타입 표기 없음)
identity x = x
-- 추론: identity :: a -> a
map f [] = []
map f (x:xs) = f x : map f xs
-- 추론: map :: (a -> b) -> [a] -> [b]
System F (다형 람다 대수)
타입 추상화:
Λα. λx:α. x : ∀α. α → α
타입 적용:
(Λα. λx:α. x) [Int] : Int → Int
HM의 상위 집합, 완전한 타입 추론 불가
(GHC Haskell의 RankNTypes 확장)
주요 타입 시스템 비교
| 시스템 | 항 → 타입 | 타입 → 항 | 타입 → 타입 | 항 → 타입(dep) |
|---|
| STLC | O | X | X | X |
| System F | O | O | X | X |
| Fω | O | O | O | X |
| CoC | O | O | O | O |
서브타이핑
리스코프 치환 원칙(LSP):
S <: T 이면 T가 필요한 모든 곳에 S 사용 가능
공변(Covariant): Array<Cat> <: Array<Animal>? → 위험
불변(Invariant): Array는 불변
반변(Contravariant): 함수 입력 타입은 반변
함수 타입의 서브타이핑:
(T₁ → T₂) <: (S₁ → S₂)
iff S₁ <: T₁ (반변) and T₂ <: S₂ (공변)
관련 개념
