양방향 타입 검사(bidirectional type checking)로 AST를 순회하며 타입 동등성 제약을 생성하는 과정을 구현한다.
URL: https://thunderseethe.dev/posts/bidirectional-constraint-generation/
Title: AST를 타입 제약으로 변환하기
언어 만들기
지난 글에서 우리가 만들고 있는 언어의 AST와 Type을 정리했다. 또한 타입 추론 알고리즘을 조감도로 살펴봤다: 제약 생성(constraint generation), 제약 해결(constraint solving), 해결된 타입을 치환(substitute)하기. 이번에는 타입 추론 알고리즘의 제약 생성 부분을 구현한다.
여러 패스(pass)들이 서로 상태를 공유해야 한다. 이 공유 상태를 담기 위해 TypeInference 구조체를 도입하고, 각 패스를 이 구조체의 메서드로 구현한다:
ruststruct TypeInference { unification_table: InPlaceUnificationTable<TypeVar>, }
unification_table은 제약 해결을 이야기할 때 더 자세히 다룰 것이다. 지금은 타입 변수에서 타입으로의 매핑이라고 생각하면 충분하며, 제약 생성 단계에서는 새로운 타입 변수를 만들고 나중을 위해 추적하는 데 사용한다.
우리는 AST의 문맥 정보(contextual information)로부터 제약들의 집합을 생성한다. 이 문맥을 얻으려면 AST의 모든 노드를 방문하면서 그 노드에 대한 제약을 수집해야 한다. 전통적으로 이는 바텀업(bottom-up) 트리 순회(예: HM의 Algorithm J)로 수행된다. 노드의 모든 자식을 먼저 방문하고, 그 자식들의 문맥을 이용해 현재 노드의 타입을 더 잘 추론한다. 이 접근은 논리적으로 올바르다. 항상 올바른 타입을 추론하고, 타입 오류가 발생해야 할 때 오류를 낸다. 하지만 올바르긴 해도 사용 가능한 정보를 가장 효율적으로 활용하진 못한다. 예를 들어 application 노드에서는 함수 자식이 반드시 함수 타입이어야 함을 알고 있다. 그런데 타입을 오직 바텀업으로만 추론하면, 함수 노드에 대해 임의의 타입을 추론한 뒤 “그 타입은 함수여야 한다”라는 제약을 추가해야 한다.
최근 몇 년간 이러한 비효율을 해결하기 위해 양방향 타입 검사(Bidirectional Type Checking)라는 새로운 접근이 등장했다. 양방향 타입 검사에서는 타입 검사가 두 가지 모드로 동작한다:
infer - 앞서 설명한 HM 타입 시스템과 동일하게 바텀업으로 타입을 추론한다.check - 반대 방향인 탑다운(top-down)으로 동작한다. check에는 타입이 입력으로 전달되며, AST가 그 타입을 갖는지 _검사_한다.이 두 모드는 서로를 상호 재귀(mutually recursively) 호출하면서 AST를 순회한다. 이제 application 노드를 타입 검사할 때 새로운 선택지가 생긴다. application 노드에서 함수 타입을 구성하고, 그 구성한 함수 타입으로 함수 노드를 check할 수 있다. 이렇게 탑다운 문맥 정보를 더 잘 활용하면 더 적은 타입 변수를 만들고 더 나은 에러 메시지를 만들 수 있다. 타입 변수가 적다는 것이 즉각적인 이점처럼 보이지 않을 수도 있지만, 타입 체커를 더 빠르게 만든다. 제약 해결은 우리가 풀어야 할 타입 변수의 수에 부분적으로 제약을 받기 때문이다. 또한 디버깅이 훨씬 쉬워진다. 각 타입 변수는 간접 참조의 한 지점이므로, 디버깅 관점에서도 적을수록 좋다. 따라서 양방향 타입 검사는 “더 좋은” 타입을 추론하게 해주지는 않지만, 순수 바텀업 타입 추론을 약간 확장하는 것만으로도 실질적인 이점을 제공한다.
이제 AST를 순회하며 제약을 수집하는 방법을 알았으니, 제약이 실제로 어떤 모양인지 이야기해보자. 타입 추론의 첫 번째 최소 기능 제품(MVP)에서는 Constraint를 단순한 타입 동등성(type equality)으로만 둘 것이다:
rustenum Constraint { TypeEqual(NodeId, Type, Type) }
두 타입이 “같다”는 의미가 무엇인지는 제약 해결에서 더 다룬다. 지금은 제약 생성의 결과로 타입 동등성들의 집합을 만들어내면 충분하다. 에러 보고를 위해 제약이 어디서 왔는지 기억할 수 있도록 Constraint에 NodeId를 붙인다.
제약 생성은 TypeInference 구조체 위에서 3개의 메서드로 구현된다:
rustimpl TypeInference { fn fresh_ty_var(&mut self) -> TypeVar { ... } fn infer( &mut self, env: im::HashMap<Var, Type>, ast: Ast<Var> ) -> (GenOut, Type) { ... } fn check( &mut self, env: im::HashMap<Var, Type>, ast: Ast<Var>, ty: Type ) -> GenOut { .. } }
fresh_ty_var는 잠깐 제쳐두자. (제약 해결에서 다룰 게 많다!) 이는 unification_table을 사용해 호출할 때마다 유일한 타입 변수를 만들어낸다. 그 외에는 infer와 check의 형태에서 두 모드의 차이를 볼 수 있다. infer는 AST 노드를 받아 타입을 반환하는 반면, check는 AST 노드와 타입을 함께 받는다. 이는 infer는 바텀업으로 동작하고 check는 탑다운으로 동작하기 때문이다.
잠깐 env와 GenOut도 살펴보자. infer와 check는 둘 다 env 파라미터를 받는다. 이는 현재 스코프에서 AST 변수들의 타입을 추적하는 데 사용된다. env는 im 크레이트의 불변(immutable) HashMap으로 구현된다. 불변 해시맵을 쓰면 새로운 변수가 스코프에 들어올 때 쉽게 추가하고, 스코프를 벗어날 때 쉽게 제거할 수 있다. 또한 infer와 check는 둘 다 GenOut을 반환한다. 이는 “제약들의 집합”과 “타입이 주석(annotate)된 AST”의 쌍이다:
ruststruct GenOut { // 해결해야 할 제약들의 집합 constraints: Vec<Constraint>, // 모든 변수가 자신의 타입으로 주석된 Ast typed_ast: Ast<TypedVar>, }
마지막으로, infer나 check에서 오류를 반환할 방법이 없다는 점에 주목하자. 물론 panic을 낼 수도 있지만, 미래의 우리 자신을 위해 관련된 곳에서는 Result로 오류를 반환할 것이다. 다만 제약 생성에서는 그럴 필요가 없다. 우리의 출력은 제약들의 집합이다. 서로 모순되는 제약 집합을 반환하는 것도 완전히 유효하다. 모순은 제약을 풀려고 할 때 발견하고 타입 오류를 낸다. 즉, 제약 생성 단계에는 오류 케이스가 없다. 깔끔하다!
설정은 끝났으니 infer와 check 구현으로 들어가자. 먼저 infer부터 다룬다. AST가 처음에는 무타입(untyped)이므로 타입 추론은 항상 infer부터 시작한다. 따라서 자연스러운 출발점이다. infer는 입력 ast에 대한 단순한 매치(match)다:
rustfn infer( &mut self, env: im::HashMap<Var, Type>, ast: Ast<Var> ) -> (GenOut, Type) { match ast { Ast::Int(i) => todo!(), Ast::Var(v) => todo!(), Ast::Fun(arg, body) => todo!(), Ast::App(fun, arg) => todo!(), } }
각 케이스를 하나씩 보자. 먼저 워밍업으로 쉬운 것부터 시작하자:
rustAst::Int(i) => ( GenOut::new( vec![], Ast::Int(i) ), Type::Int ),
정수 리터럴을 보면 타입이 Int라는 것을 즉시 알 수 있다. 이를 성립시키기 위해 필요한 제약이 없으므로 빈 Vec을 반환한다.
정수보다 한 단계 복잡한 것이 변수 케이스다:
rustAst::Var(v) => { let ty = &env[&v]; ( GenOut::new( vec![], // `Var` 대신 `TypedVar`를 반환 Ast::Var(TypedVar(v, ty.clone()) ), ty.clone(), ) },
변수를 만나면 env에서 그 타입을 조회하고 그 타입을 반환한다. 다만 env 조회가 실패할 수도 있다. 만약 env에 없는 변수를 조회하면 어떻게 될까? 이는 정의되지 않은 변수(undefined variable)라는 뜻이며, 우리는 panic!할 것이다. 우리의 목적에선 괜찮다. 타입 추론 전에 어떤 형태로든 이름 해석(name resolution)을 수행했을 것으로 기대한다. 정의되지 않은 변수를 만난다면 이름 해석 단계에서 이미 오류로 종료했어야 한다.
그 외에는 Var 케이스는 Int 케이스와 매우 비슷하다. 생성할 제약이 없고, 즉시 조회한 타입을 반환한다.
다음은 Fun 케이스를 보자:
rustAst::Fun(arg, body) => { // 아직 알 수 없는 타입을 위한 타입 변수를 생성 let arg_ty_var = self.fresh_ty_var(); // 인자를 env에 (그 타입과 함께) 추가 let env = env.update(arg, Type::Var(arg_ty_var)); // 확장된 env로 함수 본문을 추론 let (body_out, body_ty) = self.infer(env, *body); ( GenOut::new( // body가 만든 제약은 전파된다 body_out.constraints, Ast::fun( // 이제 `Fun`은 `TypedVar`를 가진다 TypedVar(arg, Type::Var(arg_ty_var)), body_out.typed_ast, ), ), Type::fun(Type::Var(arg_ty_var), body_ty), ) }
Fun에서 비로소 비자명한 추론을 한다. 새 타입 변수를 만들고, 이를 env에서 arg의 타입으로 기록한다. 이 새 타입 변수가 스코프에 있는 상태로 body의 타입을 추론한다. 그리고 추론한 본문 타입과 생성한 인자 타입을 사용해 Fun 노드의 함수 타입을 구성한다. Fun 자체가 직접 제약을 만들진 않지만, body가 만든 제약은 그대로 전달한다.
이제 함수 타입을 정하는 방법을 알았으니, 함수 적용(application)을 타입화하는 법을 배우자:
rustAst::App(fun, arg) => { let (arg_out, arg_ty) = self.infer(env.clone(), *arg); let ret_ty = Type::Var(self.fresh_ty_var()); let fun_ty = Type::fun(arg_ty, ret_ty.clone()); // 인자 타입을 추론했으므로, // 검사할 함수 타입을 구성할 수 있다. let fun_out = self.check(env, *fun, fun_ty); ( GenOut::new( // 두 자식 노드의 제약을 모두 전달 arg_out .constraints .into_iter() .chain(fun_out.constraints.into_iter()) .collect(), Ast::app(fun_out.typed_ast, arg_out.typed_ast), ), ret_ty, ) }
App은 이전 케이스들보다 더 미묘하다. arg의 타입을 추론하고, 그 타입을 입력 타입으로 하며 반환 타입은 새 타입 변수인 함수 타입을 구성한다. 이 함수 타입으로 fun 노드가 함수 타입인지 check한다. App 노드의 최종 타입은 새로 만든 반환 타입 변수이며, fun과 arg에서 나온 제약을 합쳐 최종 제약 집합을 만든다.
여기서 왜 fun 노드의 타입을 추론하지 않고 arg의 타입을 먼저 추론했는지 의문이 들 수 있다. fun 타입을 먼저 추론하는 것도 합리적이며, 동일하게 유효한 결과를 낸다. 하지만 우리는 몇 가지 이유로 그렇게 하지 않았다. fun 노드의 타입을 추론하면 그 결과는 불투명(opaque)하다. 반드시 함수 타입이어야 한다는 것만 알고 있고, 추론 결과로 얻는 것은 단지 Type 하나뿐이다. 이를 함수 타입으로 “강제(coerce)”하려면 새로 구성한 함수 타입에 대해 제약을 내보내야 한다:
rustlet (fun_out, infer_fun_ty) = self.infer(env.clone(), *fun); let arg_ty = self.fresh_ty_var(); let ret_ty = self.fresh_ty_var(); let fun_ty = Type::fun(arg_ty.clone(), ret_ty.clone()); let fun_constr = Constraint::TypeEqual(infer_fun_ty, fun_ty); let arg_out = self.check(env, *arg, arg_ty); // ...
arg를 먼저 추론하는 방식에 비해 타입 변수를 하나 더 만들고 제약도 하나 더 만들어야 한다. 큰 차이는 아니며, 사실 더 표현력이 풍부한 타입 시스템에서는 함수 타입을 먼저 추론하는 쪽이 인자 타입을 검사하는 데 유용한 메타데이터를 제공하므로 이 트레이드오프가 가치 있기도 하다. 하지만 우리의 타입 시스템은 그런 범주가 아니므로, 매번 더 적은 제약과 더 적은 타입 변수를 선택한다. 이렇게 “언제 infer 하고 언제 check 할 것인가”가 명확하지 않은 선택이 자주 등장한다. Bidirectional Typing에는 이러한 트레이드오프와 접근 방법을 결정하는 법에 대한 심도 있는 논의가 있다.
이로써 모든 infer 케이스를 다뤘고, 바텀업 순회를 완성했다. 이제 형제격인 check를 이야기해보자. infer와 달리 check는 모든 AST 케이스를 명시적으로 다루지 않는다. 이미 알려진 타입에 대해 AST를 검사하기 때문에, 검사에 성공할 것이라 아는 케이스만 매칭하고 나머지는 모두 “버킷(bucket)” 케이스로 처리한다. 그래도 여전히 케이스별로 다루므로, 높은 수준에서 check는 infer와 매우 비슷하게 생겼다:
rustfn check( &mut self, ast: Ast<Var>, ty: Type ) -> GenOut { match (ast, ty) { // ... } }
AST와 타입을 함께 매치하므로 우리가 관심 있는 케이스만 선택할 수 있다. 이제 각 케이스를 보자:
rust(Ast::Int(i), Type::Int) => GenOut::new( vec![], Ast::Int(i) ),
정수 리터럴은 정수 타입에 대해 자명하게 검사된다. 이 케이스는 불필요해 보일 수도 있다. 버킷 케이스에서 처리하게 해도 되지 않을까? 물론 가능하다. 하지만 이 명시적 케이스 덕분에 타입 변수를 피하고 제약도 피할 수 있다.
다른 명시적 check 케이스는 Fun이다:
rust(Ast::Fun(arg, body), Type::Fun(arg_ty, ret_ty)) => { let env = env.update(arg, *arg_ty.clone()); let body_out = self.check(env, *body, *ret_ty); GenOut { typed_ast: Ast::fun(TypeVar(arg, *arg_ty), body_out.typed_ast), ..body_out } }
Fun 케이스도 간단하다. Type::Fun을 인자 타입과 반환 타입으로 분해한다. env에 arg의 타입이 arg_ty임을 기록하고, 갱신된 env에서 body가 ret_ty를 갖는지 검사한다. infer의 Fun 케이스와 거의 거울상인데, 타입을 위로 끌어올리는 대신 아래로 밀어 넣는다는 차이가 있다.
이 두 케이스만 명시적으로 다루며, 나머지는 모두 버킷 케이스에서 처리한다:
rust(ast, expected_ty) => { let (mut out, actual_ty) = self.infer(ast); out.constraints .push(Constraint::TypeEqual(expected_ty, actual_ty)); out }
마지막으로 버킷 케이스다. 처음 보면 너무 쉬워 보일 수 있다. 알 수 없는 쌍을 만나면 그냥 AST의 타입을 infer로 추론하고, 그 타입이 우리가 검사하려는 타입과 같아야 한다는 제약을 하나 추가한다.
하지만 생각해보면 타당하다. 둘 다 변수 타입이 아닌 경우((Int, Fun) 또는 (Fun, Int))에는 제약을 풀려고 할 때 타입 오류가 발생한다. 한쪽이 변수 타입인 경우에는 제약을 추가함으로써 그 변수에 필요한 문맥 정보를 기록한 셈이 된다. 그 정보가 필요한 곳으로 전파되는 것은 제약 해결에 맡길 수 있다.
이곳이 우리가 제약을 명시적으로 방출(emit)하는 유일한 지점이다. 다른 모든 곳에서는 자식들의 재귀 호출에서 나온 제약을 전파하기만 한다. check에서 다시 infer로 전환되는 지점이야말로, 타입이 맞도록 보장하기 위해 제약이 필요한 유일한 지점이다. infer와 check에 대한 직관이 이런 결론을 이끌어준다. 이것이 양방향 타입 시스템의 통찰과 힘의 일부다. 타입 시스템을 더 복잡한 타입으로 확장할수록 이 가치는 더 커질 것이다.
두 함수가 어떻게 함께 맞물리는지 구현만으로는 보기 어렵다. 예제를 통해 infer와 check가 어떻게 동작하는지 살펴보자. 다음과 같은 인위적인 AST를 생각해보자:
rustAst::app( Ast::fun( Var(0), Ast::Var(Var(0))), Ast::Int(3) )
이는 정수에 적용된 항등 함수(identity function)다. 단순한 예제지만 우리의 모든 AST 노드를 사용하며, check가 infer만으로는 할 수 없는 더 많은 타입 정보를 어떻게 전파하는지 통찰을 제공한다. 예제에서는 환경을 들여다보고 사람이 읽기 쉬운 이름을 쓰기 위해 다음 표기법을 사용한다:
textx, y, z는 변수를 나타낸다 α, β, γ는 타입 변수를 나타낸다 env는 리터럴로 표기하며 { <var0>: <type0>, <var1>: <type1>, ... } 형식을 사용한다. {}는 빈 환경이다.
이 표기법으로 AST 예제를 더 줄여 쓸 수 있다:
rustAst::app( NodeId(0), Ast:fun(NodeId(1), x, Ast::Var(NodeId(2), x)), Ast::Int(NodeId(3), 3) )
이제 루트 App 노드에서 infer를 호출하며 시작한다:
textinfer({}, Ast::App(...))
App 케이스는 먼저 arg의 타입을 추론한다. 인자가 Ast::Int(3)이므로 추론된 타입은 Int다:
textinfer({}, Ast::Int(..., 3)) = Int
이 인자 타입과 새 반환 타입을 사용해, App의 func에 대해 검사할 함수 타입을 구성한다:
textcheck( {}, Ast::Fun(..., x, Ast::Var(..., x)), Fun(Int, Var(α)) )
함수와 함수 타입의 조합은 우리가 명시적으로 처리하는 check 케이스 중 하나다(버킷 케이스로 떨어지지 않는다). 함수 타입을 분해하여 인자와 본문의 타입을 결정한다. 여기서 check의 장점이 드러난다. infer만 있었다면 x에 대해 새 타입 변수를 도입하고, 그 타입 변수가 Int여야 한다는 제약을 추가해야 한다. 대신, 우리는 곧바로 x의 타입이 Int여야 한다는 것을 알 수 있다. env에 x: Int를 추가한 뒤, 함수 타입의 반환 타입에 대해 본문을 검사한다:
textcheck( { x: Int }, Var(..., x), Var(α) )
이는 우리가 아는 check 케이스가 아니므로 버킷 케이스로 간다. 버킷 케이스는 본문의 타입을 infer로 추론한다. 이는 환경에서 x의 타입을 찾아 반환한다:
textinfer({ x: Int }, Var(..., x)) = Int
예제에서는 생략했지만, 여기서는 x가 자신의 타입으로 주석된 새로운 AST도 반환된다: TypeVar(x, Int). 최종 출력에서 이게 어떻게 쓰이는지 볼 것이다.
그리고 검사하려던 타입과 추론된 타입이 같아야 한다는 제약이 추가된다:
rustConstraint::TypeEqual( NodeId(2), Var(α), Int )
이 제약을 출력하면 infer와 check 호출은 끝난다. 콜스택 위로 제약을 전파하면서 typed AST를 구성한다. 모든 재귀 호출이 반환된 뒤에는 제약 집합(단 하나의 제약만 있음):
rustvec![Constraint::TypeEqual(..., Var(α), Int)]
그리고 typed AST:
rustAst::app( ..., Ast::fun( ..., TypeVar(x, Int), Ast::Var(..., TypedVar(x, Int)) ), Ast::Int(..., 3) )
전체 AST의 최종 타입(첫 infer 호출이 반환하는 타입)은 Var(α)다. 함수 타입이 Fun(Int, Var(α))였음을 기억하자. 이는 제약 해결 이후에 최종 치환(substitution) 단계가 왜 필요한지 보여준다. 제약을 풀어 α = Int임을 알아야만 전체 AST의 타입이 Int라고 올바르게 결론낼 수 있다.
이로써 제약 생성을 마쳤다. 제약 생성의 출력으로 우리는 세 가지를 만든다: 제약들의 집합, typed AST, 그리고 전체 AST에 대한 Type. typed AST에는 모든 변수에 타입이 연결되어 있으며(거기서 모든 노드의 타입도 복구 가능), 하지만 여전히 많은 부분이 미지의 타입 변수다. 이 AST는 일단 저장해두고, 제약 집합을 해결해 모든 타입 변수에 대한 해를 얻은 뒤 다시 살펴볼 것이다. 그러면 자연스럽게 다음 글에서는 제약 해결을 구현할 것이다. 전체 소스 코드는 동반 레포(companion repo)에서 확인할 수 있다.