URL: https://thunderseethe.dev/posts/unification/

타입 추론 매듭짓기

Making a Language

제약 해결(Constraint Solving) Link to heading

지난주 에피소드에서는 양방향 타입 시스템으로 제약(constraint)들의 집합을 생성했다. 이제 제약 집합이 있으니 이를 풀어볼 수 있다. 그런데 제약을 “푼다”는 건 무슨 뜻일까? 제약이란 우리 타입들에 대해 참이어야 하는 어떤 조건이다. 제약이 요구하는 바를 참이라고 증명할 수 있다면, 그 제약을 푼 것이다. 우리의 Constraint 데이터 타입은 단순히 타입 동등성(type equality)이므로, 두 타입이 같음을 증명함으로써 모든 제약을 풀 수 있다. 만약 두 타입이 같음을 증명하지 못하면 타입 오류가 발생하며, 즉시 중단할 수 있다.

좋아, 그럴듯하다. 하지만 질문이 하나 남는다. 두 타입이 “같다”는 건 무슨 의미일까? 여기서는 구조적(structural) 동등성을 기준으로 타입을 같다고 판단한다. 각 타입의 트리를 살펴보고, 같은 노드이며 모든 자식들이 서로 같다면 두 타입을 같다고 본다. 이는 타입 변수(type variable)를 제외하면 아주 잘 동작한다. 타입 변수의 경우 단순히 “변수끼리 같다/다르다”를 확인하는 것만으로는 충분하지 않다. 타입 변수는 어떤 타입(심지어 다른 타입 변수)도 될 수 있다. 타입 변수를 다른 타입과 비교할 때, “그 타입 변수가 그 타입을 의미한다”고 자유롭게 가정하면 두 타입을 쉽게 같게 만들 수 있다. 개별 동등성 하나만 놓고 보면 훌륭하지만, 제약 전체 집합에 대해 무턱대고 이런 식으로 처리하면 문제가 생길 수 있다. 예를 들어 어떤 동등성에서는 타입 변수 a가 Type::Int라고 가정하고, 다른 동등성에서는 Type::Fun(Type::Var(b), Type::Var(c))라고 가정할 수 있다. 타입 변수는 어떤 타입이든 될 수 있지만, 동시에 두 타입이 될 수는 없다. 제약들의 집합이 어떤 타입 변수가 두 개의 서로 다른 타입을 동시에 의미해야만 성립한다면 타입 오류다. 이를 해결하려면, 제약을 풀어가는 동안 타입 변수에 어떤 타입을 할당했는지 기억해야 한다.

타입 변수를 타입에 대응시키는 할당을 타입 치환(type substitution) 이라고 한다. 제약 해결 과정에서 타입 치환을 점진적으로 구축하고, 마지막에는 모든 타입 변수에 대한 항목이 치환에 들어 있기를 기대한다. 이렇게 “타입들을 같게 만드는 치환을 구축함으로써 제약 집합을 푸는” 과정에는 이름이 있는데, 바로 유니피케이션(Unification)이다.

유니피케이션(Unification) Link to heading

유니피케이션은 제약 집합을 참으로 만들 수 있는 타입 치환이 존재하는지 결정하는 과정이다. 그런 치환이 없다면(늘 그렇듯) 타입 오류다. 유니피케이션은 기본적으로 탐색(search) 문제다. 타입 변수들에 여러 타입을 대입해 보며, 동작하는 할당을 찾거나 그런 할당이 존재할 수 없음을 알아내야 하기 때문이다. 여기서는 하지 않겠지만, 무식하게(bruteforce) 해법을 찾으려 한다면 굉장히 오래 걸릴 수도 있다고 상상할 수 있다. 다행히 이번에도 수학이 도와준다. 유니피케이션은 잘 연구된 주제이며, 거의 선형 시간에 타입을 유니파이할 수 있는 알고리즘들이 몇 가지 발견되어 있다. 우리는 그중 하나를 “진열대에서 꺼내” 빠른 타입 추론으로 즐겁게 나아가면 된다.

유니온-파인드(Union-find) Link to heading

유니피케이션을 빠르게 만드는 비밀은 타입 치환을 어떻게 저장하느냐에 있다. 타입 치환을 구축하기 위해 유니온-파인드(Union-Find) 자료구조를 사용하겠다. 유니온-파인드에 대해 말할 수 있는 게 정말 많지만 대부분은 건너뛰겠다. 유니온-파인드는 우리 유니피케이션 알고리즘의 중요한 구현 디테일일 뿐이다. 유니온-파인드는 서로소(disjoint) 집합들의 모음을 효율적으로 저장하는 방법이고, 여기서는 “타입들의 집합”을 저장하게 된다. 이를 위해 두 가지 연산을 제공한다: union과 find. 각 서로소 집합은 그 집합의 원소 중 하나가 대표(representative)로서 집합을 나타낸다. union은 두 집합을 합쳐 대표들을 결합해 새 대표를 만든다. find는 어떤 타입이 속한 집합을 찾아 그 집합의 대표를 반환한다.

이 두 연산이 어떻게 타입 치환 구현으로 이어지는지 바로 떠오르지 않을 수 있다. 유니온-파인드로 타입 치환을 구현하는 방식을 보기 위해, 제약 생성에서 대충 지나갔던 코드 unification_table과 fresh_ty_var를 다시 보자:

struct TypeInference {
  unification_table: InPlaceUnificationTable<TypeVar>,
}

fn fresh_ty_var(&mut self) -> TypeVar {
  self.unification_table.new_key(None)
}

이제 맥락이 생기니 unification_table이 더 이해된다. 이것이 바로 우리의 유니온-파인드 자료구조다. fresh_ty_var를 호출할 때마다 유니온-파인드에 새로운 “빈 집합”을 만들고 그 대표를 반환한다. 직접 유니온-파인드를 구현하지는 않을 것이다(재미있겠지만). rustc 팀이 그들의 유니온-파인드를 ena 크레이트로 공개해 두었으니, 이를 유니온-파인드 구현으로 사용하겠다.

제약 해결을 시작할 때, 유니온-파인드에는 이미 각 타입 변수마다 그 변수 자체를 대표로 갖는 집합이 하나씩 존재한다. 이는 “모든 변수가 자기 자신으로 매핑된다”는 타입 치환이라고 생각할 수 있다. 유니파이하면서 우리는 union을 호출해 집합들을 합친다. 두 집합을 합치면, 그 집합 안의 모든 타입 변수는 이제 새 대표로 매핑된다. 유니피케이션 중 타입 변수를 치환해야 한다면(스포일러: 하게 된다), find를 호출해 현재 대표를 조회하면 된다.

다시 유니피케이션으로 Link to heading

이제 거의 선형 시간에 타입 치환을 유지하는 방법을 알았으니, 타입을 어떻게 유니파이하는지 살펴보자. 유니피케이션 구현은 unification 함수로 시작한다:

fn unification(
  &mut self, 
  constraints: Vec<Constraint>
) -> Result<(), TypeError> {
  for constr in constraints {
    match constr {
      Constraint::TypeEqual(left, right) => 
        self.unify_ty_ty(left, right)
            .map_err(|kind| TypeError { kind, node_id })?,
    }
  }
  Ok(())
}

아직은 볼 게 많지 않다. 각 제약마다 unify_ty_ty를 호출해 유니피케이션 이후에도 타입이 같아지는지 확인한다. 어떤 개별 제약에서든 오류를 만나면, 즉시 중단하고 더 이상 제약을 풀려 하지 않는다.

좋다. 그럼 unify_ty_ty는 어떻게 생겼을까?

fn unify_ty_ty(
  &mut self, 
  unnorm_left: Type, 
  unnorm_right: Type
) -> Result<(), TypeErrorKind> {
  let left = self.normalize_ty(unnorm_left);
  let right = self.normalize_ty(unnorm_right);
  match (left, right) {
    // ...
  }
}

오, 큰 match 문이겠군. 이제 익숙하다. 그런데 위쪽의 normalize_ty는 뭘까? 유니파이하면서 타입 치환을 구축하고, 타입 변수에 타입을 할당해 나가고 있다. 어떤 타입 변수를 어떤 타입으로 “해결(solve)”했다면, 제약에서 그 변수를 다시 만날 때마다 매번 다시 해결하고 싶지 않다. 이미 해결된 타입 변수를 재해결하는 일을 피하기 위해, 해결된 타입 변수를 유니파이할 때는 먼저 그 변수를 해당 타입으로 치환해야 한다. 이렇게 하면 타입 변수는 오직 하나의 타입만 할당받고, 그 타입 변수에 할당될 수 있었던 다른 타입들과도 일관되게 같아진다. 그래서 타입을 유니파이하기 전에, normalize_ty에서 가능한 모든 치환을 타입에 적용한다:

fn normalize_ty(
  &mut self, 
  ty: Type
) -> Type {
  match ty {
    Type::Int => Type::Int,
    Type::Fun(arg, ret) => {
      let arg = self.normalize_ty(*arg);
      let ret = self.normalize_ty(*ret);
      Type::fun(arg, ret)
    }
    Type::Var(v) => match self.unification_table.probe_value(v) {
      Some(ty) => self.normalize_ty(ty),
      None => Type::Var(self.unification_table.find(v)),
    },
  }
}

정규화(normalize)할 때는 유니온-파인드에서 타입 변수의 대표를 조회하고, 타입 변수의 모든 위치가 대표로 바뀐 새 타입을 반환한다. 유니온-파인드에서 변수에 해당하는 타입을 꺼내어 그 타입으로 치환할 때, 그 타입에도 normalize_ty를 호출한다는 점을 주의하자. 그 타입 안에 또 다른 타입 변수들이 있을 수 있고, 그것들이 이미 해결되었을 수 있으므로 정규화해서 가능한 한 “가장 많이 알려진 타입”을 만들기 위함이다. 만약 변수가 어떤 타입으로도 해결되지 않았다면, find를 호출해 유니온-파인드의 루트 변수를 반환한다. 이는 두 변수를 서로 유니파이한 결과로 “한 타입 변수가 다른 타입 변수로 해결되는” 상황을 처리한다.

좋다! 이제 정규화로 제거할 수 있는 타입 변수들을 모두 제거했으니, 유니피케이션 케이스들을 분해해 보자:

(Type::Int, Type::Int) => Ok(()),

관례대로 Int 케이스부터 시작하자. 임의의 두 Int 타입은 자명하게 같으므로 즉시 반환하면 된다. 다음은 함수 타입이다:

(Type::Fun(a_arg, a_ret), Type::Fun(b_arg, b_ret)) => {
  self.unify_ty_ty(*a_arg, *b_arg)?;
  self.unify_ty_ty(*a_ret, *b_ret)
}

두 함수 타입은 인자 타입과 반환 타입이 각각 같을 때만 같다. 따라서 인자 타입끼리 유니파이하고, 반환 타입끼리도 유니파이한다. 다음은 타입 변수 유니파이다:

(Type::Var(a), Type::Var(b)) => {
  self.unification_table
    .unify_var_var(a, b)
    .map_err(|(l, r)| TypeErrorKind::TypeNotEqual(l, r))
}

여기서 처음으로 타입 치환에 정보를 추가한다. 두 타입 변수가 같으려면, 유니온-파인드에서 두 변수가 속한 집합을 합칠 수 있어야 한다. 두 변수가 이미 “타입을 대표로” 가지고 있는 상태라면 합치기가 실패할 수 있다. 그런 경우 대표 타입들끼리 서로 같은지 확인해야 한다. 만약 같지 않으면 union에 실패하고 타입 오류를 반환한다. 타입들이 같거나(따라서 합쳐도 모순이 없거나), 또는 한쪽만 대표 타입을 가지고 있다면 집합을 합친다. 그러면 두 집합에 있던 모든 타입 변수는 새 대표 타입으로 매핑된다. 어떤 타입이 대표가 되는지는 중요하지 않다. 같기만 하면 되므로 임의로 하나를 고르면 된다. 다음은 변수와 다른 타입을 유니파이하는 경우다:

(Type::Var(v), ty) | (ty, Type::Var(v)) => {
  ty.occurs_check(v)
    .map_err(|ty| TypeErrorKind::InfiniteType(v, ty))?;
  self
    .unification_table
    .unify_var_value(v, Some(ty))
    .map_err(|(l, r)| TypeErrorKind::TypeNotEqual(l, r))
}

이 케이스는 실제로 타입 변수에 타입을 할당하는 지점이다. 타입 변수가 (변수가 아닌) 타입과 마주치면 둘을 유니파이하여, 구체 타입(concrete type)이 그 타입 변수가 속한 집합의 대표가 되게 만든다. 이후부터는 그 타입 변수(또는 같은 집합의 다른 타입 변수)를 정규화할 때 이 타입이 반환된다.

그 전에 occurs_check를 호출해, 필요하다면 InfiniteType 오류를 만든다. occurs_check는 타입을 순회하면서 우리가 유니파이하려는 타입 변수가 그 타입 내부에 등장하지 않는지 확인한다. 이를 피해야 하는 이유는 타입 치환에 사이클이 만들어지기 때문이다. 이는 정규화에서 문제가 된다. 정규화는 어떤 타입으로 치환할 때 먼저 그 타입을 정규화한다. 그런데 그 타입 안에 원래의 변수가 포함되어 있다면, 다시 그 변수를 lookup하고 또 정규화하고… 무한 루프가 된다. 무한 루프는 빠른 타입 추론에 도움이 되지 않으므로, 변수와 타입을 유니파이하기 전에 사이클을 만들지 않는지 확인해야 한다. 마지막으로 타입 오류 케이스다:

(left, right) => Err(TypeErrorKind::TypeNotEqual(left, right)),

이 마지막 케이스는 타입들이 서로 맞지 않는 모든 조합을 포괄한다(예: (Int, Fun(...)) 등). 이는 제약 집합에 모순이 있음을 의미한다. 할 수 있는 일은 타입 오류를 반환하고 즉시 중단하는 것뿐이다.

이로써 제약 집합을 성공적으로 해결하여 타입 치환을 만들었다. 제약 해결 단계는 이렇게 정리된다. 이제 마지막으로, 모든 것을 연결해 타입 추론 시스템을 완성해야 한다.

매듭짓기(Tying the knot) Link to heading

제약을 생성하고 해결한 뒤에는 세 가지가 있다:

• 전체 AST에 대한 추론된 타입
• 모든 변수가 타입 주석으로 표시된 typed AST
• 모든 타입 변수를 그 타입으로 매핑하는 타입 치환

타입 추론의 마지막 단계는 타입 치환을 사용해, 제약 생성 단계에서 얻은 추론 타입들을 모두 “해결된 타입”으로 만드는 것이다. 이를 위해 AST를 순회하면서 만나는 각 타입을, 타입 치환을 사용해 정규화한다. 이 코드는 매우 기계적이라 자세히 다루지는 않겠지만, 보고 싶다면 전체 소스를 참고하라.

일반화(Generalization) Link to heading

AST를 순회하며 타입을 정규화하다 보면, 아직 다루지 않은 케이스를 만나게 된다. 타입 치환이 어떤 타입 변수를 자기 자신(또는 다른 타입 변수)으로 해결한다면 어떻게 해야 할까? 그런 일이 실제로 일어날까? 물론이다. 심지어 예시를 만드는 것도 어렵지 않다:

let x = Var(0);
let id = Ast::Fun(..., x, Ast::Var(..., x));

여기서 이 AST에 대해 어떤 타입을 추론해야 할까? x의 타입을 추론하기에 충분한 문맥 정보가 없다. 제약 해결 후에는 x의 타입이 어떤 타입 변수로 해결되어 있음을 발견하게 된다.

이는 사실 괜찮다. 오히려 의도된 동작이다. 이런 상황은 전체 AST의 타입이 다형적(polymorphic)이라는 뜻이며, 타입 변수 자체를 포함해야 한다는 의미다. 이를 처리하는 방법은 타입 추론이 끝날 때 바인딩되지 않은(unbound) 타입 변수들을 일반화(generalize) 하는 것이다. 타입과 그 타입에 포함된 바인딩되지 않은 타입 변수를 함께 묶은 것을 타입 스킴(type scheme)이라고 한다. 따라서 예시 AST id에 대해 추론되는 타입 스킴은 다음과 같다:

TypeScheme {
  unbound: vec![TypeVar(0)],
  ty: Type::Fun(Type::Var(TypeVar(0)), Type::Var(TypeVar(0)))
}

바인딩되지 않은 타입 변수가 하나 있고, 함수는 그 타입 변수를 받아 그대로 반환한다. 누군가 이 함수를 호출하려면 타입 변수에 대한 구체 타입을 제공해야 하고, 그때서야 함수의 타입이 완전히 정해진다.

결론(Conclusion) Link to heading

이제 모든 조각이 제자리에 놓였으니, 이들을 꽤 간결하게 붙여 type_infer 함수에서 타입 추론을 수행할 수 있다:

fn type_infer(ast: Ast<Var>) -> Result<(Ast<TypedVar>, TypeScheme), TypeError> {
  let mut ctx = TypeInference {
    unification_table: InPlaceUnificationTable::default(),
  };

  // Constraint generation
  let (out, ty) = ctx.infer(im::HashMap::default(), ast);

  // Constraint solving
  ctx.unification(out.constraints)?;

  // Apply our substition to our inferred types
  let (mut unbound, ty) = ctx.substitute(ty);
  let (unbound_ast, typed_ast) = ctx.substitute_ast(out.typed_ast);
  unbound.extend(unbound_ast);

  // Return our typed ast and it's type scheme
  Ok((typed_ast, TypeScheme { unbound, ty }))
}

이 함수는 단계별로도 깔끔하게 나뉜다. 제약 집합을 생성하고, 이를 치환으로 해결한 뒤, 그 치환을 적용한다. 전체 소스 코드는 GitHub 레포로 공개되어 있으니, 여기서 확인하고 직접 가지고 놀아볼 수 있다.

해냈다! 이제 우리의 간단한 언어에 대해 타입을 추론할 수 있다. 성능을 더 끌어올리거나 더 강력한 타입을 추론하도록 개선할 여지는 엄청나지만, 그건 다음에 하자. 이 글은 디테일을 얼마나 많이 생략했는지에 비해 이미 지나치게 길다. 그래도 가지고 놀 수 있는 훌륭한 MVP를 만들었다. 파서만 끝없이 만지작거리다 막히는 일도 없었다. 다음에는 첫 오류를 넘어 계속 진행하기를 통해 타입 추론을 더 견고하게 만들 것이다.