13장: 카인드와 타입 생성자

새 파일

• src/kinds.rs

변경된 파일

• src/types.rs
• src/typecheck.rs
• src/core_lint.rs
• src/ast.rs
• src/core.rs
• src/core_type.rs
• src/data.rs
• src/elaborate.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/parse.rs
• src/rename.rs

동기

Int는 값을 기술합니다. Maybe Int도 마찬가지입니다. 하지만 Maybe는 그 자체만으로는 값을 기술하기 전에 다른 타입을 하나 더 기다리고 있습니다. 우리는 이미 데이터 타입의 인자 개수를 세는 방식으로 이를 처리하고 있습니다. 그런데 그 인자 중 하나가 그 자체로 Maybe 같은 것이라면 어떻게 될까요?

타입이 f a인 필드를 생각해 봅시다. 여기서 f는 타입을 받아야 하고, a는 그 인자 자리를 채웁니다. 우리에게는 이 둘의 서로 다른 역할을 기술할 방법이 필요합니다. 이러한 기술을 카인드(kind)라고 부릅니다. 카인드는 일반 타입의 풍부한 구성 요소 대신 화살표와 *를 사용하므로, 다행히도 낯익어 보입니다.

우리에게 필요한 장치 중 상당수도 이미 익숙한 것입니다. 타입을 추론했던 것과 마찬가지로, 방정식을 풀어 카인드를 추론할 것입니다. 이는 컴파일러의 한 아이디어가 두 번째로 제 몫을 톡톡히 해내는 좋은 예입니다.

현재의 언어

data Wrap f a = Wrap (f a)

unwrap :: Wrap Maybe Int -> Maybe Int
unwrap (Wrap x) = x

main = unwrap (Wrap (Just 42))

Wrap의 카인드는 (* -> *) -> * -> *입니다. data Fix f = Fix (f (Fix f)) 같은 재귀 선언은 Fix에 (* -> *) -> * 카인드를 부여합니다. 선언 간 의존성은 강하게 연결된 요소(strongly connected component)로 묶입니다. 각 요소를 먼저 추론한 뒤에야 제약되지 않은 카인드 변수가 *로 기본 지정됩니다.

type Pair a = (a,a)

type Count = Int

addPair :: Pair Count -> Count
addPair (x,y) = x + y

main = addPair (20,22)

타입 동의어는 생성자도, 런타임 표현도 도입하지 않습니다. 타입 동의어는 완전히 적용되어야 하며, 부분 적용된 데이터 타입이라면 올바른 카인드를 가질 자리에서도 마찬가지입니다. 순환은 사용되지 않는 순환까지 포함하여 거부됩니다. E0301은 카인드 불일치를, E0302는 부분 적용된 동의어를, E0303은 동의어 순환을 보고합니다. 타입 생성자 [], (,), (,,), (->)는 카인드가 허용하는 곳이라면 적용되지 않은 채로 나타날 수 있습니다.

이론

Maybe :: * -> *는 함수 타입과 비슷하게 읽으십시오. 이것은 값들의 타입 하나를 받아 다른 타입을 만들어 냅니다. 이것을 Int :: *에 적용하면 Maybe Int :: *가 됩니다. 카인드 적용 규칙은 바로 그 단계를 적어 놓은 것입니다.

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

함수의 인자와 결과는 각각 카인드 *를 가져야 합니다. 생성자 필드 역시 카인드 *를 가져야 합니다. 적용되지 않은 타입 생성자 Maybe에 속하는 값은 있을 수 없기 때문입니다. 카인드와 타입의 구분은 Pierce (Pierce 2002)가 고차 타입 연산자를 제시한 방식을 따릅니다. Fun은 카인드를 추론하지만 타입 수준 람다나 명시적 카인드 표기를 추가하지는 않습니다.

동의어 치환은 Haskell Report의 완전 적용(fully applied) 관례를 따릅니다(Simon Marlow 2010). 동의어에 들어가기 전에 인자를 먼저 전개하므로, 반복된 이름을 선언 순환으로 오인하지 않고 Id (Id Int)를 허용할 수 있습니다. 정의 스택은 전개 중에 실제 재귀를 탐지합니다.

구현

카인드는 타입이 항을 분류하는 것과 같은 방식으로 타입 생성자를 분류합니다. 구현은 카인드 단일화, 발생 검사, 의존성 순서 결정을 결합하여 그러한 분류를 추론합니다.

#![allow(unused)]
fn main() {
pub enum Kind {
    Star,
    Arrow(Box<Kind>, Box<Kind>),
    Meta(u32),
}
}

Store::unify는 해를 따라가고, 화살표 구조를 비교하며, 자신에게 제안된 해 안에 나타나는 메타변수를 거부합니다. finish는 선언 요소의 모든 필드를 검사한 뒤에야 풀리지 않은 셀을 기본값으로 지정합니다.

#![allow(unused)]
fn main() {
pub fn unify(
    &mut self,
    a: &Kind,
    b: &Kind,
    span: Span,
) -> Result<(), Diagnostic> {
    let (a, b) = (self.zonk(a), self.zonk(b));
    match (&a, &b) {
        _ if a == b => Ok(()),
        (Kind::Meta(n), k) | (k, Kind::Meta(n))
            if !self.occurs(*n, k) =>
        {
            self.solutions[*n as usize] = Some(k.clone());
            Ok(())
        }
        (Kind::Arrow(a, b), Kind::Arrow(c, d)) => {
            self.unify(a, c, span)?;
            self.unify(b, d, span)
        }
        _ => Err(Diagnostic::error(
            ErrorCode::Kind,
            format!("cannot unify kind {a} with {b}"),
            span,
        )),
    }
}
}

선언 패스는 먼저 모든 헤드를 등록한 다음, 9장의 Tarjan 구현을 재사용합니다. 시그니처는 그렇게 닫힌 테이블을 기준으로 암묵적 변수의 카인드를 추론합니다. 불변 데이터 타입 환경은 동의어 사용을 검증하고, 전개된 구문을 추론용 타입으로 변환합니다.

이제 타입 저장소는 각 메타변수에 카인드를 기록합니다. 스킴을 인스턴스화할 때는 변수를 새로 만드는 것뿐 아니라 정량화된 카인드도 복사합니다. f a와 Maybe Int의 단일화는 양쪽에서 마지막 적용을 분리하여, 어느 쪽에도 값 타입일 것을 요구하지 않고 f = Maybe와 a = Int를 풀어 냅니다.

Core는 고유한 타입 바인더 식별자를 키로 하는 카인드 테이블을 유지합니다. 린트는 적용, 생성자 인자, 함수 피연산자를 이 테이블에 비추어 독립적으로 검사합니다. 감싸는 어떤 스킴에도 나타나지 않는 내부 타입 변수는 알맞은 카인드의 닫힌 증인(witness)을 받습니다. 이러한 컴파일러 전용 타입 상수에는 값도 소스 구문도 없으며 소거 단계에서 사라집니다. 이는 10장에서 사용한 Int 증인을 Int가 적합하지 않은 카인드로까지 확장한 것입니다.

실행해 보기

$ cd crates/ch13_kinds
$ cargo run -q -- run tests/programs/kinds/wrapper.fun --lint
Just 42
$ cargo run -q -- dump --pass=types tests/programs/kinds/wrapper.fun
main : Maybe Int
$ cargo run -q -- check tests/programs/kinds/synonym-self.fun
E0303

마지막 명령은 실패하며 잘못된 카인드 적용을 가리킵니다. 다음으로 부분 적용된 데이터 타입 생성자를, 그다음에는 부분 적용된 동의어를 시도해 보십시오. 전자는 상위 카인드에서 유용하게 쓰일 수 있지만, 후자는 우리의 동의어 규칙에 의해 거부됩니다. 빠진 인자의 개수가 겉보기에 같다고 해서 두 선언을 서로 바꿔 쓸 수 있는 것은 아닙니다.

연습 문제

1. 준비 운동. data Compose f g a = Compose (f (g a))의 카인드를 추론하십시오.
2. 중급. data Bad f = Bad (f f)가 발생 검사에서 실패하는 이유를 설명하십시오.
3. 중급. 서로 의존하는 선언들에 대한 카인드 추론 과정을 추적하십시오.
4. 고급. 정교화 과정에서 카인드 * -> *의 내부 증인이 필요한 항을 찾고, 그에 대응하는 Core 적용을 살펴보십시오.

더 읽을거리

• 타입 연산자에 대한 Pierce의 설명 (Pierce 2002).
• Haskell Report의 데이터 타입 및 동의어 규칙 (Simon Marlow 2010).
• 고차 타입 연산자와 System F-omega (Pierce 2002).