타입 검사기: Hindley–Milner를 Mere로 쓰다

평가기는, 프로그램이 뜻을 이루는지를 개의치 않고 돌린다. 타입 검사기는 그것을 개의하는 부품이다 —— 1 + "hello"를, 도중에 실패하는 대신, 돌기 전에 거부하는 것. 둘 중 셀프 호스트하기가 더 어렵고, 그 이유는 종류의 차이에 있다: 평가기는 그저 계산하면 되고, 트리를 걸으며 값을 낳지만, 타입 검사기는 풀어야 하고, 언어의 바로 중심에 앉은 조용한 추론 알고리즘을 돌린다.

평가기가 요하지 않은 알고리즘

그 알고리즘은 Hindley–Milner 추론, 최소 코어의 회에서 이름 붙여진 것과 같은 것 —— 타입 표기 없이 fn x -> x라고 쓸 수 있고, 그것이 int에서도 bool에서도 쓰일 수 있음을 컴파일러가 스스로 도출해 내는, 그 기구다. 타입 검사기를 셀프 호스트한다는 것은, 그 기구를 Mere로 다시 세우는 것이고, 그것은 어느 HM 구현에나 되풀이해 나타나는 몇 부품으로 귀착한다.

새 타입 변수가 있다 —— 아직 알려지지 않은 타입의 자리 표시자로, 검사기가 즉각 확정할 수 없는 것에 만날 때마다 주조된다. unification이 있다, 그 전체의 심장: 같아야 하는 두 타입 —— 함수가 기대하는 파라미터와, 건네받은 인자 —— 을 받아, 나아가며 미지를 결속하여 같게 하거나, 화해할 수 없으면 실패한다 (int 대 str는 타입 error; 함수 타입 대 함수 타입은 인자와 결과로 재귀한다). unification은 occurs check로 지켜진다. 그것은, 변수를 자신을 포함하는 타입에 결속하기를 거부하여, 추론이 무한 타입을 세울 수 없게 한다. 그리고 다형을 돌게 하는 쌍이 있다: 일반화, 추론된 타입을, 진짜로 자유로운 미지에 대해 양화함으로써 재사용 가능한 스킴으로 바꾸는 것, 그리고 instantiation, 다형 값의 각 사용에, 그 스킴의 자기만의 새 사본을 주는 것. 일반화한 다음 instantiate하는 것이야말로, 하나의 id가 모든 타입에 봉사하게 한다 —— let 다형의 미묘하고, 하중을 짊어지는 세부이고, 조용히 틀리기가 가장 쉬운 부분이다.

평가기는 이 중 아무것도 요하지 않았다. 값을 계산하는 것은 직접적이다; 타입을 푸는 것은 제약 문제이고, 그 해결기를 Mere로 표현하는 것은, 언어가, 자신에게 타입을 주는 바로 그 기구를 명확히 진술하는 것이다.

원래의 대부분은 scope 밖

OCaml 타입 검사기는 천구백 줄 가깝고, 평가기와 마찬가지로, 정직한 한 수는 그 얼마만큼이 self-host를 요하지 않는지에 알아채는 것이다. 그 대략 삼분의 일이 앞 Part의 고급 정적 분석 —— 대여 검사기, region 추적, 능력과 이펙트의 추론, Part II와 III의 기구다. 또 한 조각은 사용자 경험의 광택이다: 철자를 틀린 이름으로의 “혹시” 제안, error 메시지를 친절하게 하는 배려. 그것들을, 당분간 scope 밖으로 옆에 두면, 남는 것은 core의 Hindley–Milner 추론 —— 칠백 줄쯤의 Mere, 평가기와 같은 자릿수의 규모다.

그 scope 설정은 그 자신, Part IV의 커버리지 장부의 정신으로, 태연히 말할 가치가 있는 결정이다. 셀프 호스트 타입 검사기는, 언어의 다형 함수적 심장부를 검사한다; 그것은 아직, Mere를 특징짓는 대여 모드도, region도, 이펙트 시스템도 재구현하지 않는다. 그것들은 당분간 OCaml 레퍼런스에 머물고, 그렇게 말하는 것은, “타입 검사기는 셀프 호스트되었다”가 실제 이상을 함의하는 것을 허용하기보다 정직하다. 셀프 호스트는 한 번에 한 층씩 나아가고, 이 층은 고전적인 코어다.

두 변수를 구별해야 했던 한 곳

작지만 말해 주는 주름이 시작에 앉는다. 구문 트리에는 이미 타입 변수의 개념이 있다 —— 프로그래머가 표기에 쓰는 'a, 파서가 날라 오는 것. 하지만 추론 알고리즘은 자기 종류의 변수를 요한다: 풀면서 발명하는 새 미지, 그것은 전혀 다른 것이다. 하나는 사용자가 쓴 이름; 다른 하나는 검사기가 메우려 하는 구멍. 그것들은 닮아 보인다 —— 둘 다 “타입 변수”다 —— 그리고 혼동하면 버그가 되므로, 셀프 호스트 검사기는 추론의 미지에 별개의 표현을 주어야 했다.

이것은 언어 자신의 되풀이되는 본능 —— 하나의 이름이 슬며시 두 뜻을 나르면, 가른다 —— 이, 이제 자기 자신의 구현 안에서 표면화한 것이다. region과 arena를 통합하고, 대여의 두 축을 가른 것과 같은 규율이, 여기서는, 둘 다 우연히 타입 변수라 불리고 같지 않은 두 가지에 적용된다. 타입 검사기를 Mere로 쓰는 것은, 언어의 설계가 개의하는 구별에, 언어의 설계를 강제하는 검사기 안에서, 직면하는 것을 뜻했다.

파이프라인이 닫힌다

어느 셀프 호스트 부품과도 그러하듯, 타입 검사기는 cross-validate된다: 그것이 추론하는 타입은, 프로그램의 코퍼스 위에서 OCaml 타입 검사기가 추론하는 타입에 대해 체크되고, 일치를 요구받는다. 그리고 그것이 자리 잡아, 끝에서 끝까지의 파이프라인 전체가 Mere에 존재한다 —— 파싱, 타입 검사, 평가 —— 각 단이 언어로 쓰이고, 하나의 구문 트리를 공유하고, 저마다가 OCaml 레퍼런스에 유지된다. Wasm으로 컴파일되어 브라우저에 떨어져, 그것은 세 회에 걸쳐 데모가 향해 온 것이 된다: Mere 프로그램을 붙이면, Mere의 파이프라인이 그 타입을 추론하고 또 그 결과를 계산한다, 완전히 셀프 호스트되어.

이름 붙일 가치가 있는 루프의 닫힘이 있다. 바로 첫 회들은, Mere가 확신할 수 있는 프로그램을 최적화하고, 추론과 명시는 싸우는 것이 아니라 화해하기 위한 것이다 —— 중요한 타입을 쓰고, 나머지는 추론시킨다 —— 라고 논했다. 타입 검사기는, 그 화해를 현실로 만드는 기계이고, 그것이 이제 Mere 자신으로 쓰여 있다. 언어에 그 보장을 주는 기구가, 그것이 보장하는 언어로 표현된다.

셀프 호스트 집합에서 아직 컴파일러의 한 조각이 빠져 있다. 파이프라인은 Mere를 읽고, 검사하고, 해석할 수 있다 —— 하지만 해석하는 것은 컴파일하는 것이 아니다. 셀프 호스트를 완전히 닫으려면, Mere는 코드를 뱉을 수 있어야 한다: 검사된 프로그램을 취해, 기계가 직접 돌리는 무언가를 낳는다. 다음 회: Mere로 쓰인 코드 생성기, 그리고, 언어가 자기 자신을 컴파일할 수 있는 순간.