---
title: "비전공자를 위한 1ML 타입 시스템 입문"
published: 2026-01-02T22:32:35.000Z
canonical: https://jeff.news/article/346
---
# 비전공자를 위한 1ML 타입 시스템 입문

Andreas Rossberg의 1ML 타입 시스템을 컴파일러 제작자 관점에서 해설하는 시리즈 첫 편. System Fw 기반 구조, 의미론적 타입 체계, 구현 권장사항을 다룸

## 1ML이란

- Andreas Rossberg가 설계한 타입 시스템으로, ML 스타일 모듈 시스템을 언어에 통합하는 데 현재 가장 좋은 접근법을 제공함
- 문제는 논문이 너무 학술적이라 컴파일러 제작자들과의 소통 장벽이 존재한다는 것임. 저자는 수개월간 1ML을 연구하며 프로토타입 구현을 진행 중임
- 온라인에서 1ML을 "언급"하는 글은 많지만, 깊이 이해하고 논의하는 글은 드묾

## 핵심 구조: System Fw 위의 문법적 설탕

- 1ML의 본질은 System Fw(하스켈의 핵심 타입 시스템으로, 고차 카인드 타입 생성자와 명시적 다형성을 포함)에 대한 정교한 문법적 설탕(syntactic sugar)임
- 표면 타입 T는 즉시 Fw 타입 Xi로 변환되고, 이후 규칙들은 T를 완전히 잊어버림
- Fw 타입 표현식은 기본 "타입"이 Omega(타입의 카인드)인 단순 타입 람다 대수의 항으로 볼 수 있음. 타입 수준에서 계산을 호출할 수 있다는 게 핵심적인 힘이자, 구현자에게는 STLC 인터프리터를 타입 체커에 내장해야 하는 부담이 됨

## 의미론적 타입 체계

- Large(Sigma)와 Small(sigma) 타입은 새로운 문법이 아니라 Fw 타입의 부분 문법임. `{sigma} ⊆ {Sigma} ⊆ {Xi} ⊆ {tau}` 관계가 성립함
- 새로운 타입 생성자로 싱글톤 `[=Xi]`와 순수성 주석이 달린 함수 타입 `Sigma →η Xi`가 추가됨
- Path(`pi = alpha | pi sigma`)는 타입이 대략 정규형임을 강제하는 역할인데, "경로"라는 이름은 사실 오해를 부르는 명칭임

> [!NOTE]
> 추상화 타입 `Xi = ∃alpha.Sigma`에서 ∃를 진짜 존재 양화로 생각하면 직관이 틀어짐. 자유 변수와 그 카인드 정보를 가진 바인더로 이해하는 게 맞음.

## 구현 권장사항

- Fw 타입과 Large 타입을 별도 데이터 타입으로 분리하지 말 것 — Large 타입 하나로 통합할 것
- Small 타입도 별도 데이터 타입으로 만들면 코드 중복이 심해지니, 불변 조건으로만 관리할 것
- Xi(추상화 타입)는 별도 데이터 타입으로 만들 것: `type signat = (type_variable * kind) list * large_type`
- 싱글톤 `[=Xi]`와 함수 타입에 대해서는 전용 생성자를 도입할 것
- 시리즈 다음 편에서는 표면 문법, 디슈가링, 위상 분리를 다룰 예정임

## 핵심 포인트

- 1ML은 System Fw에 대한 정교한 문법적 설탕으로, ML 스타일 모듈 시스템 통합에 최적
- Large/Small 타입은 Fw 타입의 부분 문법이며 싱글톤과 순수성 주석 함수 타입이 추가됨
- 구현 시 Fw 타입과 Large 타입을 통합하고, Xi는 별도 데이터 타입으로 분리할 것을 권장

## 인사이트

학술 논문과 실제 컴파일러 구현 사이의 간극을 메우려는 실용적 해설