4장: 단순 타입 람다 대수

새 파일

• src/types.rs

변경된 파일

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

동기

우리의 평가기는 1 True를 기꺼이 실행하려 듭니다. 평가기는 결국 정수가 함수가 아니라는 사실을 알아내지만, 이 실수를 발견하려고 프로그램을 실행할 필요는 없었습니다. 컴파일러가 이런 실수를 대신 잡아 줄 수는 없을까요?

타입 검사기가 하는 일이 바로 이런 종류의 추론입니다. 함수 타입은 함수가 무엇을 받고 무엇을 반환하는지 알려 줍니다. 우리는 이 타입들을 넘기려는 인자와 비교하여 호출을 검사합니다. 규칙은 적어 내려갈 수 있을 만큼 작고, Rust 구현도 이 규칙을 충실히 따를 것입니다.

당분간은 프로그래머에게 람다 매개변수에 타입을 표기해 달라고 요청하겠습니다. 이렇게 하면 명확한 출발점이 생깁니다. 6장에서는 컴파일러가 스스로 타입을 알아내도록 가르칠 것이며, 여기에는 여러 종류의 값에 두루 쓰이는 타입도 포함됩니다.

현재의 언어

타입은 Int, Bool, 그리고 화살표입니다. 화살표는 오른쪽으로 결합하므로 Int -> Bool -> Int는 Int -> (Bool -> Int)를 뜻합니다. 왼쪽에 오는 화살표에는 괄호가 필요합니다.

let choose = \(b : Bool) -> \(x : Int) -> \(y : Int) ->
  if b then x else y
in choose True 10 20

모든 람다 매개변수에 타입을 표기하지만, 호출, 산술, 스코프는 이전과 똑같이 동작합니다. 정수를 함수처럼 다시 호출해 보십시오. 이번에는 평가기가 관여하기 전에 검사기에서 E0201이 나옵니다. 우리는 실수를 발견하는 시점을 과정의 더 앞쪽으로 옮겼습니다.

이론

타입이 있는 문법

새로 추가되는 요소는 각 람다 매개변수에 붙는 타입입니다. 먼저 우리가 쓸 수 있는 타입은 다음과 같습니다. 함수의 입력과 출력 자체가 함수일 수도 있습니다.

$$\begin{array}{rlrl}\tau & =\text{Int}& & \text{integers}\\ & \mid \text{Bool}& & \text{booleans}\\ & \mid {\tau }_1\to {\tau }_2& & \text{function type}\end{array}$$

식은 앞 장에서 이미 본 것들입니다. $\lambda x:\tau .e$의 표기는 검사기에게 $x$에 대해 무엇을 가정해도 되는지 알려 줍니다.

$$\begin{array}{rlrl}e& =x& & \text{variable}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x:\tau .e& & \text{typed abstraction}\\ & \mid n& & \text{integer literal}\\ & \mid \text{True}\mid \text{False}& & \text{boolean literal}\\ & \mid \text{let}x=e_1\text{in}{e}_2& & \text{local binding}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid -e& & \text{integer negation}\\ & \mid e_{1}op{e}_2& & \text{binary operation}\end{array}$$

앞에서와 마찬가지로 $n$은 정수이고 $op$는 +, -, *, /, ==, <, <= 중 하나입니다. 소스 스팬과 파서의 오류 복구용 자리 표시자는 생략합니다. 이 문법은 우리가 파싱할 수 있는 것을 기술합니다. 아래의 타입 규칙은 그런 식 가운데 어떤 것을 안전하게 실행할 수 있는지 결정합니다. 예를 들어 1 True는 여전히 적용의 모양을 갖추고 있지만, 타입 유도는 존재하지 않습니다.

타입 부여와 안전성

타입 환경은 이름을 타입에 대응시킵니다. 변수를 읽을 때는 가장 가까운 바인딩을 찾습니다. 람다는 본문을 검사하는 동안 그 환경을 확장합니다. 적용은 인자를 함수의 정의역과 대조하여 검사합니다 (Pierce 2002).

$$\frac{\Gamma ,x:\tau ⊢e:\sigma }{\Gamma ⊢(\mathsf{lambda}x:\tau .e):\tau \to \sigma }\text{(Abs)}$$

$$\frac{\Gamma ⊢f:\tau \to \sigma \Gamma ⊢a:\tau }{\Gamma ⊢fa:\sigma }\text{(App)}$$

if의 조건은 Bool 타입입니다. 두 분기의 타입은 같습니다. 산술 연산은 정수를 받고, 비교 연산은 불리언을 반환합니다. let은 환경을 확장하기 전에 우변을 검사하므로 재귀적이지 않은 상태로 남습니다. 암묵적인 양화(quantification)는 없습니다. Int -> Int로 표기된 항등 함수는 Bool까지 받을 수는 없습니다.

우리가 얻은 것을 설명해 주는 유용한 개념이 두 가지 있습니다. 보존성(preservation)은 평가 단계를 한 번 밟아도 식의 타입이 바뀌지 않는다는 성질입니다. Int 식에서 시작했다면, 그것을 축약했을 때 갑자기 함수가 나와서는 안 됩니다. 람다 호출에 대한 증명의 핵심 단계는 올바르게 타입이 매겨진 인자를 치환해도 본문의 타입이 그대로 유지된다는 것을 보이는 것입니다. 이것이 바로 치환 보조정리입니다.

진행(progress)은 닫혀 있고 타입이 올바른 식이 값이거나 한 단계 더 진행할 수 있다고 말합니다. 우리는 42를 호출하는 것과 같은 무의미한 명령에 도달하지 않습니다. 0으로 나누면 여전히 런타임 오류가 보고될 수 있으므로, 우리의 나눗셈 프리미티브에는 약간의 단서가 필요합니다. 타입은 이 언어의 형태 실수를 잡아냅니다. 타입이 모든 계산의 성공을 약속하지는 않습니다. Pierce는 이러한 주장 뒤에 있는 증명을 전개합니다 (Pierce 2002).

구현

types.rs는 화살표를 재귀적으로 표현하고, 필요한 괄호와 함께 출력합니다. 아직 메타변수나 치환 맵은 없습니다.

#![allow(unused)]
fn main() {
/// Simple types have no variables, schemes, or implicit quantification.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Type {
    Int,
    Bool,
    Arrow(Box<Type>, Box<Type>),
}

impl Type {
    pub fn arrow(domain: Self, codomain: Self) -> Self {
        Self::Arrow(Box::new(domain), Box::new(codomain))
    }
}

impl fmt::Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Int => write!(f, "Int"),
            Self::Bool => write!(f, "Bool"),
            Self::Arrow(a, b) => {
                if matches!(**a, Self::Arrow(..)) {
                    write!(f, "({a})")?;
                } else {
                    write!(f, "{a}")?;
                }
                write!(f, " -> {b}")
            }
        }
    }
}
}

문법은 화살표의 공역에 오른쪽 재귀를 사용합니다. 이제 AST의 람다 변형은 매개변수 이름 옆에 Type을 저장하므로, 파싱에 성공한 람다에는 항상 타입 표기가 붙어 있습니다.

Type: Type = {
    <a:TypeAtom> "->" <b:Type> => Type::arrow(a, b),
    TypeAtom,
};
TypeAtom: Type = {
    "Int" => Type::Int, "Bool" => Type::Bool, "(" <Type> ")",
};

검사기는 타입 규칙을 그대로 반영합니다. 검사기의 환경은 스택이며, 가장 안쪽 바인딩부터 바깥쪽으로 탐색합니다. 본문 검사가 오류를 반환하더라도 스코프는 꺼내집니다. 적용은 먼저 함수 타입을 찾은 다음 인자를 검사하므로, 호출 전체가 아니라 인자 위치에서 유용한 오류를 보고합니다.

#![allow(unused)]
fn main() {
fn infer(
    expr: &Expr,
    env: &mut Vec<(String, Type)>,
) -> Result<Type, Diagnostic> {
    match &expr.kind {
        Kind::Int(_) => Ok(Type::Int),
        Kind::Bool(_) => Ok(Type::Bool),
        Kind::Var(name) => env
            .iter()
            .rev()
            .find(|(n, _)| n == name)
            .map(|(_, ty)| ty.clone())
            .ok_or_else(|| {
                Diagnostic::new(
                    "E0101",
                    format!("unbound variable {name}"),
                    expr.span.clone(),
                )
            }),
        Kind::Lam(name, parameter, body) => {
            env.push((name.clone(), parameter.clone()));
            let result = infer(body, env);
            env.pop();
            Ok(Type::arrow(parameter.clone(), result?))
        }
        Kind::App(function, argument) => {
            let function_ty = infer(function, env)?;
            let Type::Arrow(domain, codomain) = function_ty else {
                return Err(mismatch(
                    function,
                    "a function type",
                    &function_ty,
                ));
            };
            expect(argument, infer(argument, env)?, &domain)?;
            Ok(*codomain)
        }
        Kind::Let(name, value, body) => {
            let ty = infer(value, env)?;
            env.push((name.clone(), ty));
            let result = infer(body, env);
            env.pop();
            result
        }
        Kind::If(condition, yes, no) => {
            expect(condition, infer(condition, env)?, &Type::Bool)?;
            let ty = infer(yes, env)?;
            expect(no, infer(no, env)?, &ty)?;
            Ok(ty)
        }
        Kind::Neg(value) => {
            expect(value, infer(value, env)?, &Type::Int)?;
            Ok(Type::Int)
        }
        Kind::Binary(op, left, right) => {
            expect(left, infer(left, env)?, &Type::Int)?;
            expect(right, infer(right, env)?, &Type::Int)?;
            Ok(match op {
                Op::Eq | Op::Lt | Op::Le => Type::Bool,
                _ => Type::Int,
            })
        }
        Kind::Error => Err(Diagnostic::new(
            "E0002",
            "unrecovered syntax error",
            expr.span.clone(),
        )),
    }
}
}

작은 expect 도우미는 두 단순 타입을 구조적으로 비교합니다. 불일치가 있으면, 식의 바이트 범위에서 기대한 타입과 발견한 타입을 모두 보고합니다. Ariadne가 소스 발췌를 렌더링합니다. 이 독립형 검사기는 첫 번째 타입 오류에서 멈춥니다. 앞선 어휘 패스와 스코프 패스는 여전히 오류를 수집합니다.

평가기는 표기를 무시하며 3장의 클로저 표현을 그대로 유지합니다. 치환, 정규 순서 축약, 드 브루인 변환은 람다를 처리하는 부분에서 타입을 함께 전달합니다. 덕분에 보존 테스트가 모든 중간 항을 검사할 수 있고, 이름 없는 덤프에서도 주석이 달린 항들이 서로 구별됩니다.

실행해 보기

$ cd crates/ch04_stlc
$ cargo run -q -- run tests/programs/typed-return.fun
42
$ cargo run -q -- dump --pass=types tests/programs/church.fun
Int
$ cargo run -q -- repl
STLC: :quit, :type EXPR, :parse EXPR, :trace EXPR.
stlc> :type \(f : Int -> Bool) -> \(x : Int) -> f x
(Int -> Bool) -> Int -> Bool
stlc> :quit

check는 평가하지 않고 검사만 합니다. 두 실행 엔진 모두 먼저 타입을 검사합니다. :trace도 축약 과정을 표시하기 전에 타입이 잘못된 입력을 거부합니다. 1 / 0의 검사가 성공하는 것은 예상된 결과입니다. 실행은 실패하지만, 그 타입은 Int입니다.

연습 문제

1. 쉬움. 추상화 규칙을 사용하여 choose 예제의 타입을 유도하십시오.
2. 쉬움. (Int -> Bool) -> Int에 괄호가 필요한 이유를 설명하십시오.
3. 보통. 타입이 올바른 함수에 잘못된 타입의 인자를 적용하는 식을 작성하십시오. 진단의 스팬을 확인하십시오.
4. 어려움. 이 계산 체계의 치환 보조정리를 대체 항에 대한 조건까지 포함하여 진술하고, 람다 경우를 직접 증명해 보십시오.

더 읽을거리

Pierce는 진행(progress) 정리와 보존(preservation) 정리의 형식적 증명을 제시합니다(Pierce 2002). Damas와 Milner는 단순 타입을 넘어서는 다음 단계, 즉 주 타입 스킴과 다형적 let이 왜 필요한지를 설명합니다(Damas and Milner 1982). Takenobu Tani의 Type Introduction Illustrated for Casual Haskellers(pdf / github)는 단순 타입부터 GHC가 추가하는 확장에 이르기까지 같은 개념을 그림으로 보여 줍니다.