200줄의 Python으로 구현하는 의존 타입
구성의 계산(Calculus of Constructions, 줄여서 CoC)은 가장 널리 쓰이는 타입 있는 람다 대수 중 하나이며, Coq와 같은 의존 타입의 프로그래밍 언어의 이론적 토대를 이룹니다. 이 글에서는 200줄의 Python으로 CoC의 타입 검사기를 구현하면서 핵심 구성 요소를 하나씩 나누어 살펴보고 각각이 어떻게 동작하는지 설명합니다. 이것은 대체로 코드 골프 연습이므로 구현이 아주 견고하지는 않지만, 이것을 Python으로도 구현할 수 있다는 점이 재미있습니다.
배경을 조금 설명하자면, CoC는 1985년 Thierry Coquand가 개발한 고차 타입 람다 대수로, 두 가지 핵심 개념을 결합합니다.
- 의존 타입 - 항에 의존할 수 있는 타입
- 타입 다형성 - 타입에 대해 양화할 수 있는 능력
이 체계에는 두 가지 종류(sort)가 있습니다. *(타입들의 타입)와 ☐(*의 타입)입니다. 이 체계는 다음과 같은 항을 지원합니다.
- 변수
- 람다 추상화 (λx:A.t)
- 함수 적용 (t u)
- 의존 곱 타입 (Πx:A.B)
- 타입 표기 (t : A)
구현을 Core 구성 요소별로 나누어 살펴봅시다. 먼저 항 표현이 있는데, 여기서는 Python 클래스를 사용해 대수적 데이터 타입을 흉내 냅니다.
De Bruijn 인덱스 이해하기
구현에 들어가기 전에, 변수 조회에 사용하는 De Bruijn 인덱스를 이해해 봅시다. De Bruijn 표기법에서 변수는 해당 변수의 바인딩 위치를 찾기 위해 바인더를 몇 개나 거슬러 올라가야 하는지를 나타내는 숫자로 표현됩니다. 예를 들면 다음과 같습니다.
# Traditional notation:
λx. λy. x y
# De Bruijn notation:
λ. λ. 1 0 # 1 refers to x (up one binder), 0 refers to y (current binder)
더 많은 예시입니다.
# Traditional: # De Bruijn: # Explanation:
λx. x λ. 0 # x is bound by the current (0th) binder
λx. λy. y λ. λ. 0 # y is bound by the current binder
λx. λy. λz. x y z λ. λ. λ. 2 1 0 # x=2, y=1, z=0 binders up
Πx:*. λy. x Π*. λ. 1 # x is one binder up from y
우리 구현에서는 컨텍스트 조회에 인덱스(안쪽부터 셈) 대신 De Bruijn 레벨(바깥쪽부터 셈)을 사용합니다. 이 때문에 컨텍스트에 접근할 때 lvl - x - 1을 사용하여 레벨을 인덱스로 변환합니다.
타입 항 계층 구조
@dataclass
class Term:
pass
@dataclass
class Lam(Term):
f: Callable[[Term], Term]
@dataclass
class Pi(Term):
a: Term
f: Callable[[Term], Term]
@dataclass
class Appl(Term):
m: Term
n: Term
@dataclass
class Ann(Term):
m: Term
a: Term
@dataclass
class FreeVar(Term):
x: int
@dataclass
class Star(Term):
pass
@dataclass
class Box(Term):
pass
항 평가를 위해 람다 대수의 Core 계산 규칙인 베타 축약을 구현합니다. eval 함수는 값에 의한 호출(call-by-value) 평가 전략을 구현하며, 의존 타입에서는 타입이 계산상 동등한지 비교해야 하므로 타입 검사에 매우 중요합니다.
def eval(term: Term) -> Term:
match term:
case Lam(f):
return Lam(lambda n: eval(f(n)))
case Pi(a, f):
return Pi(eval(a), lambda n: eval(f(n)))
case Appl(m, n):
m_eval = eval(m)
n_eval = eval(n)
match m_eval:
case Lam(f):
return f(n_eval)
case _:
return Appl(m_eval, n_eval)
case Ann(m, _):
return eval(m)
case FreeVar() | Star() | Box():
return term
타입 검사기는 서로 재귀적으로 호출하는 세 개의 함수로 나뉩니다. 주목해야 할 몇 가지 중요한 구현 세부 사항은 다음과 같습니다.
infer_ty와check_ty함수는 항상 평가된 타입을 반환합니다- 타입 컨텍스트(
ctx)는 평가된 타입만 포함해야 하며 잘 형성되어 있어야 합니다(모든 항목은 어떤 종류(sort)에 속해야 합니다) - 바인딩은 컨텍스트의 앞쪽에 추가되며 De Bruijn 인덱스로 색인됩니다
FreeVar는 De Bruijn 레벨을 사용하므로, 컨텍스트에 접근할 때lvl - x - 1을 사용합니다
def infer_ty(lvl: int, ctx: List[Term], term: Term) -> Term:
match term:
case Pi(a, f):
_s1 = infer_sort(lvl, ctx, a)
s2 = infer_sort(lvl + 1, [eval(a)] + ctx, unfurl(lvl, f))
return s2
case Appl(m, n):
m_ty = infer_ty(lvl, ctx, m)
match m_ty:
case Pi(a, f):
_ = check_ty(lvl, ctx, (n, a))
return f(n)
case _:
return panic(lvl, m, f"Want a Pi type, got {print_term(lvl, m_ty)}")
case Ann(m, a):
_s = infer_sort(lvl, ctx, a)
return check_ty(lvl, ctx, (m, eval(a)))
case FreeVar(x):
return ctx[lvl - x - 1]
case Star():
return Box()
case Box():
return panic(lvl, Box(), "Has no type")
infer_ty 함수는 양방향 타입 검사를 구현합니다:
- Pi 타입의 경우, 정의역과 공역이 모두 소트(sort)인지 확인합니다
- 적용(application)의 경우, 함수 타입을 추론하고 인자를 검사합니다
- 주석(annotation)의 경우, 타입이 올바른지 확인하고 그 타입에 대해 항을 검사합니다
- 변수의 경우, 컨텍스트에서 그 타입을 조회합니다
*의 경우,☐를 반환합니다☐는 타입을 갖지 않습니다(계층의 최상위에 있기 때문입니다)
def infer_sort(lvl: int, ctx: List[Term], a: Term) -> Term:
ty = infer_ty(lvl, ctx, a)
match ty:
case Star() | Box():
return ty
case _:
return panic(lvl, a, f"Want a sort, got {print_term(lvl, ty)}")
infer_sort 함수는 항이 * 또는 ☐ 타입을 갖는지 확인합니다:
- 항의 타입을 추론합니다
- 그것이 소트인지 확인합니다
- 타입 형성 규칙에서 사용할 수 있도록 소트를 반환합니다
def check_ty(lvl: int, ctx: List[Term], pair: Tuple[Term, Term]) -> Term:
t, ty = pair
match (t, ty):
case (Lam(f), Pi(a, g)):
_ = check_ty(lvl + 1, [a] + ctx, unfurl2(lvl, (f, g)))
return Pi(a, g)
case (Lam(f), _):
return panic(lvl, Lam(f), f"Want a Pi type, got {print_term(lvl, ty)}")
case _:
got_ty = infer_ty(lvl, ctx, t)
if equate(lvl, (ty, got_ty)):
return ty
return panic(lvl, t, f"Want type {print_term(lvl, ty)}, got {print_term(lvl, got_ty)}")
equate 함수는 구조적 동등성 검사를 구현합니다. 두 항이 베타 변환 가능한지(계산적 동등성) 검사할 때는 equate를 호출하기 전에 먼저 두 항을 평가해야 합니다. check_ty에서 추론된 타입(got_ty)과 기대 타입(ty)을 비교할 때는 둘 다 이미 정규형이므로 추가 평가가 필요하지 않습니다.
def equate(lvl: int, terms: Tuple[Term, Term]) -> bool:
def plunge(pair: Tuple[Callable[[Term], Term], Callable[[Term], Term]]) -> bool:
return equate(lvl + 1, unfurl2(lvl, pair))
match terms:
case (Lam(f), Lam(g)):
return plunge((f, g))
case (Pi(a, f), Pi(b, g)):
return equate(lvl, (a, b)) and plunge((f, g))
case (Appl(m, n), Appl(m2, n2)):
return equate(lvl, (m, m2)) and equate(lvl, (n, n2))
case (Ann(m, a), Ann(m2, b)):
return equate(lvl, (m, m2)) and equate(lvl, (a, b))
case (FreeVar(x), FreeVar(y)):
return x == y
case (Star(), Star()) | (Box(), Box()):
return True
case _:
return False
equate 함수는 구조적 동등성 검사를 구현합니다:
- 모든 항 생성자를 처리하면서 항을 재귀적으로 비교합니다
- 속박 변수에 대해서는 HOAS 비교를 사용합니다
- 레벨 카운팅 메커니즘을 통해 알파 동치를 구현합니다
def unfurl(lvl: int, f: Callable[[Term], Term]) -> Term:
return f(FreeVar(lvl))
def unfurl2(lvl: int, pair: Tuple[Callable[[Term], Term], Callable[[Term], Term]]) -> Tuple[Term, Term]:
f, g = pair
return (unfurl(lvl, f), unfurl(lvl, g))
다음 유틸리티 함수들은 HOAS 변수 조작을 처리합니다:
unfurl은 HOAS 함수를 자유 변수를 가진 항으로 변환합니다unfurl2는 함수 쌍에 대해 같은 일을 합니다- 레벨 매개변수는 변수의 올바른 스코프를 보장합니다
def print_term(lvl: int, term: Term) -> str:
def plunge(f: Callable[[Term], Term]) -> str:
return print_term(lvl + 1, unfurl(lvl, f))
match term:
case Lam(f):
return f"(λ{plunge(f)})"
case Pi(a, f):
return f"(Π{print_term(lvl, a)}.{plunge(f)})"
case Appl(m, n):
return f"({print_term(lvl, m)} {print_term(lvl, n)})"
case Ann(m, a):
return f"({print_term(lvl, m)} : {print_term(lvl, a)})"
case FreeVar(x):
return str(x)
case Star():
return "*"
case Box():
return "☐"
print_term 함수는 항을 읽기 쉬운 문자열 표현으로 변환합니다:
이제 CoC가 실제로 동작하는 두 가지 “실용적인” 예제인 처치 수(Church numeral)와 길이 색인 벡터를 살펴봅시다. 예제를 더 읽기 쉽게 만들기 위해 몇 가지 헬퍼 함수를 사용합니다:
def curry2(f):
return Lam(lambda x: Lam(lambda y: f(x, y)))
def curry3(f):
return Lam(lambda x: curry2(lambda y, z: f(x, y, z)))
def curry4(f):
return Lam(lambda x: curry3(lambda y, z, w: f(x, y, z, w)))
def curry5(f):
return Lam(lambda x: curry4(lambda y, z, w, v: f(x, y, z, w, v)))
def appl(f: Term, args: List[Term]) -> Term:
return reduce(lambda m, n: Appl(m, n), args, f)
처치 수는 자연수를 함수로 표현합니다. CoC에서는 처치 수에 정확한 타입을 부여할 수 있습니다:
# The type of Church numerals
n_ty = Pi(Star(), lambda a:
Pi(Pi(a, lambda _x: a), lambda _f:
Pi(a, lambda _x: a)))
# Zero is the identity function
zero = Ann(curry3(lambda _a, _f, x: x), n_ty)
# Successor applies f one more time
succ = Ann(
curry4(lambda n, a, f, x: Appl(f, appl(n, [a, f, x]))),
Pi(n_ty, lambda _n: n_ty)
)
# Addition combines the function applications
add = Ann(
curry5(lambda n, m, a, f, x:
appl(n, [a, f, appl(m, [a, f, x])])),
Pi(n_ty, lambda _n: Pi(n_ty, lambda _m: n_ty))
)
다음과 같은 일이 일어납니다:
- 처치 수는 타입
a, 함수f: a → a, 값x: a를 받습니다 f를x에 n번 적용하며, 여기서 n은 표현되는 수입니다zero는 x를 그대로 반환합니다succ n은 n보다 f를 한 번 더 적용합니다add n m은 f를 n+m번 적용합니다
의존 타입을 사용하면 길이를 정적으로 알 수 있는 벡터도 만들 수 있습니다:
# Vector context setup
vect_ctx = [
# Vector type constructor: (n: Nat) → (a: Type) → Type
Pi(n_ty, lambda _n: Pi(Star(), lambda _a: Star())),
# Item type and value
Star(),
item_ty,
# replicate: (n: Nat) → (a: Type) → a → Vec n a
Pi(n_ty, lambda n:
Pi(Star(), lambda a:
Pi(a, lambda _x: vect_ty(n, a)))),
# concat: (n m: Nat) → (a: Type) → Vec n a → Vec m a → Vec (n+m) a
Pi(n_ty, lambda n:
Pi(n_ty, lambda m:
Pi(Star(), lambda a:
Pi(vect_ty(n, a), lambda _x:
Pi(vect_ty(m, a), lambda _y:
vect_ty(appl(add, [n, m]), a)))))),
# zip: (n: Nat) → (a b: Type) → Vec n a → Vec n b → Vec n (Pair a b)
Pi(n_ty, lambda n:
Pi(Star(), lambda a:
Pi(Star(), lambda b:
Pi(vect_ty(n, a), lambda _x:
Pi(vect_ty(n, b), lambda _y:
vect_ty(n, appl(pair, [a, b])))))))
]
벡터 연산은 의존 타이핑을 보여 줍니다:
replicate는 하나의 값으로 채워진 길이 n의 벡터를 만듭니다concat은 벡터를 결합하며, 결과의 길이는 두 길이의 합입니다zip은 길이가 같은 두 벡터를 결합합니다
이 연산들은 다음과 같이 사용할 수 있습니다:
# Create vectors of different lengths
vect_one = replicate(one, item)
vect_three = replicate(three, item)
vect_four = concat(one, three, vect_one, vect_three)
# This will type check
zip(four, vect_four, vect_four)
# This will fail type checking - mismatched lengths
zip(four, vect_one, vect_four) # TypeError!
타입 시스템은 다음을 보장합니다:
- 벡터 길이가 정확하게 추적됩니다
- 연산이 길이 불변 조건을 유지합니다
- 길이 불일치가 정적으로 검출됩니다
이 예제들은 CoC가 계산과 정적 보장을 하나의 통합된 시스템 안에서 어떻게 함께 표현할 수 있는지 보여 줍니다. 타입 검사기는 유연한 프로그래밍 패턴을 여전히 허용하면서도 연산이 이러한 보장을 지키도록 합니다. 의존 타입은 멋집니다.
이 벡터 연산들의 구현을 더 자세히 살펴봅시다:
Replicate
# replicate: (n: Nat) → (a: Type) → a → Vec n a
def replicate(n: Term, x: Term) -> Term:
return appl(FreeVar(3), [n, item_ty, x])
replicate 함수는 모든 원소가 x인 길이 n의 벡터를 만듭니다. 타입은 결과 벡터의 길이가 입력된 수 n과 일치하도록 보장합니다. 실제 구현이라면 x를 n개 복사한 리스트를 구성하겠지만, 타입만 다루는 우리 구현에서는 타입만 추적합니다.
Concatenate
# concat: (n m: Nat) → (a: Type) → Vec n a → Vec m a → Vec (n+m) a
def concat(n: Term, m: Term, x: Term, y: Term) -> Term:
return appl(FreeVar(4), [n, m, item_ty, x, y])
concat 함수는 두 벡터를 결합합니다. 이 함수의 타입은 의존 타입이 산술 관계를 어떻게 추적할 수 있는지 보여 주므로 특히 흥미롭습니다. 출력 벡터의 길이는 입력 길이의 합인 n + m입니다. 이는 타입 시스템에 의해 정적으로 강제됩니다.
Zip
# zip: (n: Nat) → (a b: Type) → Vec n a → Vec n b → Vec n (Pair a b)
def zip(n: Term, x: Term, y: Term) -> Term:
return appl(FreeVar(5), [n, item_ty, item_ty, x, y])
zip 함수는 두 벡터를 원소별로 결합하여 쌍의 벡터로 만듭니다. 타입 시스템은 두 입력 벡터가 반드시 같은 길이 n을 가지도록 강제하며, 출력 벡터 역시 길이 n을 가지도록 보장합니다. 길이가 다른 벡터를 zip하려고 하면 런타임 오류가 아니라 컴파일 타임에 타입 오류가 발생합니다.
이 연산들은 정적 길이 검사를 갖춘 작은 벡터 라이브러리를 이룹니다. 타입 시스템은 다음과 같은 일이 불가능하도록 보장합니다:
- 벡터를 연결하면서 길이를 잘못 계산하는 일
- 길이가 다른 벡터를 zip하는 일
- 타입과 일치하지 않는 길이의 벡터를 만드는 일
이는 의존 타입이 정밀한 명세를 타입 시스템 안에 직접 인코딩할 수 있는 방법을 보여 줍니다. 우리 구현은 타입 검사기일 뿐이지만(실제로 벡터를 구성하지는 않습니다), 실제 구현을 갖추게 되는 Coq나 Agda 같은 언어에서 이러한 개념이 어떻게 작동하는지를 보여 줍니다.