6장: 힌들리–밀너 추론

새 파일

• src/algorithm_w.rs
• src/union_find.rs

변경된 파일

• src/types.rs
• src/ast.rs
• src/cbn.rs
• src/cek.rs
• src/eval.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/names.rs
• src/normal.rs

동기

\x -> x를 봅시다. 우리는 x가 어떤 타입인지 말하지 않았지만, 이미 유용한 사실을 하나 알고 있습니다. 무엇이 들어가든 정확히 그것이 그대로 다시 나옵니다. 따라서 이 함수의 타입은 a -> a 꼴이어야 합니다.

꽤 멋지지 않습니까! 우리는 함수를 한 번도 실행하지 않고 가능한 모든 호출에 대해 무언가를 알아냈습니다. 정수든, 불리언이든, 또 다른 함수든 모두 동작합니다. 타입 스킴(type scheme)은 각 사용처가 저마다의 a를 고를 수 있게 해 줍니다. 힌들리–밀너 추론은 프로그램이 허용하는 가장 일반적인 스킴을 찾아냅니다 (Damas and Milner 1982).

우리는 이것을 두 가지 방식으로 구현할 것입니다. 알고리즘 W는 자신이 발견한 타입 치환을 명시적으로 기록해 둡니다 (Damas and Milner 1982). 두 번째 구현은 가변 셀을 갱신하고, 레벨을 사용해 어떤 변수를 일반화할 수 있는지 추적합니다. 두 구현은 같은 방정식을 풀지만, 구현상의 선택은 서로 다릅니다. 두 가지를 모두 직접 따라가 보면, Fun에 가져갈 버전을 고르기 전에 알고리즘을 이해하는 데 도움이 될 것입니다.

현재의 언어

Poly에는 주석 없는 람다, 적용, 다형적 let, 함수 전용 let rec, 정수, 불리언, 조건식, 산술이 있습니다. 비교용 연습 문제를 위해 평가 장에서 다룬 명시적 fix 형식은 여전히 사용할 수 있습니다.

let id = \x -> x in
let first = id 1 in
id True

id가 두 번 나타날 때 각각은 그 스킴을 독립적으로 인스턴스화합니다. 람다 매개변수는 다르게 동작합니다. \f -> let first = f 1 in f True는 거부되는데, 그 람다 본문 전체에서 f가 하나의 타입만 가지기 때문입니다.

우리는 이전 장의 매개변수 표기를 생략할 수 있습니다. 특히 항등 함수는 더 이상 정수를 받을지 불리언을 받을지 선택하지 않아도 됩니다. 우리는 이미 이해하고 있는 평가 장치는 그대로 두고, 컴파일러가 그 자유를 어떻게 알아내는지에 집중하겠습니다.

이론

타입 규칙 읽는 법

타입 규칙으로 가득한 페이지는 처음 볼 때 위압적으로 보일 수 있습니다. 이 표기법은 대체로 같은 문장을 되풀이하지 않게 해 주려고 있는 것입니다. 각 규칙은 구문의 한 조각을 설명합니다. 먼저 가로줄 아래를 보고 우리가 무엇을 확립하려는지 확인한 다음, 줄 위를 보고 각 부분에 대해 무엇을 알아야 하는지 확인하십시오. Pierce는 타입 시스템을 다루는 책 전반에서 이 방식을 사용합니다 (Pierce 2002).

$$\Gamma ⊢e:\tau$$

이것은 “감마에 있는 가정 아래에서 식 e는 타입 tau를 가진다”라고 읽습니다. 이 기호들 덕분에 반복되는 문장을 짧게 쓸 수 있습니다:

콜론은 타입을 단언합니다. 식을 평가하지는 않습니다. Gamma에는 런타임 값이 아니라 정적인 가정이 들어 있습니다. 이 장에서 Gamma는 let으로 묶인 이름을 스킴에, 람다 매개변수를 단형 타입에 대응시키며, 단형 타입은 양화자가 없는 스킴으로 표현됩니다. 규칙에 나오는 그리스 문자 변수는 수학적 자리 표시자입니다. 추론기의 가변 메타변수는 어떤 타입이 규칙을 만족하는지 찾아내기 위한 구현 기법입니다.

가로 막대는 “위에 있는 것이 모두 성립하면 아래의 명제도 성립한다”는 뜻입니다. 나눗셈이 아닙니다. 윗부분이 비어 있는 규칙에는 전제가 없습니다. 정수 리터럴은 하위 식을 살펴보지 않고도 Int 타입을 가집니다.

$$\frac{}{\Gamma ⊢42:\mathsf{Int}}\text{(Int)}$$

적용의 경우, 두 사실이 같은 입력 타입에 대해 일치해야 합니다:

$$\frac{\Gamma ⊢e_1:\alpha \to \beta \Gamma ⊢e_2:\alpha }{\Gamma ⊢e_1{e}_2:\beta }\text{(App)}$$

e1이 정수를 받아 불리언을 반환한다면, e2는 정수여야 하고 호출은 불리언을 반환합니다. 반복되는 $\alpha$가 그 일치를 표현합니다. 추론 과정에서 우리는 이를 단일화로 알아냅니다. 규칙은 유효한 관계를 기술합니다. 전제를 어떤 순서로 풀어야 하는지 정해 주지는 않습니다.

작은 유도 만들기

\x -> x + 1을 생각해 봅시다. x에 임시 타입을 부여하십시오. 덧셈 규칙은 두 피연산자가 모두 정수일 것을 요구하므로, 그 임시 타입은 Int로 정해집니다. $\Delta =\Gamma ,x:\mathsf{Int}$로 쓰면 결과 트리를 간결하게 유지할 수 있습니다:

$$\frac{\frac{x:\mathsf{Int}\in \Delta }{\Delta ⊢x:\mathsf{Int}}\text{(Var)}\frac{}{\Delta ⊢1:\mathsf{Int}}\text{(Int)}}{\Delta ⊢x+1:\mathsf{Int}}\text{(Add)}$$

두 잎은 조회와 리터럴 규칙으로 Add를 정당화합니다. 그런 다음 람다 규칙이 매개변수에 관한 가정을 함수 타입 안으로 옮깁니다:

$$\frac{\Gamma ,x:\alpha ⊢e:\beta }{\Gamma ⊢\lambda x.e:\alpha \to \beta }\text{(Lam)}$$

여기서 $\lambda x.e$는 \x -> e를 뜻합니다. Lam은 우리의 함수 타입 Int -> Int를 부여하고, 본문이 x에 대해 가졌던 지역 가정을 제거합니다. 1을 True로 바꾸면 Add의 전제가 깨지므로, 유도를 완성할 수 없습니다.

단형 타입에서 스킴으로

let id = \x -> x in ...에서 흥미로운 점은 id를 사용하는 곳마다 각자 자기 인자 타입을 고를 수 있다는 것입니다. 우리는 이 허용을 스킴(scheme)에 기록합니다. 단형 타입(monotype)은 하나의 타입을 기술하며, 아직 풀지 않은 변수를 포함할 수도 있습니다. 스킴은 호출하는 쪽이 어떤 변수를 새로 고를 수 있는지 표시합니다. 그렇게 새 사본을 만드는 일이 인스턴스화(instantiation)입니다. 어떤 변수를 호출하는 쪽에 안전하게 내줄 수 있는지 정하는 일이 일반화(generalization)입니다 (Damas and Milner 1982).

둘러싼 스코프가 아직 의존하고 있는 변수는 일반화할 수 없습니다. 그렇지 않으면 지역 함수가 어떤 타입이든 받는 척하면서, 타입이 이미 고정된 바깥 값을 몰래 사용할 수 있게 됩니다. 따라서 람다 매개변수는 모든 사용처가 공유하는 단형 타입 하나로 시작합니다.

$$\frac{\Gamma ⊢e_1:\tau \sigma =\mathsf{gen}(\Gamma ,\tau )\Gamma ,x:\sigma ⊢e_2:\beta }{\Gamma ⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:\beta }\text{(Let)}$$

Let 규칙은 세 단계로 읽으십시오. 먼저 바인딩의 우변을 추론하고, 그 타입을 일반화합니다. 마지막으로 그 스킴을 스코프에 둔 채 본문을 검사합니다. $\sigma$에 대한 등식은 평가할 또 하나의 프로그램이 아니라, 그 스킴을 정의하는 부수 조건입니다. 타입이나 환경 안의 변수가 스킴의 양화사에 묶여 있지 않으면 그 변수는 자유(free) 변수입니다. 환경의 자유 변수에 들어 있지 않은 변수만 일반화할 수 있습니다.

let id = \x -> x in ...에서 우변의 타입은 $\alpha \to \alpha$입니다. $\alpha$가 둘러싼 환경과 무관하다면, 우리는 id를 $\forall \alpha .\alpha \to \alpha$에 바인딩합니다. 이름을 조회할 때마다 이 스킴을 새로 인스턴스화합니다. id 1은 Int를 고릅니다. id True는 Bool을 고릅니다. 반면 \f -> ...의 매개변수 f는 Lam 규칙에서 단형 타입 하나를 받습니다. 그 모든 사용처가 같은 타입을 만족해야 합니다. 양화는 let 규칙의 몫이지, 우연히 함수를 가리키는 모든 이름의 몫이 아닙니다.

단일화는 타입 사이의 동등성 제약을 풉니다. 두 화살표 타입은 정의역을 단일화하고, 거기서 알아낸 것을 적용한 다음, 공역을 단일화하는 방식으로 단일화됩니다. 변수는 어떤 타입 안에 나타나지 않을 때에만 그 타입으로 풀 수 있습니다. 이 발생 검사가 없으면 자기 적용에는 무한 타입이 필요해집니다. 이 오류는 E0202로 보고됩니다. 호환되지 않는 기본 타입은 E0201을 냅니다.

재귀 함수는 본문을 검사하는 동안 하나의 임시 단형 타입을 가집니다. 그 검사가 끝난 뒤에야 바깥의 let이 그것을 일반화할 수 있습니다. 우리가 fix로 낮추는 방식은 평범한 단형 자기 매개변수를 통해 이 규칙을 표현합니다. 여기에는 다형 재귀(polymorphic recursion)가 없습니다. 환경 기반 일반화 규칙과 그 효율적인 레벨 기반 형태는 인용한 문헌에서 전개됩니다 [Kiselyov (2013); Rémy (1992)].

Poly에는 가변 상태가 없으므로, let의 우변은 일반화되기 위해 구문적 값일 필요가 없습니다. 예를 들어, 항등 함수를 다른 항등 함수에 적용해도 여전히 다형적 바인딩이 만들어집니다. 이 제한 없는 규칙은 Fun에도 적용될 것입니다.

작은 보상

합성은 짧은 정의가 얼마나 많은 것을 말할 수 있는지 보여 주는 멋진 예입니다.

let compose = \f -> \g -> \x -> f (g x) in
compose (\x -> x + 1) (\x -> x * 2) 20

결과는 41입니다. 더 흥미로운 점은 compose 자체는 정수에 대해 아무것도 모른다는 것입니다. 그 주 타입은 (b -> c) -> (a -> b) -> a -> c입니다. g의 출력이 f의 입력이므로, 그 두 위치는 b를 공유합니다. a, b, c가 같은 타입이어야 한다고 요구하는 것은 아무것도 없습니다. 정의 안의 두 번의 적용만으로 이 이야기 전체를 얻을 수 있습니다. 바로 이런 점 때문에 추론은 만들어 볼 가치가 있습니다.

구현

두 알고리즘은 불변인 출력 타입과 타입 스킴은 공유하지만, 단일화자나 추론 순회는 공유하지 않습니다. 변수의 정체성은 추론이 끝난 뒤에야 첫 등장 순서에 따라 정규화됩니다. 그 덕분에 두 알고리즘의 주 타입을 이름 바꾸기를 무시하고 비교할 수 있습니다.

#![allow(unused)]
fn main() {
/// Variables are fresh identities; algorithms choose their own representation of solutions.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Type {
    Int,
    Bool,
    Var(u32),
    Arrow(Box<Type>, Box<Type>),
}

/// Quantified variables are freshened independently at every occurrence.
#[derive(Clone, Debug)]
pub struct Scheme {
    pub variables: Vec<u32>,
    pub ty: Type,
}

impl Scheme {
    pub fn mono(ty: Type) -> Self {
        Self {
            variables: vec![],
            ty,
        }
    }
}

impl Type {
    pub fn arrow(a: Self, b: Self) -> Self {
        Self::Arrow(Box::new(a), Box::new(b))
    }
    /// Rename by first occurrence, making principal types comparable up to alpha-renaming.
    pub fn canonical(&self) -> Self {
        fn go(ty: &Type, names: &mut BTreeMap<u32, u32>) -> Type {
            match ty {
                Type::Var(n) => {
                    let next = names.len() as u32;
                    Type::Var(*names.entry(*n).or_insert(next))
                }
                Type::Arrow(a, b) => {
                    Type::arrow(go(a, names), go(b, names))
                }
                other => other.clone(),
            }
        }
        go(self, &mut BTreeMap::new())
    }
}
}

알고리즘 W

algorithm_w.rs는 치환, 인스턴스화, 일반화, 추론을 분리합니다. 핵심 규칙은 Poly의 산술, 조건, 고정점 형식으로 확장되며, 진단을 위해 소스 스팬이 유지됩니다.

치환은 변수를 타입으로 사상합니다. 합성이란 먼저 이전 치환을 적용한 뒤, 그 결과를 더 새로운 치환으로 다시 쓰는 것을 뜻합니다. 스킴에 치환을 적용할 때는 그 스킴의 양화된 변수를 보호해야 합니다.

#![allow(unused)]
fn main() {
impl Subst {
    fn apply(&self, ty: &Type) -> Type {
        match ty {
            Type::Var(n) => {
                self.0.get(n).map_or_else(|| ty.clone(), |t| self.apply(t))
            }
            Type::Arrow(a, b) => Type::arrow(self.apply(a), self.apply(b)),
            other => other.clone(),
        }
    }
    /// self after earlier: every earlier range is rewritten by the newer substitution.
    fn compose(&self, earlier: &Self) -> Self {
        let mut result: BTreeMap<_, _> =
            earlier.0.iter().map(|(n, t)| (*n, self.apply(t))).collect();
        for (n, t) in &self.0 {
            result.entry(*n).or_insert_with(|| t.clone());
        }
        Self(result)
    }
    fn environment(&self, env: &Env) -> Env {
        env.iter()
            .map(|(name, scheme)| {
                let mut filtered = self.clone();
                for n in &scheme.variables {
                    filtered.0.remove(n);
                }
                (
                    name.clone(),
                    Scheme {
                        variables: scheme.variables.clone(),
                        ty: filtered.apply(&scheme.ty),
                    },
                )
            })
            .collect()
    }
}
}

적용은 함수에서 알게 된 정보를 인자를 추론하는 데 쓰이는 환경으로 넘겨줍니다. 그런 다음 함수의 타입을 인자의 타입에서 새로운 결과 타입으로 가는 화살표와 단일화합니다.

#![allow(unused)]
fn main() {
Kind::App(f, a) => {
    let (s1, tf) = self.infer(env, f)?;
    let (s2, ta) = self.infer(&s1.environment(env), a)?;
    let result = self.fresh();
    let s3 = unify(
        &s2.apply(&tf),
        &Type::arrow(ta, result.clone()),
        expr,
    )?;
    Ok((s3.compose(&s2.compose(&s1)), s3.apply(&result)))
}
}

let의 경우에는 일반화하기 전에 우변의 치환을 환경에 적용합니다. 이전 환경을 기준으로 일반화하면 이미 제약된 변수가 빠져나갈 수 있습니다.

#![allow(unused)]
fn main() {
Kind::Let(n, value, body) => {
    let (s1, t) = self.infer(env, value)?;
    let mut local = s1.environment(env);
    local.insert(n.clone(), generalize(&local, s1.apply(&t)));
    let (s2, result) = self.infer(&local, body)?;
    Ok((s2.compose(&s1), result))
}
}

가변 해와 레벨

union_find.rs는 명시적인 치환 맵을 메타변수 셀로 대체합니다. 셀은 자신이 생성된 레벨과 선택적인 해를 기록합니다. 해가 정해진 변수를 따라가면 그 경로가 압축되므로, 이후의 방문에서는 해결된 타입에 더 빨리 도달할 수 있습니다.

#![allow(unused)]
fn main() {
#[derive(Clone)]
struct Meta {
    level: u32,
    solution: Option<Type>,
}

#[derive(Default)]
struct Infer {
    level: u32,
    metas: Vec<Meta>,
}

impl Infer {
    fn fresh(&mut self) -> Type {
        let n = self.metas.len() as u32;
        self.metas.push(Meta {
            level: self.level,
            solution: None,
        });
        Type::Var(n)
    }
    fn zonk(&mut self, ty: &Type) -> Type {
        match ty {
            Type::Var(n) => {
                match self.metas[*n as usize].solution.clone() {
                    None => ty.clone(),
                    Some(t) => {
                        let t = self.zonk(&t);
                        self.metas[*n as usize].solution = Some(t.clone());
                        t
                    }
                }
            }
            Type::Arrow(a, b) => Type::arrow(self.zonk(a), self.zonk(b)),
            other => other.clone(),
        }
    }
}

let의 우변을 추론할 때는 더 깊은 레벨로 들어갑니다. 더 오래된 메타변수에 해를 설치하기 전에, 출현 검사(occurs check) 순회는 그 해에서 도달할 수 있는 모든 메타변수의 레벨을 그 오래된 레벨로 낮춥니다. 이 변수들은 let 안에서 할당되었더라도 이제 바깥 스코프에 속합니다.

#![allow(unused)]
fn main() {
/// One traversal rejects cycles and prevents younger variables escaping their scope.
fn occurs_and_lower(
    &mut self,
    n: u32,
    level: u32,
    ty: &Type,
    expr: &Expr,
) -> Result<(), Diagnostic> {
    match self.zonk(ty) {
        Type::Var(m) if m == n => Err(types::occurs(expr)),
        Type::Var(m) => {
            self.metas[m as usize].level =
                self.metas[m as usize].level.min(level);
            Ok(())
        }
        Type::Arrow(a, b) => {
            self.occurs_and_lower(n, level, &a, expr)?;
            self.occurs_and_lower(n, level, &b, expr)
        }
        _ => Ok(()),
    }
}
fn unify(
    &mut self,
    a: &Type,
    b: &Type,
    expr: &Expr,
) -> Result<(), Diagnostic> {
    let (a, b) = (self.zonk(a), self.zonk(b));
    match (&a, &b) {
        _ if a == b => Ok(()),
        (Type::Var(n), t) | (t, Type::Var(n)) => {
            self.occurs_and_lower(
                *n,
                self.metas[*n as usize].level,
                t,
                expr,
            )?;
            self.metas[*n as usize].solution = Some(t.clone());
            Ok(())
        }
        (Type::Arrow(a, b), Type::Arrow(c, d)) => {
            self.unify(a, c, expr)?;
            self.unify(b, d, expr)
        }
        _ => Err(types::mismatch(expr, &a, &b)),
    }
}
}

감싸는 레벨로 돌아온 뒤, 일반화는 레벨이 여전히 더 깊은 미해결 변수만 선택합니다. 일반화는 환경을 훑지 않습니다. 스킴이 나타날 때마다 그 스킴의 양화된 변수는 새 셀로 대체됩니다. 양화되지 않은 변수는 자신의 정체성을 유지하므로 제약도 그대로 유지합니다.

#![allow(unused)]
fn main() {
Kind::Let(n, value, body) => {
    self.level += 1;
    let result = self.infer(env, value);
    self.level -= 1;
    let scheme = self.generalize(result?);
    env.push((n.clone(), scheme));
    let result = self.infer(env, body);
    env.pop();
    result
}
}

\x -> let y = \z -> x z in ...를 시도해 보십시오. y의 타입은 x에 의존하므로, 우리는 두 호출이 그 타입으로 서로 무관한 타입을 고르게 해서는 안 됩니다. y를 정수와 불리언 양쪽으로 호출하면 실패해야 합니다. 이는 레벨을 낮추는 코드 옆에 두고 보기 좋은 예제입니다. 이 예제는 우리가 지나치게 일반화하면 정확히 무엇이 잘못되는지 보여 줍니다. 우리는 거부되어야 하는 프로그램을 포함하여 이와 같은 예제들로 두 추론기를 비교합니다.

실행해 보기

$ cd crates/ch06_poly
$ cargo run -q -- run tests/programs/poly-id.fun
True
$ cargo run -q -- dump --pass=types tests/programs/missing-annotation.fun
a -> a
$ cargo run -q -- dump --pass=types-w tests/programs/missing-annotation.fun
a -> a
$ cargo run -q -- repl
Poly: :quit, :type EXPR, :parse EXPR, :trace EXPR.
poly> :type \f -> \x -> f x
(a -> b) -> a -> b
poly> :quit

types와 일반적인 검사 경로는 레벨 기반 추론기를 사용합니다. types-w는 알고리즘 W가 독립적으로 낸 결과를 선택합니다. 표시된 주 타입의 자유 변수는 암묵적으로 양화된 것입니다. 평가는 여전히 기본적으로 엄격한 CEK 기계를 사용합니다. 추론 방식을 바꾸어도 런타임 값은 바뀌지 않습니다.

연습 문제

1. 쉬움. 먼저 새 변수들을 적어 둔 다음 \x -> \y -> x의 타입을 추론하십시오.
2. 보통. let id = \x -> x in id id에 대한 치환을 추적하십시오.
3. 보통. 처음에 본 id 예제는 성공하는데 \f -> let a = f 1 in f True는 왜 실패하는지 설명하십시오.
4. 어려움. 바깥 람다 매개변수를 포획하는 안쪽 함수에 대해 메타변수 셀과 레벨을 그려 보십시오. 레벨을 낮추는 단일화를 찾아내십시오.

더 읽을거리

Damas와 Milner는 주 타입 스킴을 확립합니다(Damas and Milner 1982). Kiselyov는 Rémy의 연구(Rémy 1992)를 바탕으로 OCaml 구현을 통해 레벨을 설명합니다(Kiselyov 2013). Pierce는 타입 판단과 유도에 대한 더 폭넓은 입문을 제공합니다(Pierce 2002).

이 아이디어들을 다른 경로로 살펴보려면 타입 시스템만 다룬 제 다른 글을 참고하십시오.