10장: 타입이 있는 Core와 Core 린트

새 파일

• src/core_lint.rs
• src/core_type.rs

변경된 파일

• src/core.rs
• src/elaborate.rs
• src/typecheck.rs
• src/eval.rs
• src/lib.rs
• src/main.rs
• src/rename.rs
• src/renamed.rs

동기

타입 검사기가 우리 프로그램을 받아들였습니다. 훌륭합니다. 이제 컴파일러가 프로그램을 다시 쓸 차례인데, 이 과정에서 우리 스스로 실수를 끼워 넣을 기회가 얼마든지 생깁니다. 잘못된 인자를 넘기거나, 타입 인스턴스화를 빠뜨리거나, 변수 정체성을 재사용할 수도 있습니다. 소스 프로그램이 올바르더라도 우리가 그것을 잘못 번역하면 아무 소용이 없습니다.

우리는 Core에 명시적인 타입을 부여하고 이를 위한 두 번째 검사기를 작성하겠습니다. 이 검사기가 맡은 일은 추론보다 쉽습니다. 모든 답이 이미 트리 안에 있으므로, 검사기는 그 답들이 서로 맞아떨어지는지만 확인하면 됩니다. 변환이 잘못되면 문제가 일어난 곳 가까이에서 그것을 잡아낼 수 있습니다. 자기 숙제를 스스로 검사하는 컴파일러는 꽤 쓸모 있는 존재입니다.

현재의 언어

우리는 여전히 타입 인자를 일일이 적지 않고도 다형 함수를 작성할 수 있습니다.

id x = x

number = id 42

main = id True

Core에서 id의 정의는 타입 변수에 대해 추상화합니다. 두 번의 사용에서는 이 함수를 먼저 Int에, 그다음 Bool에 적용합니다. 이러한 적용은 타입이 없는 식에 붙은 주석이 아니라 실제 IR 노드입니다. 평가기는 그 타입들을 무시하므로, 이 프로그램은 여전히 True를 출력합니다.

이론

소스 표현식 id 42에는 작은 결정 하나가 숨어 있습니다. 우리는 항등 함수를 Int에서 사용하고 있습니다. System F는 그 결정을 프로그램 안에 써 넣는 방법을 제공합니다. 타입 추상화(type abstraction)는 타입 매개변수를 도입하고, 타입 적용(type application)은 그 매개변수에 쓸 타입을 고릅니다. Girard와 Reynolds가 다형성을 이렇게 명시적으로 다루는 방식을 개발했습니다 [Girard (1972); Reynolds (1974)].

새로운 두 형태를 일반적인 람다 및 호출과 나란히 놓고 생각해 봅시다. 일반적인 람다는 값을 기다립니다. 타입 추상화는 타입에 대해 추상화합니다. 타입 인자는 런타임 전에 사라지지만, 이 비유는 규칙을 읽는 데 도움이 됩니다.

$$\frac{\Gamma ,\alpha ⊢e:\tau \alpha \notin \mathsf{ftv}(\Gamma )}{\Gamma ⊢\Lambda \alpha .e:\forall \alpha .\tau }\text{(Type abstraction)}$$

$$\frac{\Gamma ⊢e:\forall \alpha .\tau \Gamma ⊢\sigma :\ast }{\Gamma ⊢e[\sigma ]:\tau [\sigma /\alpha ]}\text{(Type application)}$$

이 장에서는 모든 타입 바인더의 카인드가 *입니다. 고차 카인드 생성자는 나중에 카인드 판단을 확장할 것입니다. 일반적인 적용에는 여전히 화살표 타입이 필요합니다. 전칭 한정된 함수는 먼저 자신의 타입 인자를 받아야 합니다.

Core는 System F 전체를 지원합니다. Fun은 여전히 HM 다형성만 드러냅니다. 손으로 만든 Core 항을 사용하면 소스 구문을 확장하지 않고도 그 차이를 시험할 수 있습니다 (Pierce 2002).

구현

Core 데이터 타입

Rust 코드를 보기 전에 같은 언어를 작은 문법으로 적어 볼 수 있습니다. 각 세로 막대는 “또는”으로 읽으십시오. 표현식 $e$는 아래 형태 중 하나이며, 오른쪽 열은 각 형태가 무엇을 하는지 알려 줍니다.

$$\begin{array}{rlrl}e& =x& & \text{local variable}\\ & \mid g& & \text{global reference}\\ & \mid \ell & & \text{literal}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x:\tau .e& & \text{term abstraction}\\ & \mid \Lambda \alpha .e& & \text{type abstraction}\\ & \mid e[\tau ]& & \text{type application}\\ & \mid \text{let}b\text{in}e& & \text{binding group}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid p[\overline{\tau }](\overline{e})& & \text{primitive operation}\end{array}$$

여기서 $x$와 $g$는 각각 지역 값과 전역 값을 가리키고, $\ell$은 리터럴이며, $p$는 프리미티브입니다. 윗줄은 시퀀스를 뜻하므로, $\overline{e}$는 프리미티브의 피연산자들을 평가 순서대로 나타냅니다. 표기법에서는 소스 스팬을 생략하지만, Rust 표현은 진단을 위해 이를 유지합니다.

타입과 바인딩 그룹에는 각각의 문법이 있습니다.

$$\begin{array}{rlrl}\tau & =\text{Int}\mid \text{Bool}\mid \text{Char}\mid \text{String}& & \text{base types}\\ & \mid \alpha & & \text{type variable}\\ & \mid {\tau }_1\to {\tau }_2& & \text{function type}\\ & \mid \forall \alpha .\tau & & \text{universal type}\\ b& =x:\tau =e& & \text{nonrecursive binding}\\ & \mid \text{rec}\{\overline{x:\tau =e}\}& & \text{recursive group}\end{array}$$

재귀 그룹의 이름은 그 그룹의 우변 전체에서 스코프 안에 있습니다. 린트는 또한 그 우변들이 함수를 나타내는지 검사하며, 이 함수는 타입 추상화로 감싸여 있을 수도 있습니다. 비재귀 바인딩에서는 새 이름을 let의 본문에서만 사용할 수 있습니다.

두 가지 람다가 서로 다르다는 점에 주목하십시오. $\Lambda \alpha .\lambda x:\alpha .x$에서 대문자 $\Lambda$는 어떤 값도 고르지 않습니다. 이것은 일반적인 $\lambda$가 사용하는 타입 매개변수를 도입합니다. 이 항등 함수를 타입에 적용한 다음 값에 적용하면 $(\Lambda \alpha .\lambda x:\alpha .x)[\mathsf{Int}]42$가 됩니다. 이것이 우리가 처음에 살펴본 소스 수준의 id 42를 명시적으로 나타낸 버전입니다.

Core 식은 Rust 열거형(enum)입니다. 각 변수와 항 바인더는 자신의 타입을 담은 Id를 지니므로, 린트는 추론을 다시 실행하지 않고도 트리를 검사할 수 있습니다.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
}

식 생성자는 항 수준의 함수(Lam, App)와 타입 수준의 추상화 및 인스턴스화(TyLam, TyApp)를 구별합니다. Let은 리네이머가 만들어 낸 재귀 컴포넌트를 유지합니다. Prim은 명시적인 타입 인자, 평가된 피연산자, 그리고 실패 시 보고할 소스 스팬을 지닙니다.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
}

바인딩 그룹은 타입이 붙은 이름과 우변을 담습니다. 프로그램은 이러한 그룹들을 순서대로 나열한 목록과 진입점으로 이루어집니다:

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
}

이 장에는 아직 If가 있습니다. 데이터 타입 생성자와 패턴 매치는 11장에서, 평탄한 case와 조인 포인트는 16장에서 등장합니다. 여기서는 더 작은 열거형을 사용하므로, 그러한 형태들을 추가하기 전에 타입이 있는 정교화와 린트를 먼저 확립할 수 있습니다.

추론 결과 기록하기

이제 이름이 바뀐 식에는 안정적인 노드 번호가 있습니다. 검사기는 각 변수 출현에서 사용된 새 타입 인자, 각 바인딩의 스킴, 각 람다 매개변수의 단형 타입을 기록합니다. 검사기는 반환하기 전에 이 모든 타입을 zonk하므로, 정교화 단계에서는 가변 메타변수 저장소에 접근할 필요가 전혀 없습니다.

재귀 그룹 안에서 추론된 변수 출현은 처음에는 임시 단형 타입을 보게 됩니다. 컴포넌트가 일반화되고 나면, 정교화 단계는 그 컴포넌트의 재귀적 Core 참조를 대응하는 일반화된 변수로 인스턴스화합니다. 일반적인 출현은 추론 중에 기록된 새 인자를 사용합니다.

다형성 정교화하기

일반화된 각 메타변수는 새로운 Core 타입 식별자를 받습니다. 바인더 타입은 변환된 단형 타입을 Forall로 감쌉니다. 우변은 자신의 항을 그에 맞는 TyLam들로 감쌉니다. 지역 스킴은 여전히 바깥 함수의 추상화가 묶은 타입 변수를 언급할 수 있습니다.

#![allow(unused)]
fn main() {
fn group(
    &mut self,
    group: &renamed::BindGroup,
    outer: &BTreeMap<u32, u32>,
    global: bool,
) -> BindGroup {
    for binding in &group.binds {
        self.binder(
            binding.id.clone(),
            &self.typed.schemes[&binding.id],
            outer,
            global,
        );
    }
    let binds = group
        .binds
        .iter()
        .map(|binding| {
            let binder = self.binders[&binding.id].clone();
            let mut variables = outer.clone();
            variables.extend(binder.quantifiers.iter().copied());
            let mut rhs = self.expression(&binding.rhs, &variables);
            for (_, variable) in binder.quantifiers.iter().rev() {
                rhs = Expr::TyLam(*variable, Box::new(rhs));
            }
            Bind {
                name: binder.id,
                rhs: Box::new(rhs),
            }
        })
        .collect();
    BindGroup {
        recursive: group.recursive,
        binds,
    }
}
}

출현에는 TyApp이 붙고, 람다 매개변수는 변환된 타입을 지닙니다. Core는 전역 참조와 지역 변수를 구별합니다. Core의 바인더 표기는 선언된 환경에 대조하여 검사되므로, 다른 부분이 잘못된 출현에 그럴듯해 보이는 타입을 붙여도 린트를 피해 갈 수 없습니다.

둘러싼 어느 스킴에도 없는 내부 변수에는 닫힌 증거(witness)가 필요합니다. (\f -> 42) (\x -> x)가 그러한 예입니다. 우리는 이렇게 지워지는 표기에 Int를 사용합니다. 이는 소스 식에 기본 타입을 정해 주거나 모호한 클래스 제약을 해소하는 것이 아닙니다.

독립적인 린트

검사기는 항 스코프와 타입 스코프를 유지하고, 이미 사용된 바인더 식별자들의 집합도 함께 관리합니다. 검사기는 화살표 적용, 프리미티브 포화, 조건문 분기, 재귀 함수 그룹, 바인더 표기를 검사합니다. 다음은 명시적 타입 추상화 규칙과 타입 적용 규칙입니다:

#![allow(unused)]
fn main() {
Expr::TyLam(variable, body) => {
    if !self.seen_types.insert(*variable) {
        return Err(format!(
            "duplicate Core type binder t{variable}"
        ));
    }
    self.types.insert(*variable);
    let body = self.expression(body)?;
    self.types.remove(variable);
    Ok(Type::Forall(*variable, Box::new(body)))
}
Expr::TyApp(fun, argument) => {
    self.well_formed(argument)?;
    let function = self.expression(fun)?;
    let Type::Forall(variable, body) = function else {
        return Err(format!(
            "Core type application of non-polymorphic type {function}"
        ));
    };
    Ok(body.substitute(variable, argument))
}
}

타입 적용은 한정된 본문에 치환을 수행합니다. 치환은 인자에 있는 자유 타입 변수를 포획하지 않아야 하며, 이는 우리 일래버레이터 밖에서 구성된 Core 항에 대해서도 마찬가지입니다. 구현은 충돌하는 바인더를 새 이름으로 바꿉니다:

#![allow(unused)]
fn main() {
pub fn substitute(&self, variable: u32, replacement: &Type) -> Type {
    match self {
        Self::Var(v) if *v == variable => replacement.clone(),
        Self::Arrow(a, b) => Self::arrow(
            a.substitute(variable, replacement),
            b.substitute(variable, replacement),
        ),
        Self::Forall(v, _) if *v == variable => self.clone(),
        Self::Forall(v, body) => {
            let (v, body) = if replacement.free().contains(v) {
                let fresh = self
                    .largest()
                    .max(replacement.largest())
                    .max(variable)
                    .checked_add(1)
                    .expect("type variable supply exhausted");
                (fresh, body.substitute(*v, &Self::Var(fresh)))
            } else {
                (*v, *body.clone())
            };
            Self::Forall(
                v,
                Box::new(body.substitute(variable, replacement)),
            )
        }
        _ => self.clone(),
    }
}
}

타입 동등성은 알파 동치이므로, 두 forall 타입이 서로 다른 새 식별자를 사용하더라도 같은 타입을 나타낼 수 있습니다. 반면에 자유 타입 변수는 반드시 같은 바깥 바인더를 가리켜야 합니다.

#![allow(unused)]
fn main() {
pub fn lint(program: &Program) -> Result<(), String> {
    let mut checker = Checker::default();
    for group in &program.groups {
        checker.group(group, true)?;
    }
    checker.expression(&Expr::Global(program.main.clone()))?;
    Ok(())
}
}

여담. 다형 항등 함수의 적용에서 TyApp을 빠뜨리는 컴파일러 버그는 Core application of non-function type forall t0. t0 -> t0을 만들어 냅니다. 소스 프로그램은 올바를 수 있습니다. 생성된 Core는 그렇지 않습니다. 잘못된 Core 테스트는 소스 추론을 다시 실행하지 않고 이 실패를 직접 검사합니다.

소거와 엄격한 실행

TyLam과 TyApp은 런타임 객체를 할당하지 않습니다. 인터프리터는 런타임 값을 치환하지 않고 이들을 그대로 지나갑니다. 이것은 System F를 위한 별도의 런타임 평가 전략이 아니라 소거입니다.

특히 타입 추상화는 엄격한 초기화식을 지연시키지 않습니다. 아래의 사용되지 않는 다형 바인딩은 main이 선택되기 전에 여전히 실패합니다:

unused = (\x -> \y -> y) (div 1 0)

main = 42

18장에서는 명시적으로 소거된 IR을 도입합니다. 코퍼스 실행은 이미 --lint를 활성화합니다.

실행해 보기

$ cd crates/ch10_core
$ cargo run -q -- run tests/programs/core/self-instantiation.fun --lint
42
$ cargo run -q -- dump --pass=core --no-prelude tests/programs/layout/signature.fun
nonrec { id#0 : forall t0. t0 -> t0 = (type-lambda t0 (lambda x#2 : t0 x#2)); }
nonrec { main#1 : Int = (app (type-app @id#0 Int) 42); }
$ cargo test -p ch10_core --test system_f

유용한 실험으로, 작은 Core 항에서 타입 적용 하나를 제거한 뒤 린트를 실행해 보십시오. 이 테스트에서 소스 검사기는 아무 역할도 하지 않습니다. 우리는 컴파일러만이 저지를 수 있었던 실수를 두 번째 검사기에 일부러 넣고 있습니다. 두 번째 검사기는 평가 전에 그 항을 거부해야 합니다.

연습 문제

1. 입문. id id 42에 대한 Core 덤프에서 모든 타입 추상화와 타입 적용을 찾아보십시오.
2. 중급. 포획된 바깥 타입 변수가 지역 바인딩의 스킴에서는 자유 변수로 남지만 완전한 Core 프로그램에서는 속박되는 이유를 설명하십시오.
3. 중급. 인자 개수는 맞지만 피연산자 타입이 잘못된, 잘못된 Core 프리미티브 호출을 구성해 보십시오.
4. 고급. 새 이름 부여를 제거했을 때 타입 치환에서 발생하는 포획 버그를 보이고, 알파 동치만으로는 이를 바로잡을 수 없는 이유를 설명하십시오.

더 읽을거리

명시적 다형성의 원전은 지라르(Girard)의 학위 논문과 레이놀즈(Reynolds)의 논문입니다 [Girard (1972); Reynolds (1974)]. 피어스(Pierce)는 System F의 타입 규칙과 치환 규칙을 전개합니다 (Pierce 2002).