1ML 타입 시스템, 컴파일러 개발자를 위한 심층 분석

by DD
5개월 전
조회수 11

1ML은 Andreas Rossberg가 설계한 ML 스타일 모듈 시스템으로, 새로운 언어에 통합하기 위한 최적의 선택지 중 하나로 평가됨.

논문의 난해함으로 인해, 1ML에 대한 심층적인 이해보다는 단순 참조가 많은 현실을 지적하며, 핵심 개념을 쉽게 풀이하고자 함.

를 기반으로 하는 1ML의 타입 시스템 구조와 구현 시 고려사항, 특히 Semantic TypesAbstracted Types에 대한 구현 권장 사항을 제시함.

Fω 기반 1ML 타입 시스템 아키텍처

1ML은 System Fω의 syntactic sugar로, Fω는 Haskell의 핵심 타입 시스템을 포함한다. 구체적으로 1ML terms는 Fω terms로, 1ML types는 Fω types로 변환된다. 따라서, 타입 레벨 계산을 통해 강력한 기능을 제공하지만, 구현자는 STLC 인터프리터를 구축해야 하는 부담을 갖는다. 타입 등가 규칙은 컴파일러에서 단방향 감소로 간주되어야 한다.

Semantic Types의 이해와 구현

Semantic types는 Fω types의 하위 집합으로, singleton [=Ξ]와 함수 타입 Σ→ηΞ를 포함한다. 저자는 [=Ξ]와 함수 타입을 별도의 타입 생성자로 처리하는 것을 권장한다. Path 문법은 Fω 타입의 하위 집합을 강제하는 역할을 하며, Abstracted types는 ML의 signature에 해당한다. 따라서, 구현 시에는 Ξ에 대한 별도의 데이터 타입을 생성해야 한다.

1ML 구현을 위한 실질적인 조언

저자는 Fω types를 위한 별도의 데이터 타입을 생성하지 않고, large types Σ를 표현하는 데이터 타입을 사용할 것을 제안한다. 또한, contexts Γ는 large types를 포함해야 하며, small types에 대한 별도의 데이터 타입을 생성하는 것은 코드 중복을 야기할 수 있다. Abstracted type인 Ξ에 대한 별도의 데이터 타입을 생성하고, [=Ξ]에 대한 전용 생성자를 도입하는 것이 좋다. 순수 함수를 위한 구문을 모델링하는 것이 중요하다.

1ML for non-specialists: introduction