부록 B: 타입 규칙

이 규칙들은 Fun 소스 타입 시스템을 선언적으로 기술합니다. 이 규칙들은 패턴, 바인딩 그룹, 클래스, 레코드, IO를 포함하여 이 책 전반에서 사용한 판단들을 한데 모은 것입니다. 이 규칙들은 어떤 프로그램이 올바르게 타입이 매겨지는지를 기술합니다. 구현은 단일화, 레벨, 제약 풀이를 사용하여 그러한 유도를 찾아냅니다. Core에는 10장에서 소개한, 명시적으로 다형적인 자체 타입 판단이 있습니다.

규칙 읽는 법

분수 꼴의 규칙을 아래에서 위로 읽으면 하나의 질문이 됩니다. 결론을 성립시키려면 선 위의 각 전제를 성립시키십시오. 위에서 아래로 읽으면 하나의 증명이 됩니다. 이 전제들이 그 결론을 정당화합니다. 전제가 없는 규칙은 공리입니다. 괄호 안의 이름은 추가 조건이 아니라 해당 단계를 식별하는 것입니다(Pierce 2002).

우리의 주된 판단은 $P;\Gamma ⊢e:\tau$입니다. 이 판단은 $\Gamma$의 변수들이 나열된 스킴을 가지고 $P$의 클래스 술어들이 성립할 때 식 $e$가 타입 $\tau$를 가진다는 뜻입니다. 세미콜론은 환경들을 구분합니다. 이 세미콜론은 Fun 소스에서는 아무 의미도 없습니다. 예를 들면 다음과 같습니다.

$$\frac{x:\mathsf{Int}\in \Gamma }{P;\Gamma ⊢x:\mathsf{Int}}\text{(Var-Int)}$$

타입 환경은 유한 맵입니다. 타입 환경을 $x:\tau$로 확장하면 $x$의 바깥쪽 바인딩이 가려집니다. 윗줄은 시퀀스를 뜻하므로, $\overline{\alpha }$는 0개 이상의 타입 변수를 나타냅니다. 아래첨자 $i$가 붙은 규칙은 지시된 시퀀스의 모든 원소에 적용됩니다. 규칙 아래에 적힌 부가 조건은 그 규칙의 일부입니다.

타입은 완전히 적용된 동의어를 전개한 뒤에 동일성을 판정합니다. 타입 스킴은 속박 변수의 이름 바꾸기를 무시하고 동일성을 판정합니다. 전역 시그니처는 데이터 생성자, 레코드 필드, 클래스, 인스턴스를 기록합니다. 아래의 모든 규칙은 그 시그니처가 선언 검사를 통과했다고 가정합니다.

카인드와 타입 형성

카인드는 $\ast$와 ${\kappa }_1\to {\kappa }_2$입니다. 별은 그 식이 값을 가질 수 있는 타입을 뜻합니다. 카인드 화살표는 항 수준의 함수가 아니라 타입 생성자를 분류합니다.

$$\frac{\alpha :\kappa \in \Delta }{\Delta ⊢\alpha :\kappa }\text{(K-Var)}\frac{T:\kappa \in \Delta }{\Delta ⊢T:\kappa }\text{(K-Con)}$$

$$\frac{\Delta ⊢{\tau }_1:{\kappa }_1\to {\kappa }_2\Delta ⊢{\tau }_2:{\kappa }_1}{\Delta ⊢{\tau }_1{\tau }_2:{\kappa }_2}\text{(K-App)}$$

$$\frac{\Delta ⊢{\tau }_1:\ast \Delta ⊢{\tau }_2:\ast }{\Delta ⊢{\tau }_1\to {\tau }_2:\ast }\text{(K-Arrow)}$$

모든 항의 타입과 생성자 필드는 카인드 $\ast$를 가집니다. 술어 $C\tau$에서 $\tau$는 클래스 매개변수의 카인드를 가져야 합니다. 따라서 Functor는 카인드가 $\ast \to \ast$인 생성자를 받고, Eq는 카인드가 $\ast$인 타입을 받습니다. 카인드는 각 타입 선언 컴포넌트 안에서 함께 추론됩니다. 제약 없이 남은 카인드 변수는 $\ast$가 됩니다. 동의어 순환과 동의어의 부분 적용은, 이후의 단일화가 이를 가려 줄 수 있더라도 오류입니다.

변수, 리터럴, 함수

$$\frac{x:\forall \overline{\alpha }.Q\Rightarrow \tau \in \Gamma P⊢SQ}{P;\Gamma ⊢x:S\tau }\text{(Var)}$$

여기서 $S$는 양화된 변수를 카인드가 일치하는 단형 타입으로 바꿉니다. 생성자도 선언된 타입 스킴을 가지고 같은 규칙을 사용합니다. 리터럴은 클래스 제약 없이 고정된 타입을 가집니다:

$$\frac{}{P;\Gamma ⊢n:\mathsf{Int}}\text{(Int)}\frac{}{P;\Gamma ⊢d:\mathsf{Double}}\text{(Double)}$$

$$\frac{}{P;\Gamma ⊢c:\mathsf{Char}}\text{(Char)}\frac{}{P;\Gamma ⊢s:\mathsf{String}}\text{(String)}$$

$$\frac{P;\Gamma ,x:{\tau }_1⊢e:{\tau }_2}{P;\Gamma ⊢\lambda x.e:{\tau }_1\to {\tau }_2}\text{(Abs)}$$

$$\frac{P;\Gamma ⊢e_1:{\tau }_1\to {\tau }_{2}P;\Gamma ⊢e_2:{\tau }_1}{P;\Gamma ⊢e_1{e}_2:{\tau }_2}\text{(App)}$$

람다 매개변수는 본문 전체에서 단형(monomorphic)입니다. id를 두 번 인스턴스화하면 서로 다른 타입을 고를 수 있습니다. 람다로 바인딩된 f를 두 번 사용할 때는 같은 타입을 지켜야 합니다. 패턴 매개변수는 (Abs)를 적용하기 전에 아래의 패턴 규칙을 거칩니다.

Let, 일반화, 시그니처

$$\frac{P,Q;\Gamma ⊢e_1:{\tau }_{1}P;\Gamma ,x:\sigma ⊢e_2:{\tau }_2}{P;\Gamma ⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:{\tau }_2}\text{(Let)}$$

여기서 $\sigma =\forall \overline{\alpha }.Q\Rightarrow {\tau }_1$입니다. 일반화되는 변수는 ${\tau }_1$ 또는 $Q$에서는 자유 변수이지만 $\Gamma$나 $P$에서는 자유 변수가 아닙니다. $Q$가 언급하는 모든 변수는 ${\tau }_1$에도 나타나야 합니다. 솔버는 먼저 $Q$를 축약하고 단순화한 뒤, 구체적인 술어를 해소하고 모든 필드 제약을 해결합니다. 이 바인딩의 일반화 스코프 바깥에 있는 변수에 대한 술어는 $P$에 남습니다. 일반화할 수도 없고 인스턴스도 있을 수 없는 잔여 술어는 오류입니다. 기본값 지정(defaulting)도 없고 값 제한(value restriction)도 없습니다.

타입 주석이 없는 재귀 컴포넌트에서는 각 $x_i$에 새로운 단형 타입 ${\tau }_i$를 할당한 다음, 모든 본문을 바로 그 가정들 아래에서 검사합니다:

$$\frac{P,Q;\Gamma ,\overline{x:\tau }⊢e_i:{\tau }_{i}P;\Gamma ,\overline{x:\sigma }⊢e:\tau }{P;\Gamma ⊢\mathsf{let}\overline{x=e_i}\mathsf{in}e:\tau }\text{(Let-Rec)}$$

풀린 타입들은 (Let)과 같은 제약 조건 및 모호성 조건을 사용하여, 바깥 환경을 기준으로 함께 일반화합니다. 모든 재귀 우변은 디슈거링 후에 구문적으로 함수여야 합니다. 타입 주석이 없는 컴포넌트 안의 재귀는 단형적입니다.

표기는 새로운 경직 변수로 검사되는 약속입니다.

$$\frac{P,SQ;\Gamma ⊢e:S\tau }{P;\Gamma ⊢e:\forall \overline{\alpha }.Q\Rightarrow \tau }\text{(Signature)}$$

여기서 $S$는 각 양화된 변수를 같은 카인드의 새로운 스콜렘으로 바꿉니다. 이 스콜렘들은 임의의 타입과 단일화될 수 없고 바깥 환경으로 빠져나갈 수도 없습니다. 본문이 요구하는 술어는 $P,SQ$와 인스턴스 환경으로부터 도출되어야 합니다. 타입 주석이 달린 바인딩은 명시된 타입 스킴으로 재귀적으로 사용할 수 있으며, 이 덕분에 다형 재귀가 가능합니다. 의존성 분석은 타입 주석이 없는 컴포넌트를 구성하기 전에 타입 주석이 달린 바인딩으로 향하는 간선을 제거합니다. 식 표기는 이 규칙으로 검사된 다음, 식으로 쓰이도록 인스턴스화됩니다. 이 표기는 퍼스트 클래스(first-class) 다형 값을 도입하지 않습니다.

패턴, 가드, 케이스

판단 $⊢p:\tau \Rightarrow {\Gamma }_p$는 패턴이 타입 $\tau$의 값과 매치되며 ${\Gamma }_p$의 변수들을 도입한다는 뜻입니다.

$$\frac{}{⊢x:\tau \Rightarrow x:\tau }\text{(P-Var)}\frac{}{⊢\_:\tau \Rightarrow {\Gamma }_0}\text{(P-Wild)}$$

$$\frac{⊢p:\tau \Rightarrow {\Gamma }_p}{⊢x@p:\tau \Rightarrow {\Gamma }_p,x:\tau }\text{(P-As)}$$

$$\frac{K:\forall \overline{\alpha }.{\tau }_1\to \dots \to {\tau }_n\to T\overline{\alpha }⊢p_i:S{\tau }_i\Rightarrow {\Gamma }_i}{⊢K\overline{p}:TS\overline{\alpha }\Rightarrow \overline{{\Gamma }_i}}\text{(P-Con)}$$

여기서 ${\Gamma }_0$는 빈 환경입니다. 패턴 환경들의 정의역은 서로 겹치지 않아야 합니다. 리터럴 패턴은 해당 리터럴의 고정된 타입을 가지며 바인딩을 도입하지 않습니다. 레코드 패턴은 선언 순서를 따르는 생성자 패턴이며, 생략된 필드 자리에는 와일드카드가 들어갑니다. 리스트, 튜플, 유닛 패턴은 각자의 일반 생성자를 사용합니다.

$$\frac{P;\Gamma ⊢e:{\tau }_s⊢p_i:{\tau }_s\Rightarrow {\Gamma }_{i}P;\Gamma ,{\Gamma }_i⊢e_i:\tau }{P;\Gamma ⊢\mathsf{case}e\mathsf{of}\overline{p_i\to e_i}:\tau }\text{(Case)}$$

$$\frac{P;\Gamma ,{\Gamma }_p⊢g_j:\mathsf{Bool}P;\Gamma ,{\Gamma }_p⊢e_j:\tau }{P;\Gamma ,{\Gamma }_p⊢\overline{g_j\to e_j}:\tau }\text{(Guards)}$$

가드가 붙은 모든 분기는 case의 결과 타입을 가집니다. 한 행의 where 바인딩은 패턴 환경에서 바인딩 그룹 규칙으로 검사되며, 그 스코프는 해당 행의 가드와 결과 모두에 미칩니다. 함수 등식은 패턴 열마다 인자를 하나씩 도입한 뒤 같은 행 판단을 사용합니다. 모든 등식은 항수(arity)가 같아야 합니다. 망라되지 않은 행과 도달할 수 없는 행은 추가적인 타입 규칙이 아니라 경고를 낳습니다. 매치 실패는 어떤 결과 타입에서든 여전히 발생 가능한 런타임 오류로 남습니다.

비재귀 패턴 바인딩은 먼저 우변과 패턴을 같은 타입으로 검사합니다. 그런 다음 (Let)의 조건에 따라, 도입된 바인더들을 바깥 환경에 대해 일반화합니다. 패턴의 바인더는 그 바인딩의 우변에서는 스코프에 들어 있지 않습니다.

명목적 레코드

$\overline{\alpha }$로 매개변수화된 레코드 선언에서 필드 타입을 $\mathsf{field}(T,l)={\tau }_l$로 쓰고, $S$가 그 실제 타입 인자들을 치환한다고 합시다. 각 규칙은 레코드 생성자가 이미 식별되어 있을 것을 요구합니다.

$$\frac{P;\Gamma ⊢e_i:S{\tau }_{l_i}}{P;\Gamma ⊢K\{\overline{l_i=e_i}\}:TS\overline{\alpha }}\text{(Record)}$$

선언된 모든 필드는 정확히 한 번씩 나타나야 하며, 알 수 없는 레이블은 없어야 합니다. 필드 슬롯은 선언 순서를 따르지만, 평가 순서는 소스 순서가 결정합니다.

$$\frac{P;\Gamma ⊢e:TS\overline{\alpha }\mathsf{field}(T,l)={\tau }_l}{P;\Gamma ⊢e.l:S{\tau }_l}\text{(Project)}$$

$$\frac{P;\Gamma ⊢e:TS\overline{\alpha }P;\Gamma ⊢v_i:S{\tau }_{l_i}}{P;\Gamma ⊢e\{\overline{l_i=v_i}\}:TS\overline{\alpha }}\text{(Update)}$$

갱신 레이블들은 서로 달라야 하며 $T$에 속해야 합니다. 입력, 필드 타입, 결과에 같은 치환이 나타나므로, 갱신은 타입 매개변수를 바꿀 수 없습니다.

추론은 $T$가 알려지기 전에 $\mathsf{Has}(\tau ,l,{\tau }_r)$를 생성합니다. $l$을 선언하는 레코드가 하나뿐이라면, 추론은 새로운 매개변수로 그 레코드를 선택합니다. 그렇지 않으면 $\tau$의 머리 생성자가 정해질 때까지 기다립니다. 솔버는 일반화 전에 이 과정을 반복합니다. 해결되지 않은 필드는 모두 모호한 것으로 간주되며(E0245), 프로그램 전체를 놓고 보면 레코드를 선택할 수 있는 해석이 있더라도 마찬가지입니다. 필드 제약은 절대 스킴에 들어가지 않습니다. (.l)은 \r -> r.l로 검사되므로 같은 제한이 적용됩니다.

클래스 함의와 선언

$$\frac{\pi \in P}{P⊢\pi }\text{(Given)}\frac{P⊢C\tau C\text{ has superclass }D}{P⊢D\tau }\text{(Super)}$$

$$\frac{\mathsf{instance}Q\Rightarrow C\tau P⊢SQ}{P⊢CS\tau }\text{(Instance)}$$

마지막 규칙은 선언된 인스턴스와, 그 머리를 요구된 술어에 맞추는 카인드가 올바른 치환을 사용합니다. 집합의 함의는 모든 원소의 함의를 요구합니다. 슈퍼클래스 프로젝션과 인스턴스 적용은 정교화 과정에서 쓰이는 사전 증거도 함께 구성합니다.

클래스는 매개변수를 하나 가집니다. 클래스의 메서드 시그니처는 그 매개변수를 언급할 수 있지만, 자체적인 제약을 추가할 수는 없습니다. 메서드의 다른 타입 변수는 암묵적으로 한정됩니다. 기본 메서드는 클래스 술어가 주어진 상태에서 선언된 타입으로 검사됩니다. 슈퍼클래스 관계에는 순환이 없어야 합니다.

인스턴스 헤드는 서로 다른 변수에 적용된 생성자입니다. 인스턴스의 컨텍스트는 그 변수들만 제약합니다. 어떤 두 인스턴스 헤드도 서로 겹쳐서는 안 됩니다. 인스턴스 컨텍스트를 주어진 것으로 삼아, 각 메서드를 그 머리에 맞게 특수화된 클래스 메서드 시그니처와 대조하여 검사하십시오. 필요한 슈퍼클래스 사전도 얻을 수 있어야 합니다. 빠진 메서드에는 기본 구현이 있어야 합니다. 파생(deriving)은 이와 똑같은 검사를 거치는 인스턴스를 생성합니다.

데이터 선언은 생성자 스킴을 도입하는데, 그 매개변수는 전칭 한정되고 필드는 연속된 화살표 인자가 됩니다. 생성자의 결과 타입은 선언된 데이터 타입을 가리킵니다. 이 언어에는 존재 변수, GADT 등식, 생성자별 클래스 컨텍스트가 없습니다.

문법적 설탕, IO, 전체 프로그램

이 형태들에는 별도의 추론 메커니즘이 없습니다. 이들의 타입은 전개 결과가 결정합니다:

모나드 생성자 $m:\ast \to \ast$에 대해, 바인드 단계에는 $m\alpha$ 타입의 액션과 결과 타입이 $m\beta$인 컨티뉴에이션이 필요합니다.

$$\frac{P⊢\mathsf{Monad}mP;\Gamma ⊢e:m\alpha ⊢p:\alpha \Rightarrow {\Gamma }_{p}P;\Gamma ,{\Gamma }_p⊢s:m\beta }{P;\Gamma ⊢\mathsf{do}\{p\leftarrow e;s\}:m\beta }\text{(Do-Bind)}$$

표현식 문장은 >>를 사용하고, let 문장은 바인딩 규칙을 사용하며, 마지막 표현식이 블록의 결과를 제공합니다. 반박 가능한 바인드 패턴은 error 폴백을 가진 case로 확장됩니다. MonadFail 제약은 없습니다.

IO는 소스 검사기에 대해 추상적이며 $\ast \to \ast$ 카인드를 가집니다. IO는 Monad의 인스턴스이지만, 소스 프로그램은 IO a를 () -> a와 같다고 볼 수 없습니다. 그 표현은 정교화(elaboration) 중에만 드러납니다. 부수 효과가 있는 프리미티브는 Prelude를 컴파일하는 동안에만 보입니다.

완전한 프로그램은 선언의 카인드를 검사하고, 클래스 환경을 검증하고, 바인딩 컴포넌트를 의존성 순서대로 검사하며, 남은 모든 제약을 풉니다. 프로그램의 진입점은 IO () 타입을 가져야 합니다. 해결되지 않은 클래스 제약이나 필드 제약은 하나도 남아서는 안 됩니다. 최상위 초기화식은 그 액션보다 먼저 의존 순서에 따라 실행됩니다. 이러한 평가 요구 사항은 타입 규칙을 보완합니다: 타입이 올바르다고 해서 종료가 보장되거나 명시적 런타임 오류가 없다는 뜻은 아닙니다.