힌들리-밀너와 대비되는 양방향 타입 추론을 간단한 STLC 언어에 적용해 규칙을 양방향화하고 Rust로 구현해 본다.
URL: https://ettolrach.com/blog/bidirectional_inference.html
ettolrach 작성, 2025-12-23.
가장 흔히 쓰이는 프로그래밍 언어들은 타입 추론에 널리 알려진 단일 알고리즘을 쓰지 않는다. 몇몇 언어는 힌들리-밀너(Hindley–Milner) 타입 추론을 사용하는데, 예를 들면 Rust, Haskell, F# 등이 있다.
(내가 알기로) 어떤 대중적인 언어도 사용하지 않는 또 다른 알고리즘으로 양방향 타입 추론(bidirectional type inference) 이 있다. 힌들리-밀너와 달리, 구현이 더 쉽고 더 나은 오류 메시지를 제공한다고 알려져 있지만, 단점은 이해하기가 더 어렵고 시작하기가 더 까다롭다는 점이다.
[업데이트 2025-12-30: 이후 Swift가 양방향 알고리즘을 사용한다는 사실을 알게 되었다! 그래서 내 말이 틀렸다.]
관련 튜토리얼이 많지 않은데, 특히 이론 지식이 많지 않은 사람을 대상으로 한 자료가 더더욱 부족하다. 더 읽고 싶다면, 좀 더 형식적인 소개로는 Dunfield and Krishnaswami (2013)를, 또 다른 비형식적이고 쉬운 튜토리얼로는 Christiansen (2013)를 추천한다.
우리는 간단한 언어, 즉 단순 타입 람다 계산법(simply typed lambda calculus) 으로 시작할 것이다. 관심이 있다면, 다형성을 위한 ‘완전하고 쉬운(complete and easy)’ 변형의 좋은 구현도 나중 글에서 작성해, 다형적 타입 언어를 어떻게 타입체크하는지 배울 수 있게 해 보겠다.
아래에서는 Rust를 사용하지만, 대부분의 다른 언어에서도 비슷할 것이다.
단순 타입 람다 계산법(STLC)은 함수형 프로그래밍 언어의 핵심을 포착한다. 우리는 자유 변수, 추상화(즉 람다), 그리고 (함수) 적용만 가진다. 또한 기본 원시값으로 불리언 false 와 true 를 둔다. 나중에는 또 다른 원시 구성요소인 if-then-else 로 확장할 것이다. 현대 언어(C를 제외한 거의 모든 흔히 쓰이는 언어)를 써 봤다면, 이미 이런 것들을 써 본 경험이 있을 것이다! 또한 항(term)에 타입을 주석(annotate, sometimes called decorate)으로 달 수 있게 한다. 문법은 다음과 같다:
(원문에는 여기 STLC의 구문 정의가 그림/수식으로 제시된다.)
타입도 단순하게 유지한다. 기본 타입 Bool 하나와, 함수(화살표) 타입만 가진다.
이름이 암시하듯, 타입체크는 두 방향으로 진행된다. 어떤 항은 타입을 추론(infer) 하고, 다른 항은 주어진 타입인지 검사(check) 한다. 어떤 저자들은 항이 타입을 “합성(synthesise)”하고 다른 항은 타입을 “상속(inherit)”한다고 말하기도 한다. “합성(synthesising)과 검사(checking)”라는 혼합 표현도 본 적이 있다. 나는 개인적으로 “추론(inferring)과 검사(checking)”를 선호하지만, 이것은 순전히 취향이다.
먼저, 항이 어느 방향으로 갈지(추론인지 검사인지)를 어떻게 선택하는지 살펴보겠다. 지루하거나 길을 잃는다면 구현 부분으로 건너뛰어도 된다. 이해가 안 되면 언제든 앞의 섹션으로 돌아가면 된다.
그런데 어떤 항이 추론하고 어떤 항이 검사하도록 결정해야 할까? 우리는 Pfenning 방법 (Dunfield and Pfenning, 2004)을 따를 것이다. 먼저 타이핑 규칙을 적는다.
Var 는 자유 변수를 타입체크하는 규칙이다. 컨텍스트에 x가 타입 A로 매핑되어 있다면, 자유 변수 x는 타입 A를 가진다.Anno 규칙은 타입 추론이 동작하도록 돕는다. 항 L이 타입 A일 때, 우리는 언제든 L에 타입 A라는 주석을 달 수 있다. 주석이 달린 표현 자체도 같은 타입 A를 가진다.Ty Eq 규칙이 있다. 두 타입 A와 B가 같다면, 타입이 A인 항을 타입 B로 바꿔도 된다는 의미다. 지금은 꽤 쓸모없어 보이지만, 곧 유용해질 것이다.false 와 true 는 타입 Bool을 가지는 원시값이며, Rust에서처럼 언제든 구성할 수 있다.-> Intr 는 화살표 타입 도입(arrow introduction), 즉 추상화(람다)를 만드는 규칙이다. 컨텍스트에 이름이 x이고 타입이 A인 자유 변수를 추가했을 때 항 L이 타입 B를 가진다면, 인자 x의 타입이 A이고 본문이 L인 추상화는 타입 A -> B를 가진다.-> Elim 은 화살표 타입 제거(arrow elimination), 즉 적용(application) 규칙이다. L이 타입 A -> B인 항(즉 추상화)이고, M이 타입 A인 항이라면, L에 M을 적용한 결과는 타입 B를 가진다.두 번째 단계는 각 타입 규칙을 보고 이를 추론 규칙과 검사 규칙으로 바꾸는 것이다. 콜론을 화살표로 바꿔서 이를 수행할 수 있다. 항의 타입을 추론하는 규칙에는 =>를, 주어진 타입을 검사하는 규칙에는 <=를 사용하자.
도입(introduction) 규칙과 제거(elimination) 규칙부터 시작하자. 규칙의 주판단(principal judgement) 을 찾아야 한다. 즉 도입에서는 도입되는 항(보통 결론에 있는 것), 제거에서는 제거되는 항(보통 첫 번째 가정에 있는 것)이다. 그런 다음 이 주판단을 양방향화(bidirectionalise) 한다. 즉 콜론을 =>(추론) 또는 <=(검사)로 바꾼다. 도입은 검사, 제거는 추론으로 한다.
그 다음 규칙의 나머지 부분도 양방향화해야 한다. 가정의 가장 이른 판단부터 시작해 뒤의 판단들로, 마지막으로 결론으로 이동한다. 어느 방향을 택할지는, 이미 양방향화된 판단들로부터 얻은 타입 정보를 가능하면 활용해야 한다. 예를 들어 이미 L : B를 알고 있다면, 규칙의 다른 부분에 L : B가 다시 등장할 때 그 정보는 검사로 활용하는 편이 낫다.
시작해 보자! 첫 번째 도입/제거 규칙은 False 와 True 다. 둘 다 도입이므로 검사 규칙이어야 한다. 규칙에 다른 판단은 없으니 끝이다.
다음은 도입 규칙인 -> Intr 이다. 주판단은 결론의 Γ ⊢ (\x. L) : A -> B 이므로 이를 검사 규칙으로 만든다. 우리가 검사한다는 것은 이미 타입 B를 안다는 뜻이다. 따라서 L이 정말로 타입 B인지 검사할 수 있다.
-> Elim 은 제거 규칙이다. 주판단은 추상화 Γ ⊢ L : A -> B 이므로 이를 추론 규칙으로 만든다. 이제 추상화의 인자에 필요한 타입이 A라는 것을 알게 되었으므로, 다른 가정 판단인 Γ ⊢ M : A는 검사 규칙으로 만들 수 있다. 마지막으로, 이미 타입 B를 추론했으니 결론도 B를 추론한다.
마지막으로, 도입도 제거도 아닌 규칙이 세 개 있다: Var, Anno, Ty Eq.
Var 는 컨텍스트에서 타입을 이미 알 수 있으므로 추론한다.Anno 의 주판단은 결론 Γ ⊢ (L: A) : A 이다. 주석이 타입을 제공하므로 이를 추론으로 해도 된다. 이제 가정에서는 타입 A를 이미 알고 있으니, 표현식이 정말로 타입 A인지 검사해야 한다. 직관적으로는, 사용자가 주석으로 달아 준 타입을 항이 실제로 갖는지 확인하는 것이다.Ty Eq 는 이것이 없을 때 생길 문제를 해결하기 위해 추가된다. 어떤 항을 추론해야 하는데 그 항이 검사 방향으로만 가능한 경우, 주석을 사용해 화살표 방향을 “뒤집어” 검사 항을 추론 항으로 바꿀 수 있다. 하지만 그 반대(추론 항을 검사 항으로 바꾸는)가 없다! 그래서 이를 위한 방법으로 Ty Eq 를 사용한다. 이렇게 명시적으로 같음(=)을 검사하도록 해 두면, 나중에 서브타이핑을 지원할 때 =를 <:로 바꾸기만 하면 된다. 요컨대 결론은 검사 판단, 가정은 추론 판단이 되어야 한다.따라서 다음과 같은 규칙들을 얻는다(앞의 규칙들과 함께 정리한 것이다):
(원문에는 여기에서 양방향 규칙들이 수식으로 정리되어 있다.)
드디어! 이제 코드를 써 보자. 전체 소스 코드는 내 GitHub의 bidirectional-rs 저장소에서 볼 수 있다. 토크나이저와 파서도 작성해 두었으니, 저장소의 코드로 언어를 가지고 놀아볼 수도 있다. 우리는 항을 AST(추상 구문 트리)로 구현한다.
rust#[derive(Debug, Clone, PartialEq, Eq)] pub enum Type { Bool, Arrow(Box<Type>, Box<Type>), /// Only used when a type error ends type inference early. Unknown, } #[derive(Debug, Clone)] pub enum Expr { True, False, // IfThenElse(Box<TrackedExpr>, Box<TrackedExpr>, Box<TrackedExpr>), Fv(String), Abs(String, Box<TrackedExpr>), App(Box<TrackedExpr>, Box<TrackedExpr>), Anno(Box<TrackedExpr>, Type), } #[derive(Debug, Clone)] pub struct TrackedExpr { pub expr: Expr, pub line: usize, pub column: usize, }
Type에는 기본 타입(Bool)과 화살표 타입이 있다. 또한 “unknown” 타입이 있는데, 이는 올바른 타입을 아직 계산하지 못한 상태에서 타입 오류로 조기에 종료해야 할 때 오류 메시지에만 사용한다.
Expr는 예상대로다. 추가 항으로 IfThenElse가 있는데, 이는 뒤의 연습문제를 위한 것이다. 또한 더 나은 오류 메시지를 제공하기 위해, 재귀하는 변형(variant)들에서는 TrackedExpr를 참조한다. TrackedExpr는 우리가 보고 있는 항이 몇 번째 줄/열인지 “추적(track)”하기 위한 구조체다.
또한 이 구현은 가장 효율적이지 않을 것이다. Clone 트레이트를 쓰지 않고 Copy 타입(예: u64)만으로도 알고리즘이 동작하도록 만드는 방법이 거의 확실히 있을 것이다. 하지만 이 글의 초점은 거기가 아니다.
이 타입체크 방법의 장점 중 하나는 꽤 구체적인 오류 메시지를 제공할 수 있다는 점이다. 우리는 오류 보고에 다음 구조체를 사용하게 된다:
rust#[derive(Debug)] pub enum ErrorKind { /// Expr didn't match type. AnnotationMismatch { caused_by: Box<TypeError> }, /// Expression requires an annotation. AnnotationRequired, /// An application wasn't a function (arrow) type. ApplicationNotArrow { actual: Type }, /// Argument to abstraction had wrong type. ArgWrongType { expected: Type, actual: Type }, /// Checked for the expected type, got the actual type. CheckedWrongType { expected: Type, actual: Type }, /// A free variable was used before it was in scope. UndeclaredFv, } #[derive(Debug)] pub struct TypeError { pub kind: ErrorKind, pub line: usize, pub column: usize, }
서로 재귀하는 두 함수 infer 와 check 를 작성해야 한다. 각각 => 와 <= 에 대응한다. infer 함수는 타입 또는 오류를 반환하고, check 함수는 단위 타입 또는 오류를 반환한다(검사가 실패했을 때만 의미 있는 정보가 있으며, 성공했다면 보고할 것이 없다).
rustuse std::collections::HashMap; pub fn infer( tracked_expr: TrackedExpr, context: &mut HashMap<String, Type>, ) -> Result<Type, TypeError> { // --snip-- } pub fn check( tracked_expr: TrackedExpr, ty: Type, context: &mut HashMap<String, Type>, ) -> Result<(), TypeError> { // --snip-- }
infer부터 시작하자.
rustpub fn infer( tracked_expr: TrackedExpr, context: &mut HashMap<String, Type>, ) -> Result<Type, TypeError> { let line = tracked_expr.line; let column = tracked_expr.column; match tracked_expr.expr { Expr::Fv(s) => { if let Some(ty) = context.get(&s) { Ok(ty.clone()) } else { Err(TypeError { kind: ErrorKind::UndeclaredFv, line, column, }) } }
자유 변수의 경우, 컨텍스트에서 해당 식별자가 어떤 타입에 매핑되는지 확인해야 한다. 존재한다면 매핑된 타입을 반환한다. 없으면 오류를 보고한다.
rustExpr::Anno(expr, ty) => { match check(*expr.clone(), ty.clone(), context) { Ok(_) => Ok(ty), Err(e) => Err(TypeError { kind: ErrorKind::AnnotationMismatch { caused_by: Box::new(e), }, line, column, }), } }
양방향 규칙 Anno에서 L이 타입 A인지 검사했던 것을 떠올려 보자. 위 코드에서는, 항 expr과 타입 ty를 컨텍스트와 함께 check 함수에 넘겨 이를 수행한다(컨텍스트는 그대로 둔다). 성공하면 주석에 적힌 타입을 반환한다. 실패하면, 근본 원인이 된 타입체크 실패를 포함해서 오류를 보고한다.
rustExpr::App(l, m) => match infer(*l, context)? { Type::Arrow(a, b) => match check(*m.clone(), *a, context) { Ok(_) => Ok(*b), Err(TypeError { kind: ErrorKind::CheckedWrongType { expected: a, actual }, line, column, }) => Err(TypeError { kind: ErrorKind::ArgWrongType { expected: a, actual }, line, column, }), Err(e) => Err(e), }, actual => Err(TypeError { kind: ErrorKind::ApplicationNotArrow { actual }, line, column, }), },
이제 적용(application)이다. 이는 -> Elim 규칙에 해당한다. 복잡해 보이지만, 코드 대부분은 오류 보고용이니 겁먹지 말자! 사실 중요한 것은 첫 세 줄뿐이다.
규칙은 먼저 L의 타입을 추론해야 한다고 말한다. 코드에서는 infer를 호출하고 반환된 타입으로 패턴 매칭한다. 화살표 타입이 아니면 타입 오류다. 화살표 타입이라면 A -> B를 추론한 것이다. 이제 인자 M이 올바른 타입 A를 가지는지 확인해야 한다. 그렇다면 적용 결과 타입 B를 반환한다. 아니라면 오류를 보고한다.
rust_ => Err(TypeError { kind: ErrorKind::AnnotationRequired, line, column, }), } }
마지막으로 그 외의 경우라면, 우리는 ‘잘못된 방향’으로 가고 있는 것이므로 사용자가 타입 주석을 달아 도와줘야 한다.
이제 check 함수다.
rustpub fn check( tracked_expr: TrackedExpr, ty: Type, context: &mut HashMap<String, Type>, ) -> Result<(), TypeError> { let line = tracked_expr.line; let column = tracked_expr.column; match tracked_expr.expr { Expr::False | Expr::True => { if ty == Type::Bool { Ok(()) } else { Err(TypeError { kind: ErrorKind::CheckedWrongType { expected: ty, actual: Type::Bool, }, line, column, }) } }
이전처럼 오류 보고를 위해 줄/열을 얻고, 표현식을 매칭한다. 리터럴 false나 true라면, 검사 중인 타입이 Bool인지 확인해야 한다. 아니면 오류를 반환한다.
rustExpr::Abs(s, expr) => match ty { Type::Arrow(a, b) => { context.insert(s.clone(), *a.clone()); let res = check(*expr, *b, context); context.remove(&s); res } _ => Err(TypeError { kind: ErrorKind::CheckedWrongType { expected: ty, actual: Type::Arrow(Box::new(Type::Unknown), Box::new(Type::Unknown)), }, line, column, }), },
추상화에 대해 -> Intr 규칙을 떠올려 보자. 먼저 검사 중인 타입이 화살표 타입 A -> B인지 확인한다. 그런 다음 가정에서, 컨텍스트를 x : A로 확장했을 때 L이 타입 B를 가져야 한다. 코드에서는 화살표 타입인지 확인한 뒤, 문자열 식별자 s를 컨텍스트 HashMap에 삽입한다. 그리고 check를 호출하여 추상화의 본문 expr이 타입 B인지 확인하고, 다시 s를 제거한 뒤, check의 결과를 반환한다.
여기서 중요한 점은, HashMap에 대한 가변 참조를 쓰지 않았다면 식별자를 다시 제거할 필요가 없다는 것이다. 대신 재귀 호출에 넘길 때마다 컨텍스트를 복제(clone)할 수도 있고(그리고 아마 더 저렴한 맵, 예를 들어 ListMap/VecMap 같은 것을 쓰겠지만) 말이다.
rust_ => { let inferred_ty = infer(tracked_expr, context)?; if inferred_ty == ty { Ok(()) } else { Err(TypeError { kind: ErrorKind::CheckedWrongType { expected: ty, actual: inferred_ty, }, line, column, }) } } } }
마지막으로 Ty Eq가 있다. 단순히 infer를 호출하고, 추론된 타입이 검사 중인 타입과 같은지 확인한다.
이게 전부다! 이제 타입체킹 알고리즘을 구동하는 두 함수를 얻었다. 다음처럼 typecheck 함수를 작성할 수 있다:
rustpub fn typecheck(tracked_expr: TrackedExpr, ty: Type) -> Result<(), TypeError> { let mut context = HashMap::new(); check(tracked_expr, ty, &mut context) }
알고리즘이 올바르게 동작함을 보이는 테스트도 작성할 수 있다:
rust#[cfg(test)] pub fn typecheck_assert(tracked_expr: TrackedExpr, ty: Type) { let mut context = HashMap::new(); let checked = check(tracked_expr, ty, &mut context); assert!(checked.is_ok()); } #[cfg(test)] mod tests { use super::*; use crate::parser::parse; #[test] fn simple_typechecking() { let s = String::from("((\\x. x): Bool -> Bool) false"); let parsed = parse(s).unwrap(); typecheck_assert(parsed, Type::Bool); } #[test] fn wrongtype() { let s = String::from("((\\x. if x then false else true): Bool -> Bool -> Bool) false"); let parsed = parse(s).unwrap(); assert!(typecheck(parsed, Type::Bool).is_err()); } }
구현은 꽤 직관적이었다. 코드를 쓰기 전에 어려운 부분(화살표 방향을 어디로 둘지 결정하는 것)을 먼저 했기 때문이다. 힌들리-밀너 추론 알고리즘에 비해 얻는 장점은, 단순히 ‘타입 A와 B를 통일(unify)하지 못했다’라고 말하는 것보다 더 구체적인 오류를 제공할 수 있다는 점이다.
양방향 타입 추론의 흔히 언급되는 단점 중 하나는, 때로는 ‘명백해 보이는’ 곳에도 타입 주석을 추가해야 한다는 점이다. 하지만 타입 주석이 있는 let-바인딩을 언어에 추가하고, 최상위(top-level)의 모든 것을 let-바인딩으로 강제한다면, let-바인딩 본문에서는 추가 타입 주석이 거의 필요 없게 된다! 이런 제한은 언어로서 비현실적이지 않다. 예를 들어 Rust와 C는 최상위 선언이 함수, 상수, 사용자 정의 타입(그리고 매크로 같은 몇 가지 다른 구성요소)이어야 한다. 최상위 함수에 타입 시그니처를 요구하지 않는 Haskell조차도, 타입 시그니처를 사용하는 것을 권장한다. 따라서 사용자 입장에서 그렇게 성가시지 않을 것이다.
if-then-else라는 확장을 생각해 보자:
L : Bool 판단을 검사로 만들든 추론으로 만들든 크게 중요하지 않다. 나는 타입 주석 필요성을 줄여 주기 때문에 검사를 약간 선호하지만, 둘 다 정답이다. 다른 판단들에 대해서는 타입 B가 주어지지 않는다. 그래서 B는 다른 곳에서 주어져야 한다.stlc-exercise라는 Rust 크레이트가 있을 것이다. src/term.rs 파일에 IfThenElse가 변형으로 추가되어 있다. 이제 src/typechecking.rs에서 infer 또는 check 함수에 match arm을 추가하여 IfThenElse 케이스가 처리되고 테스트가 통과하도록 해라. 힌트: 1번에서 If가 검사 규칙임을 알아차렸어야 한다(아니라면 1번 해설을 보라). 따라서 check 함수에 추가해야 한다.조금 만져보다 보면, 이 규칙이 검사 규칙이면서 동시에 추론 규칙으로도 동작한다는 것을 알게 될 것이다. 둘 다 건전한 경우에는 다른 기준을 사용할 수 있다: 코드를 작성하기 귀찮아지는가? 여기서 판단들을 추론 규칙으로 만들면 꽤 귀찮아진다. 예를 들어 if (length l > 2): Bool then (l at 3): Bool else (false: Bool) 같은 코드를 상상해 보라. 따라서 각 판단을 검사로 만들자.
해답은 stlc 크레이트에서 볼 수 있다.
예의를 지켜 달라. 내가 부적절하다고 판단하는 댓글은 삭제될 것이다. 댓글을 제출하면 개인정보 처리방침에 동의하는 것으로 간주한다.
아직 댓글이 없다.