URL: https://thunderseethe.dev/posts/row-types/

로우 타입 보트, 물살을 가르며

언어 만들기

이 글은 언어 만들기 시리즈의 일부입니다. Rust를 사용해 프로그래밍 언어를 구현하는 방법을 가르치는 시리즈죠.

이 글은 우리 언어에 데이터 타입을 추가하는 방법인 로우 타입(row types)을 위한 타입 추론을 다룹니다. 기본 언어를 확장해 로우 타입과 그 구성 요소들을 지원하도록 합니다.

지난 편에서는 간단한 타입 추론 엔진을 처음부터 끝까지 조립했습니다. 아무런 애너테이션 없이도 함수와 정수를 모두 검사할 수 있을 만큼 강력했죠. 완벽해 보이지만, 우리의 타입 추론(그리고 언어)에는 아주 자그마한 기능이 하나 부족합니다. 데이터 타입이 없습니다. 오늘 편에서는 로우 타입 지원을 추가해 이를 바로잡아 보겠습니다.

로우 타입은 레이블(label)에서 타입으로의 매핑입니다. 예를 들어:

( x : Int, y : Int )

이는 x와 y 두 레이블이 있고 둘 다 Int 타입에 매핑되는 로우입니다. 로우는 두 가지 방식으로 사용됩니다:

• 곱(product) 타입으로 사용될 때: x, y 두 필드를 가진 struct가 됩니다.
• 합(sum) 타입으로 사용될 때: x, y 두 변이를 가진 enum이 됩니다.

대수적 데이터 타입(ADT)이나 클래스 같은 전통적인 명목적(nominal) 데이터 타입과 달리, 로우 타입은 구조적(structural) 입니다. 명목적 타입 시스템에서는 각 데이터 타입이 새로운 이름을 도입하고 그 이름은 오직 자기 자신과만 같죠. 구조적 로우 타입에서는 더 관대한 동치 정의를 씁니다. 두 로우 타입은 같은 레이블을 갖고, 그 레이블들이 같은 타입에 매핑될 때 서로 같습니다. 다시 말해 이름이 아니라 구조를 보고 타입 동치를 결정합니다.

로우 시스템은 다양한 구현 방식이 고안되었습니다. 우리의 구현은 Abstracting Extensible Data Types에 자세히 설명된 아이디어에 기반합니다. 이보다 더 탄탄한 기반은 없을 겁니다. 이 구현의 특징은 로우의 조합을 표현하기 위해 trait 같은 메커니즘을 사용한다는 점입니다. 이 메커니즘은 우리 매개변수적 다형 타입 시스템에 자연스럽게 들어맞습니다. 다른 로우 타입 시스템들은 서브타이핑이나 존재(presence) 다형성을 쓰는데, 이는 우리 타입 시스템에 매핑하기가 더 어렵습니다.

그럼 로우 조합(row combination)이란 뭘까요? 두 로우가 공통 필드를 하나도 갖지 않는다면, 둘을 결합해 새로운 로우를 만들 수 있습니다:

( x : Int ) + ( f : String, y: Int ) = ( f : String, x : Int, y : Int )

더 좋은 점은 로우 변수(row variable)를 도입해 다른 로우와 결합할 수도 있다는 겁니다:

ρ + ( x : Int, y : Int ) = α

이 유용함은 바로 와닿지 않을 수도 있습니다. 이렇게 로우 변수를 결합하면 로우를 제네릭하게 다룰 수 있는 방법이 생깁니다. 로우 조합을 통해 로우 변수들 사이의 관계를 만들고, 제네릭 로우에서 동작하는 함수의 타입을 기술할 수 있습니다. 제네릭 타입에서 동작하는 함수의 타입을 기술하기 위해 trait와 타입 변수를 쓰는 것과 같은 방식이죠.

덕분에 데이터가 문제 도메인을 아주 정확하게 표현할 수 있습니다. 명목적 시스템에서는 유효한 필드 부분집합만 사용하도록 런타임 어서션에 의존하곤 합니다. 하지만 로우 타입에서는 유효한 필드만 남을 때까지 로우를 마음껏 잘라낼 수 있습니다.

ADT나 클래스에 비해 로우 타입은 언어에서 데이터 타입을 다루는 방법으로서 꽤 덜 탐구된 편입니다. OCaml의 한 구석이라든지, JavaScript에 정적 타입을 덧대는 언어들(PureScript, TypeScript 등)에서나 찾아볼 수 있죠. 학계에는 로우에 관한 연구가 무성하지만, 주류로 자라난 것은 많지 않습니다. 아쉽죠. 마침 저는 언어를 설계하고 있으니, 뭔가를 해보기 좋은 위치에 있기도 하고요.

이제 이념적 동기가 가득 찼으니, 로우 타입을 추론하도록 타입 추론을 확장하는 계획을 세워봅시다. 로우 타입을 지원하려면 3가지 수정이 필요합니다:

1. 로우 생성자를 위한 AST 노드 만들기
2. 노드에서 로우 타입 제약(constraint) 생성하기
3. 로우 제약을 단일화(unify)하여 로우 타입을 풀기

새 AST 노드

로우를 지원하려면 여섯 개의 새 노드가 필요합니다. 많아 보일 수 있습니다(우리 AST 케이스가 250% 증가합니다!). 하지만 이 노드들은 앞으로 영원히 우리의 모든 데이터 요구를 지원할 겁니다. 영원한 모든 데이터 타입을 위해 여섯 개면 싸게 먹히는 거죠.

새 노드는 3쌍으로 나뉘며, 각 쌍은 생성자(constructor)와 소멸자(destructor)로 구성됩니다:

• 곱 타입(product types)
• 합 타입(sum types)
• 레이블 타입(label types) – 일반 항(term)을 로우 항으로 변환하거나 그 반대로 변환

곱 타입 쌍은 다음과 같습니다:

// 나중에 필요할 거예요
// 딱 넣을 만한 자리가 없었어요
// 미안합니다 :(
enum Direction {
  Left,
  Right,
}

// 하나 더 억지로 끼워넣기
type Label = String
// 이제 진짜로 좋은 stuff

enum Ast<V> {
  // ...
  Concat(NodeId, Box<Self>, Box<Self>),
  Project(NodeId, Direction, Box<Self>),

Concat은 두 곱 타입을 결합해 더 큰 곱 타입을 만듭니다.

Project는 곱 타입을, 그 필드의 부분집합으로 이루어진 더 작은 곱 타입으로 매핑합니다.

다음 쌍은 합 타입입니다:

Inject(NodeId, Direction, Box<Self>),
  Branch(NodeId, Box<Self>, Box<Self>),

Inject는 작은 합 타입을, 그 작은 합 타입의 케이스들을 포함하는 더 큰 합 타입으로 매핑합니다.

Branch는 합 타입 소멸자 두 개를 결합해, 두 합 타입의 조합에 대한 큰 소멸자를 만듭니다.

이는 match 문을 로우 방식으로 만든 버전입니다. 실제로 어떻게 보이는지는 다루지 않겠지만, 관심 있다면 그 논문에 이를 위한 섹션이 있습니다.

새 곱/합 노드에는 새 로우를 만드는 방법이 없습니다. 기존 로우에서 더 큰/작은 로우를 만드는 방법만 있죠. Haskell이라면 데이터로서 Concat 노드를 무한 트리로 만들게 허용할지도 모르지만, 우리는 더 엄격합니다. 다행히 이 문제를 해결할 노드가 두 개 남아 있습니다:

//...
  Label(NodeId, Label, Box<Self>),
  Unlabel(NodeId, Box<Self>, Label),
}

Label은 항(term)을 싱글턴 로우(singleton row)로 바꿉니다. Unlabel은 지정한 레이블을 제거해 싱글턴 로우를 다시 일반 항으로 바꿉니다. Unlabel은 어떤 로우(싱글턴뿐 아니라)에도 적용될 수 있을 것처럼 보이죠. 실제로 그럴 수도 있지만, 우리는 Unlabel이 오직 싱글턴 로우에만 적용되도록 요구할 겁니다. 제약 생성(constraint generation)을 보면 더 이해가 될 거예요. Unlabel에 단일 레이블을 요구하면 정확한 로우 조합을 추론하는 데 도움이 됩니다. 여러 레이블을 가진 로우를 unlabel하고 싶다면, 먼저 projection으로 싱글턴으로 만든 다음 unlabel합니다.

이게 새 노드들의 전부입니다. 어떤 항이든 싱글턴 로우로 올린 다음, concat이나 inject로 더 큰 로우에 집어넣을 수 있습니다. 이론적으로는 이것만으로 충분하지만, 실제로 모든 로우를 Concat들의 연쇄로 만들려면 너무 장황합니다. 실제 구현에서는 싱글턴뿐 아니라 여러 레이블을 한 번에 구성하는 로우 생성도 지원할 겁니다.

이 노드들로 우리가 좋아하는 모든 데이터 작업을 어떻게 할까요? 두 로우를 결합하고 그 멤버 하나에 접근하는 예를 봅시다:

Ast::unlabel(
  ...,
  Ast::project(
    ...,
    Left,
    Ast::concat(
      ...,
      Ast::label(
        ...,
        "x", 
        Ast::Int(..., 4)),
      Ast::label(
        ...,
        "y", 
        Ast::Int(..., 3)),
    )
  ),
  "x"
)

여기서 Label은 두 번 쓰여 x : Int와 y : Int 두 싱글턴 로우를 만듭니다. 이를 concat해 하나의 곱 로우 { x : Int, y : Int }를 만듭니다. 그 곱 로우에서 { x : Int }를 project로 뽑아내고, 마지막으로 unlabel해서 정수 4를 다시 얻습니다.

로우 타입

기본 타입 추론에서 했던 것처럼, 새 AST 노드로부터 어떤 새 타입이 필요한지 알 수 있습니다. 값을 만들어내는 새 생성자마다 타입이 필요하니까요:

• Concat - Product 타입
• Inject - Sum 타입
• Label - 레이블이 달린 타입. 이를 Label 타입이라 부르겠습니다

여기서 중요한 점: 새 타입들 중에는 로우 타입이 없습니다.

더 심각한 문제: 사실 지금까지 계속 거짓말을 했습니다.

로우 타입은 없습니다. 애초에 없었습니다. 로우는 그 자체로 타입이 될 수 없습니다. 곱이나 합으로 감쌀 때에만 타입이 됩니다. 이는 우리의 새 Type 노드에 반영됩니다:

enum Type {
  // ... 이전 케이스들
  // 위에 로우 타입 숨겨둔 거 아닙니다 진짜로
  /// 곱 타입
  Prod(Row),
  /// 합 타입
  Sum(Row),
  /// 싱글턴 로우의 타입
  Label(Label, Box<Self>),
  // 로우 타입은 없습니다 ¯\_(ツ)_/¯
}

좋습니다. 신뢰가 산산조각 났으니… 로우가 타입이 아니라면 대체 뭔가요?

struct RowVar(u32);

enum Row {
  Open(RowVar),
  Closed(ClosedRow),
}

별로 도움은 안 되네요. 로우는 열려(open) 있고 로우 변수이거나, 닫혀(closed) 있고 ClosedRow라는 무엇인가입니다. RowVar는 그냥 정수니까 별 도움은 안 됩니다. ClosedRow가 도와주길 바라봅시다:

struct ClosedRow {
  // 사전순으로 정렬됨
  fields: Vec<Label>,
  // fields의 각 필드에 대응하는 타입
  values: Vec<Type>,
}

익숙한 모습이 보이기 시작하네요. 닫힌 로우는 필드에서 타입으로의 매핑을, 정렬된 벡터 두 개로 저장합니다.

닫힌 로우는 HashMap(혹은 최소한 BTreeMap)일 거라 기대할 수도 있습니다. 하지만 단일화 중에는 로우의 필드를 비교하여 빠르게 동치성을 확인하는 게 유용합니다. 이를 쉽게 하기 위해 필드와 값을 분리해서 저장합니다. 자세한 내용은 나중에 보겠지만, 엔트로피에도 질서가 있다는 것만 믿어주세요.

타입 쪽에서 마지막으로 필요한 기계장치는 새 로우 제약입니다. 새 제약은 로우 조합입니다:

enum Constraint {
  // ... 이전 케이스들
  RowCombine(NodeId, RowCombination),
}
struct RowCombination {
  left: Row,
  right: Row,
  goal: Row,
}

이것이 사실(fact)이 아니라 제약(constraint)인 이유는, 로우를 결합하는 것이 항상 유효하진 않기 때문입니다. left와 right가 겹치는 필드를 가지면 결합할 수 없습니다. 단일화 과정에서 우리는 주어진 대로 로우들을 결합할 수 있음을 납득(증명)하려고 할 겁니다. 납득할 수 없다면 타입 오류입니다.

이게 전부입니다! 로우를 지원하는 데 필요한 새 제약은 하나뿐입니다. 여섯 개의 새 AST 노드와 세 개의 새 타입이 필요했던 것치곤 너무 좋아 보이죠. 정말 제약 하나로 충분한지 확인하기 위해, 이 로우 제약으로 새 로우 노드들을 어떻게 타이핑하는지 봅시다:

정말로 전부 타이핑되네요. 저자라는 입장에서 자신감 있는 척했지만, 사실 여러분만큼 저도 회의적이었습니다. 저 Abstract Extensible Data Types 논문은 정말 뭔가를 알고 있어요.

좋습니다. 제약 하나면 충분하다는 걸 믿게 됐습니다. 이제 해야 할 일은 이 제약을 생성하는 것뿐입니다.

로우 제약 생성

생성의 본론으로 가기 전에, TypeInference 구조체에 약간의 보일러플레이트가 필요합니다:

struct TypeInference {
  // ... 이전 필드들
  row_unification_table: 
    InPlaceUnificationTable<RowVar>,
  partial_row_combs: 
    BTreeSet<RowCombination>,
  row_to_combo: 
    HashMap<NodeId, RowCombination>,
  branch_to_ret_ty:
    HashMap<NodeId, Type>,
}
// 여기서 헬퍼 메서드도 추가합시다
impl TypeInference {
  // ... 이전 것들
  /// 유일한 로우 변수를 만든다
  fn fresh_row_var(&mut self) 
      -> RowVar {
    self.row_unification_table.new_key(None)
  }

  /// fresh 로우 변수로 로우 방정식을 만든다
  fn fresh_row_combination(&mut self) 
      -> RowCombination {
    RowCombination {
      left: Row::Open(self.fresh_row_var()),
      right: Row::Open(self.fresh_row_var()),
      goal: Row::Open(self.fresh_row_var()),
    }
  }
  // ... 이후 내용
}

로우를 위한 새 변수 종류가 생겼으니, 새 단일화 테이블도 생깁니다. 로우 변수는 ClosedRow로 풀립니다. 또 부분 로우 조합(partial row combinations) 집합이 있는데, 이는 단일화 중에 나중에 필요합니다. 아직 풀기에 정보가 부족한 로우 조합들로, 단일화 중 더 많은 로우 정보를 알게 되면 풀게 됩니다.

마지막 새 멤버인 row_to_combo와 branch_to_ret_ty는 타입 추론의 끝에서 사용할 출력을 저장합니다. row_to_combo는 로우 AST의 NodeId를 각 노드에 대해 생성된 로우 조합에 매핑합니다. branch_to_ret_ty는 Branch의 NodeId를 그 노드에 대해 추론된 반환 타입에 매핑합니다. 이후 패스에서 이를 사용할 것이므로 타입 추론 중에 저장해 둡니다.

각 로우 노드는 가능한 로우 조합을 여러 개 가질 수도 있습니다. Project는 입력 로우의 어떤 부분집합 필드도 반환할 수 있죠. 타입 추론을 통해 각 로우 노드에서 어떤 특정 로우 조합이 사용되는지 알아낼 수 있습니다. 하지만 변수와 달리, 나중에 타입을 재구성하는 것만으로는 어떤 로우 조합이 선택되었는지 알 수 없습니다. 그래서 나중 패스에서 타입 추론이 어떤 선택을 했는지 알 수 있도록 로우 조합 자체를 저장합니다.

Infer

행정 처리는 여기까지 하고, 로우에 대한 infer 케이스를 봅시다. 먼저 Label 케이스부터:

Label

Ast::Label(id, label, value) => {
  let (out, value_ty) = 
    self.infer(env, *value);
  (
    out.with_typed_ast(|ast| 
      Ast::label(
        id,
        label.clone(), 
        ast
      )
    ),
    Type::label(
      label, 
      value_ty
    ),
  )
}

Label 케이스는 간단합니다. value의 타입을 추론하고, 추론된 타입을 주어진 label로 감싸 Label 타입을 만듭니다. 쉽죠. 다음은 Unlabel입니다:

Ast::Unlabel(id, value, label) => {
  let value_var = 
    self.fresh_ty_var();
  let expected_ty = 
    Type::label(label, Type::Var(value_var));
  let out = 
    self.check(env, *value, expected_ty);
  (
    out.with_typed_ast(|ast|
      Ast::unlabel(id, ast, label)),
    Type::Var(value_var)
  )
}

Unlabel 케이스가 더 흥미롭습니다. check를 이용해 Unlabel이 주는 추가 정보를 활용할 수 있기 때문이죠. Unlabel의 값은 반드시 Label 타입이어야 하고, 그 타입은 label 필드를 포함해야 합니다. 그래서 fresh 타입 변수를 가진 Label을 만들어 value를 그 타입에 맞춰 검사합니다.

곱 타입(Product)

이제 감이 왔죠. Concat은 새 로우 조합 제약을 사용합니다:

Ast::Concat(id, left, right) => {
  let row_comb = 
    self.fresh_row_combination();

  // Concat은 두 작은 로우를 결합해 큰 로우를 만든다.
  // 이를 확인하기 위해 입력이 left와 right의 작은 로우 타입을 갖는지 검사한다.
  let left_out = 
    self.check(env.clone(), *left, 
      Type::Prod(row_comb.left.clone()));
  let right_out = 
    self.check(env, *right, 
      Type::Prod(row_comb.right.clone()));

  // 그렇다면 출력 타입은 goal 로우로 만든 큰 로우 타입이다
  let out_ty = 
    Type::Prod(row_comb.goal.clone());
  let mut constraints =
    left_out.constraints;
  constraints.extend(right_out.constraints);
  // concat을 풀기 위한 로우 방정식 제약을 추가
  constraints.push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev.insert(id, row_comb);

  let typed_ast = Ast::concat(
    id,
    left_out.typed_ast,
    right_out.typed_ast,
  );

  (
    InferOut {
      constraints,
      typed_ast,
    },
    out_ty,
  )
}

먼저 fresh 로우 조합을 만듭니다. 이 조합의 goal이 추론된 곱 타입이 됩니다. left와 right는 곱 타입이어야 한다는 걸 알고 있으니, 조합의 left/right 로우로 만든 Prod 타입에 맞춰 check 합니다.

이 패턴은 모든 로우 노드들이 대략 공유합니다. 각 노드는 생성한 RowCombination을 저장하죠. Project도 비슷합니다:

Ast::Project(id, dir, goal) => {
  let row_comb = 
    self.fresh_row_combination();

  let sub_row = match dir {
    Direction::Left => 
      row_comb.left.clone(),
    Direction::Right => 
      row_comb.right.clone(),
  };

  // goal 로우에 대해 검사한다
  let mut out = 
    self.check(env, *goal, Type::Prod(row_comb.goal.clone()));

  out
    .constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev.insert(id, row_comb);
  (
    out.with_typed_ast(|ast| 
      Ast::project(id, dir, ast)),
    // sub_row가 projection의 출력 타입
    Type::Prod(sub_row),
  )
}

눈에 띄는 차이 하나: 이번에는 로우 조합의 goal이 입력 타입입니다. 출력 타입은 방향에 따라 left 또는 right 입니다. Direction은 오직 left/right 중 어느 쪽을 쓸지 토글하기 위해 존재합니다. 지금의 로우 사용에서는 큰 의미가 없으니 넘어가겠습니다(언제나 그렇듯 자세한 건 논문에 있습니다).

합 타입(sum types)을 추론하는 방식은 곱 타입과 매우 비슷합니다(대칭성의 마법). 지면 관계상 생략하지만 관심 있다면 보세요:

Sums

들러줘서 고마워요!

Ast::Branch(id, left, right) => {
  let row_comb = 
    self.fresh_row_combination();
  let ret_ty = 
    self.fresh_ty_var();

  // Branch는 두 입력이 핸들러 함수여야 한다.
  // 타입: <sum> -> a
  // 따라서 left와 right가 동일한 반환 타입을 갖는 핸들러 함수 타입인지 검사한다
  let left_out = self.check(
    env.clone(),
    *left,
    Type::fun(Type::Sum(row_comb.left.clone()), Type::Var(ret_ty)),
  );
  let right_out = self.check(
    env,
    *right,
    Type::fun(Type::Sum(row_comb.right.clone()), Type::Var(ret_ty)),
  );

  // 그렇다면 Branch 노드 전체 타입은 goal 로우의 sum 타입에서 ret_ty로 가는 함수
  let out_ty = Type::fun(Type::Sum(row_comb.goal.clone()), Type::Var(ret_ty));
  // 최종 출력에 필요한 제약들을 모은다
  let mut constraints = left_out.constraints;
  constraints
    .extend(right_out.constraints);
  constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev
      .insert(id, row_comb);
  self.branch_to_ret_ty
      .insert(id, Type::Var(ret_ty));

  (
    InferOut {
      constraints,
      typed_ast: Ast::branch(
        id,
        left_out.typed_ast, 
        right_out.typed_ast
      ),
    },
    out_ty,
  )
}

이는 Concat과 거의 완전히 같습니다. 다만 branch는 left와 right가 함수여야 합니다. 반환 타입들이 일치하도록 더 많은 부기 작업을 해야 하죠.

Ast::Inject(id, dir, value) => {
  let row_comb = 
    self.fresh_row_combination();

  let sub_row = match dir {
    Direction::Left => 
      row_comb.left.clone(),
    Direction::Right => 
      row_comb.right.clone(),
  };

  let out_ty = 
    Type::Sum(row_comb.goal.clone());

  let mut out = 
    self.check(env, *value, Type::Sum(sub_row));
  out
    .constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev.insert(id, row_comb);
  (
    out.with_typed_ast(|ast| 
      Ast::inject(id, dir, ast)),
    // goal 로우가 출력 타입
    out_ty,
  )
}

이는 Project와 거의 같습니다. 큰 차이는 Inject가 작은 로우를 큰 로우로 매핑한다는 점입니다. 그래서 goal이 입력 타입이 아니라 출력 타입으로 쓰입니다. Direction은 입력 로우가 left인지 right인지 결정합니다(Project의 direction과 반대).

각 로우 케이스는 fresh 로우 조합을 만들고, 이를 이용해 로우 항들의 타입을 추론합니다. 곧 보겠지만 check도 같은 방식으로 로우 타입을 검사합니다.

Check

한 번 해본 적 있죠. 이제 전문가입니다. infer 다음에는 새 타입들에 대해 check를 합니다. check는 노드가 어떤 타입에 대해 검사되는지 결정하기 위해 더 많은 일을 해야 합니다. 하지만 그 전에, 레이블부터 검사해야 합니다.

Label

( Ast::Label(id, ast_lbl, val)
, Type::Label(ty_lbl, ty)) 
    if ast_lbl == ty_lbl => {
  self.check(env, *val, *ty)
    .with_typed_ast(|term| Ast::label(id, ast_lbl, term))
}

Int나 Fun 케이스처럼 Label 노드는 Label 타입에 대해 체크됩니다. 하지만 그들과 달리, Label 노드는 두 label이 같을 때만 Label 타입에 대해 체크됩니다. 더 놀랍게도 Concat과 Project도 Label 타입에 대해 체크됩니다:

(ast @ Ast::Concat(_, _), Type::Label(lbl, ty))
| (ast @ Ast::Project(_, _), Type::Label(lbl, ty)) => {
  // 싱글턴 로우를 곱 타입으로 캐스팅
  self.check(env, ast, 
    Type::Prod(Row::single(lbl, *ty)))
}

예상대로 Branch와 Inject도 Label 타입에 대해 체크됩니다:

(ast @ Ast::Branch(_, _), Type::Label(lbl, ty))
| (ast @ Ast::Inject(_, _), Type::Label(lbl, ty)) => {
  // 싱글턴 로우를 합 타입으로 캐스팅
  self.check(env, ast, 
    Type::Sum(Row::single(lbl, *ty)))
}

Label 타입은 꽤 수용적입니다. Label 타입은 싱글턴 로우처럼 동작하고, 로우는 타입이 아니므로, 곱/합 타입 사이의 중간자 역할을 합니다. 곱이나 합은 레이블을 로우로 변환해 감쌀 수 있지만, 곱으로 갈지 합으로 갈지 결정되기 전까지는 알 수 없습니다. 그래서 체크 로직에서 가능한 모든 경우를 고려해야 합니다.

다음은 훨씬 간결한 Unlabel 케이스입니다:

(Ast::Unlabel(id, term, lbl), ty) => {
  self.check(env, *term, 
    Type::label(lbl.clone(), ty))
      .with_typed_ast(|term| Ast::unlabel(id, term, lbl))
}

Unlabel은 어떤 타입에 대해서도 체크될 수 있습니다. Label 타입을 구성해 val을 그에 대해 검사하면 되니까요. 다행히 Label에 비해 케이스 수가 훨씬 적습니다.

이제 곱 타입 노드들을 체크해 봅시다.

곱 타입(Product)

앞서 Concat을 Label 타입에 대해 체크하는 건 미리 처리했습니다. 본론은 Product 타입에 대해 체크하는 것입니다:

(Ast::Concat(id, left, right), Type::Prod(goal_row)) => {
  let left_row = 
    Row::Open(self.fresh_row_var());
  let right_row = 
    Row::Open(self.fresh_row_var());

  let left_out = 
    self.check(env.clone(), *left, 
      Type::Prod(left_row.clone()));
  let right_out = 
    self.check(env, *right, 
      Type::Prod(right_row.clone()));

  // 하위 제약을 합친다
  let mut constraints = left_out.constraints;
  constraints.extend(right_out.constraints);
  // goal 로우를 위한 로우 조합을 추가
  let row_comb = RowCombination {
    left: left_row,
    right: right_row,
    goal: goal_row.clone(),
  };

  constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev
      .insert(id, row_comb);

  let typed_ast = Ast::concat(
    id,
    left_out.typed_ast,
    right_out.typed_ast,
  );

  InferOut {
    constraints,
    typed_ast,
  }
}

Concat의 infer 케이스와 달리, check 케이스에는 이미 goal 로우가 있습니다. 기대 타입(expected type)이 방정식의 goal 로우로 작동하죠. 우리는 방정식의 left와 right가 될 로우만 새로 만들면 됩니다.

infer와 마찬가지로 left와 right는 Prod 타입이어야 한다는 걸 알고 있습니다. fresh 로우 변수로 Prod 타입을 만들고 check 합니다. 마지막으로 하위 제약들을 합치고 로우 조합을 제약으로 추가하면 끝입니다.

다음은 Project입니다:

(Ast::Project(id, dir, goal), Type::Prod(sub_row)) => {
  let goal_row = Row::Open(self.fresh_row_var());

  let (left, right) = match dir {
    Direction::Left => (sub_row, Row::Open(self.fresh_row_var())),
    Direction::Right => (Row::Open(self.fresh_row_var()), sub_row),
  };

  let mut out = self.check(env, *goal, Type::Prod(goal_row.clone()));
  let row_comb = RowCombination {
    left,
    right,
    goal: goal_row,
  };
  out.constraints
     .push(Constraint::RowCombine(row_comb.clone()));

  self.row_to_ev.insert(id, row_comb);
  out.with_typed_ast(|ast| 
    Ast::project(id, dir, ast))
}

Concat처럼 Project도 기대 타입을 사용해 새 로우 조합을 구성합니다. 하지만 Project는 기대 타입을 goal 로우가 아니라 방향에 따라 left 또는 right로 사용합니다. 따라서 항은 조합의 goal에 대해 검사됩니다.

합 타입은 또 생략합니다. 재미있는 점은 함수 타입에 대해 체크한다는 것뿐이고, 나머지는 곱 타입과 매우 비슷합니다.

Sums

아, 안녕하세요! 방금 Branch 노드를 Fun 타입에 대해 체크하고 있었어요:

(Ast::Branch(id, left_ast, right_ast), Type::Fun(arg_ty, ret_ty)) => {
  let mut constraints = vec![];
  let goal = match arg_ty.deref() {
    Type::Sum(goal) => goal.clone(),
    _ => {
      let goal = self.fresh_row_var();
      constraints.push(Constraint::TypeEqual(*arg_ty, Type::Sum(Row::Open(goal))));
      Row::Open(goal)
    }
  };
  let left = Row::Open(self.fresh_row_var());
  let right = Row::Open(self.fresh_row_var());

  let left_out = self.check(
    env.clone(),
    *left_ast,
    Type::fun(Type::Sum(left.clone()), ret_ty.deref().clone()),
  );
  let right_out = self.check(
    env,
    *right_ast,
    Type::fun(Type::Sum(right.clone()), *ret_ty),
  );

  constraints.extend(left_out.constraints);
  constraints.extend(right_out.constraints);
  let row_comb = RowCombination { left, right, goal };
  constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev.insert(id, row_comb);
  self.branch_to_ret_ty.insert(id, *ret_ty);

  InferOut {
    constraints,
    typed_ast: Ast::branch(
      id,
      left_out.typed_ast, 
      right_out.typed_ast
    ),
  }
}

가능하다면 기대 타입을 Fun(Sum(arg), ret)에 대해 패턴 매칭하고 싶겠지만, Rust는 Box를 뚫고 패턴 매칭하는 걸 아직 허용하지 않습니다(여기). 그래서 먼저 check의 시작에서 arg_ty가 Sum이 되도록 제약을 걸고 그 로우를 뽑아냅니다.

그 다음부터는 Concat을 체크하는 것과 매우 비슷합니다. Concat과 달리 left와 right는 ret_ty를 반환하는 함수 타입에 대해 검사합니다. 이 차이를 제외하면 하위 노드를 체크하고, 하위 제약들을 합치고, 새 조합을 추가하면 끝입니다. 다음은 Inject:

(Ast::Inject(id, dir, value), Type::Sum(goal)) => {
  let sub_row = self.fresh_row_var();
  let mut out = self.check(env, *value, Type::Sum(Row::Open(sub_row)));
  let (left, right) = match dir {
    Direction::Left => (sub_row, self.fresh_row_var()),
    Direction::Right => (self.fresh_row_var(), sub_row),
  };
  let row_comb = RowCombination {
    left: Row::Open(left),
    right: Row::Open(right),
    goal,
  };
  out.constraints
    .push(Constraint::RowCombine(row_comb.clone()));
  self.row_to_ev.insert(id, row_comb);
  out.with_typed_ast(|ast| 
    Ast::inject(id, dir, ast))
}

이전 check 케이스들의 맥락을 알면 Inject는 가장 단순한 케이스입니다. 항을 fresh 로우 변수에 대해 체크하고, dir에 따라 그 로우 변수를 로우 조합의 left 또는 right로 씁니다. 마지막으로 로우 조합을 제약에 추가하면 끝입니다.

로우 단일화(Row Unification)

단일화에서 필요한 수정은 새 RowCombination 제약을 처리하는 것뿐입니다. 제약은 하나뿐이지만, 실제로는 단일화에 꽤 큰 변화가 필요합니다. 이유는 제약의 동치성이 바뀌었기 때문입니다. 로우를 추가하기 전에는 항을 문법적으로 비교해 같은 항끼리 단일화하면 됐습니다. 같지 않다면 단일화가 존재하지 않는다고 확신할 수 있었죠. 하지만 이제는 아닙니다. 다음 두 로우 제약을 보세요:

(x: Int) + (f: Bool, y: Int) = (f: Bool, x: Int, y: Int)
(f: Bool, y: Int) + (x: Int) = (f: Bool, x: Int, y: Int)

문법적으로는 다르지만 여전히 같은 방정식입니다. 로우 조합은 교환법칙(commutative)이 있으므로 이 둘이 같은 방정식임을 알아봐야 합니다. 단순한 예에서는 쉽지만, 변수가 섞이면 더 까다로워집니다:

a0 + b = c
b + a1 = c

눈을 가늘게 뜨고 보면 여기서 a0 = a1을 배울 정보가 충분합니다. 언제 타입 변수를 같게 둘 수 있고, 언제 두 조합이 단일화될 수 없는지 어떻게 알까요?

마지막으로, 우리의 방정식은 보통 구체적인 형태로 풀려 처리할 수 있게 되지만, 항상 그렇진 않습니다. 타입 변수처럼 어떤 조합은 단일화 끝에도 미해결 상태로 남을 수 있습니다. 이는 타입 변수와 마찬가지로, 조합을 일반화(generalize)해 최종 타입에 추가함으로써 해결합니다.

이 문제들을 안고 최상위 unification 함수로 돌아가 봅시다:

fn unification(
  &mut self,
  constraints: Vec<Constraint>,
) -> Result<(), TypeError> {
  for constr in constraints {
    match constr {
      // 다른 제약들
      Constraint::RowConcat(row_comb) => 
        self.unify_row_comb(row_comb)
            .map_err(|kind| TypeError { kind, node_id })?,
    }
  }
  Ok(())
}

새 제약에 대한 케이스가 추가되었고, 곧바로 unify_row_comb를 호출합니다:

fn unify_row_comb(&mut self, row_comb: RowCombination) -> Result<(), TypeErrorKind> {
  let left = self.normalize_row(row_comb.left);
  let right = self.normalize_row(row_comb.right);
  let goal = self.normalize_row(row_comb.goal);
  match (left, right, goal) {
    // ...
  }
}

즉시 많은 평행 구조가 보입니다:

• unify_row_comb의 구조는 unify_ty_ty와 같다
• normalize_row는 로우에 대한 normalize_ty다
• (나도 알아요, couple은 두운에 안 맞았어요)

unify_ty_ty처럼 패턴 매칭으로 진행하는 게 자연스럽습니다. 매칭 케이스들은 로우 변수 개수로 분류할 수 있습니다:

• 변수 0개 – left/right를 결합하고 그 결과를 goal과 단일화
• 변수 1개 – 알려진 두 로우로부터 변수 하나를 푼다
• 변수 2개 이상 – 이 방정식을 풀기엔 정보가 부족하다

이제 변수 0개 케이스(들)를 봅시다:

(Row::Closed(left), Row::Closed(right), goal) => {
  let calc_goal = ClosedRow::merge(left, right);
  self.unify_row_row(Row::Closed(calc_goal), goal)
}

이 첫 케이스는 사실 두 케이스를 커버합니다:

• goal이 닫힌 경우: 변수 0개
• goal이 열린 경우: 변수 1개

세기 놀이 재밌죠? 훌륭한 추상화 덕분에 둘을 같은 방식으로 처리합니다. left와 right를 결합해 새 로우를 만들고, 그 로우를 goal과 단일화합니다. ClosedRow::merge는 닫힌 로우들을 병합하는 헬퍼입니다. 두 로우의 필드를 붙이고 정렬하되, 필드->타입 매핑을 유지합니다.

로우 단일화를 많이 하게 될 테니, 이를 위한 헬퍼 unify_row_row를 도입합시다:

fn unify_row_row(&mut self, left: Row, right: Row) -> Result<(), TypeErrorKind> {
  let left = self.normalize_row(left);
  let right = self.normalize_row(right);
  match (left, right) {
    (Row::Open(left), Row::Open(right)) => todo!(),
    (Row::Open(var), Row::Closed(row)) 
    | (Row::Closed(row), Row::Open(var)) => todo!(),
    (Row::Closed(left), Row::Closed(right)) => todo!(),
  }
}

로우는 열리거나 닫힙니다. 로우가 두 개 있으니 가능성은 4개입니다. 하지만 두 경우는 같은 방식으로 처리되므로 3개 케이스만 고려하면 됩니다:

(Row::Open(left), Row::Open(right)) => 
  self
    .row_unification_table
    .unify_var_var(left, right)
    .map_err(TypeError::RowsNotEqual),

로우 변수끼리 만나면 Union-Find에서 둘을 합칩니다. 타입 변수에서 하던 것과 똑같죠.

다음은 ‘1+1=2’ 같은 BOGO 케이스: 로우 변수와 닫힌 로우:

(Row::Open(var), Row::Closed(row)) 
| (Row::Closed(row), Row::Open(var)) => {
  self.row_unification_table
      .unify_var_value(var, Some(row.clone()))
      .map_err(TypeError::RowsNotEqual)?;
  self.dispatch_any_solved(var, row)
}

로우 변수와 닫힌 로우가 만나면 변수를 그 로우로 풉니다. Union-Find에서 변수를 닫힌 로우 값으로 단일화하는 것으로 풉니다(타입에서도 비슷했죠). 그 다음 dispatch_any_solved라는 다른 헬퍼를 호출합니다. 자세한 내용은 나중에 다루겠지만, 로우 변수를 푸는 것이 어떤 부분 로우 방정식을 해결하는지 확인하는 역할입니다.

마지막 케이스는 닫힌 로우 두 개입니다:

(Row::Closed(left), Row::Closed(right)) => {
  // 단일화 가능한지 실제로 확인
  if left.fields != right.fields {
    return Err(TypeError::RowsNotEqual((left, right)));
  }

  // 가능하다면 values는 이미 정렬되어 있으므로 각각을 순회하며 타입을 단일화
  let left_tys = left.values.into_iter();
  let right_tys = right.values.into_iter();
  for (left_ty, right_ty) in left_tys.zip(right_tys) {
    self.unify_ty_ty(left_ty, right_ty)?;
  }
  Ok(())
}

닫힌 로우 두 개가 만나면(함수 타입끼리 만났을 때처럼) 분해할 수 있습니다. 먼저 필드가 같은지 확인합니다. 다르면 단일화할 방법이 없으니 즉시 오류를 냅니다. 필드가 같다면 타입 벡터를 zip하여 각 쌍을 단일화합니다.

이제 로우를 단일화하는 방법을 알았으니, 로우 조합 단일화로 돌아가 변수 1개 케이스를 봅시다:

(Row::Open(var), Row::Closed(sub), Row::Closed(goal))
| (Row::Closed(sub), Row::Open(var), Row::Closed(goal)) => {
  let diff_row = self.diff_and_unify(goal, sub)?;
  self.unify_row_row(Row::Open(var), Row::Closed(diff_row))
}

변수가 어디에 있든 같은 방식으로 처리합니다. goal 로우와 sub 로우로부터 변수를 풀기에 충분합니다. goal에서 sub를 뺀 차집합 로우를 만들고, 그것을 변수와 단일화합니다. 차집합 계산은 diff_and_unify가 합니다.

중요한 디테일: diff_and_unify의 ‘and’ 뒤에 있습니다. goal과 sub의 차를 계산하는 동안, goal과 sub 자체도 서로 단일화해야 합니다. 저는 아직 겪어본 적은 없지만, 이걸 잊으면 타입 체커가 조용히 틀린 결과를 내서 며칠 동안 머리를 긁게 된다고 하더군요. 다행히 우리는 이 글을 읽었으니 그 수치스러운 시간 낭비를 피했습니다.

마지막 케이스는 변수 2개 이상입니다:

(left, right, goal) => {
  let new_comb = RowCombination { left, right, goal };
  // 이미 본 조합 중 단일화 가능한 것이 있는지 확인
  let poss_uni = self.partial_row_combs.iter().find_map(|comb| {
    if comb.is_unifiable(&new_comb) {
      Some(comb.clone())
    // 교환된(computed) 조합도 확인
    } else if comb.is_comm_unifiable(&new_comb) {
      // 나중에 올바른 로우를 단일화하도록 조합을 commute
      Some(RowCombination {
        left: comb.right.clone(),
        right: comb.left.clone(),
        goal: comb.goal.clone(),
      })
    } else {
      None
    }
  });

  match poss_uni {
    // 매치가 있으면 단일화
    Some(match_comb) => {
      self.unify_row_row(new_comb.left, match_comb.left)?;
      self.unify_row_row(new_comb.right, match_comb.right)?;
      self.unify_row_row(new_comb.goal, match_comb.goal)?;
    }
    // 없으면 부분 조합 집합에 추가
    None => {
      self.partial_row_combs.insert(new_comb);
    }
  }
  Ok(())
}

변수 2개 이상인 케이스는 우리가 아는 게 가장 적습니다. 앞의 두 케이스처럼 풀 수 없죠. 대신 부분 조합 집합에 추가해, 나중에 충분한 정보를 얻을 때까지 보류해야 합니다.

하지만 그냥 넣고 넘어갈 수는 없습니다. 그러면 앞서 diff_and_unify에서 놓칠 뻔했던 것과 같은 학습 기회를 놓치게 됩니다. 먼저 기존 조합들을 확인해 새 로우 조합이 그들과 단일화 가능한지 봅니다. 로우 조합을 풀 수 없다고 해서, 거기서 아무것도 배울 수 없다는 뜻은 아닙니다.

조합을 추가하기 전에, 기존 조합 중 새 조합과 단일화 가능한 것이 있는지 찾습니다. 그러려면 조합이 언제 단일화 가능한지 알아야 합니다. 두 로우 조합은 구성 요소 중 두 개가 단일화 가능하면 단일화 가능합니다. 예를 들어:

b + c = (x : Int, y : e)
b + d = (x : Int, y : Int)

이 둘은 단일화 가능합니다. b는 같은 로우 변수이므로 자기 자신과 단일화되고, (x : Int, y : e)는 (x : Int, y : Int)와 필드가 같고 각 필드의 타입이 단일화 가능하므로 단일화됩니다. 이 검사는 is_unifiable과 is_comm_unifiable 헬퍼가 수행합니다. 로우 조합은 교환되므로 두 순서를 모두 확인해야 합니다.

단일화 가능한 조합을 찾았다면, 새 조합을 집합에 추가할 필요가 없습니다. 그 조합과 단일화하는 것만으로 충분합니다. 단일화 가능한 조합을 찾지 못할 때에만 새 조합을 집합에 넣어야 합니다. 이렇게 하면 각 조합에서 로우 변수에 대해 최대한 많은 것을 배우고, 부분 조합 집합도 최소로 유지할 수 있습니다.

이제 로우 조합을 성공적으로 풀고 있습니다. 마지막으로 앞에서 스쳐 지나간 디테일 하나만 다루면 됩니다. 로우 변수가 닫힌 로우와 단일화될 때 dispatch_any_solved를 호출했죠. 이는 무엇을 할까요?

fn dispatch_any_solved(&mut self, var: RowVar, row: ClosedRow) -> Result<(), TypeErrorKind> {
  let mut changed_combs = vec![];
  self.partial_row_combs = std::mem::take(&mut self.partial_row_combs)
    .into_iter()
    .filter_map(/* 변수를 찾는다 */)
    .collect();

  for row_comb in changed_combs {
    self.unify_row_comb(row_comb)?;
  }
  Ok(())
}

dispatch_any_solved는 모든 부분 방정식을 순회하면서 해당 변수를 포함하는지 찾습니다. 포함한다면 부분 집합에서 제거하고, 그 변수를 해(solution)로 치환한 뒤 changed_combs에 추가합니다. 그 작업은 filter_map에 전달된 콜백에서 이뤄집니다:

|comb| match comb {
  RowCombination { left, right, goal }
    if left == Row::Open(var) => {
    changed_combs.push(RowCombination {
      left: Row::Closed(row.clone()),
      right,
      goal,
    });
    None
  }
  RowCombination { left, right, goal }
    if right == Row::Open(var) => {
    changed_combs.push(RowCombination {
      left,
      right: Row::Closed(row.clone()),
      goal,
    });
    None
  }
  RowCombination { left, right, goal }
    if goal == Row::Open(var) => {
    changed_combs.push(RowCombination {
      left,
      right,
      goal: Row::Closed(row.clone()),
    });
    None
  }
  comb => Some(comb),
}

바뀐 방정식들을 모두 모은 뒤 unify_row_comb로 다시 단일화합니다. 이렇게 해서 단일화가 끝납니다.

이 과정은 unify_ty_ty보다 훨씬 많은 기계장치가 필요했습니다. 로우가 더 이상 문법적으로만 같지 않다는 사실이 생각보다 큰 파급을 가져왔죠. 더 이론적인 설명을 원한다면, 우리는 문법적 단일화(syntactic unification)의 세계를 떠나 E-단일화(E-unification)의 영역에 들어섰습니다. 물론 우리는 E-단일화의 바다에 발끝만 담근 수준이지만요.

E-단일화는 등식적 단일화(equational unification)입니다. 항을 순수하게 문법적으로만 비교하는 대신, 등식들의 집합을 가지고 비교합니다. 우리에게 그 집합은 하나뿐입니다: 교환법칙(x + y = y + x). 하지만 일반적으로는 임의 개수의 등식을 포함할 수 있습니다.

어떤 집합을 선택하든 공통점이 하나 있습니다. 등식 집합을 허용하는 순간, 문법적 단일화가 제공하던 거의 선형에 가까운 실행 시간을 잃게 됩니다.

우리도 마찬가지입니다(최대한 숨기려 했지만요). 로우 조합을 단일화할 때 부분 로우 조합들을 순회합니다. 더 나쁜 건 dispatch_any_solved의 연쇄 호출로 인해 순회가 폭포처럼 이어질 수도 있다는 점입니다. 실제로는 어떤 항목에 대해 부분 조합 집합이 작을 거라 기대하지만, 우리가 하는 트레이드오프를 인식하는 게 중요합니다.

노 젓기를 마무리하며

터널 끝의 빛이 보이나요? 로우 타입이라는 해변에 닿기까지 딱 하나만 남았습니다: 미해결 로우 조합. 정말 거의 다 왔습니다. 모래 맛이 느껴질 정도예요.

타입 변수처럼, 로우 조합도 때때로 미해결로 남습니다. 너무나도 비슷해서 처리 방식도 같습니다. 미해결 타입 변수는 타입 스킴(type scheme)의 일부로 최종 타입에 추가되었죠. 미해결 로우 조합도 같은 방식으로 타입 스킴에 추가할 겁니다. 단, 한 가지 조건이 있습니다. 타입에 실제로 사용되는 로우 변수에 대한 조합만 타입 스킴에 추가합니다. Project와 Inject는 사용되지 않는 로우 변수를 포함하는 로우 조합을 만들기도 하는데, 그런 것들은 미해결이더라도 최종 타입에 나타나면 안 됩니다.

아주 편리하게도, 미해결 문제를 다른 누군가에게 떠넘길 수 있네요. 마지막 한 번의 노 젓기로 우리는 마침내 해안에 도착했습니다. 우리 언어는 데이터 타입을 지원하며, 로우 타입 덕분에 꽤 유연한 데이터 타입을 갖게 됐습니다.

시간 관계상 몇몇 코드는 건너뛰었지만, 모든 피비린내 나는 디테일을 보고 싶다면 전체 구현에서 확인할 수 있습니다.

다음 편에서는 두 가지 선택지가 있습니다: 최상위 함수의 타입체크를 하거나, 혹은 로우 내리기(lower rows)를 할 수도 있습니다.