비전공자를 위한 1ML 타입 시스템 입문

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)는 타입이 대략 정규형임을 강제하는 역할인데, "경로"라는 이름은 사실 오해를 부르는 명칭임

구현 권장사항

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