본문으로 건너뛰기
J
피드

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

backend 약 4분
tags
#type-system#programming-languages#ml#compiler#functional-programming
vote
0
댓글
북마크

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

  • 1

    1ML은 System Fw에 대한 정교한 문법적 설탕으로, ML 스타일 모듈 시스템 통합에 최적

  • 2

    Large/Small 타입은 Fw 타입의 부분 문법이며 싱글톤과 순수성 주석 함수 타입이 추가됨

  • 3

    구현 시 Fw 타입과 Large 타입을 통합하고, Xi는 별도 데이터 타입으로 분리할 것을 권장

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

ℹ️참고

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

구현 권장사항

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

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

prev

이전 기사 (P)

next

다음 기사 (N)

댓글

댓글

댓글을 불러오는 중...

관련 기사

backend

클릭하우스가 PgBouncer 처리량을 4배로 끌어올린 방법

ClickHouse Managed Postgres 팀은 단일 스레드인 PgBouncer를 여러 프로세스로 띄우고 `so_reuseport`와 피어링(peering)을 조합해 16 vCPU 머신을 제대로 쓰게 만들었다. 동일한 AWS 환경에서 단일 프로세스는 약 8.7만 TPS 근처에서 막혔지만, 16개 프로세스 구성은 약 33.6만 TPS까지 올라갔다.

backend

SQLite 쓸 거면 STRICT 테이블을 기본값으로 보자는 주장

SQLite의 STRICT 테이블은 INTEGER 컬럼에 문자열이 들어가는 식의 타입 실수를 막아주는 기능이다. 글쓴이는 SQLite 특유의 유연한 타입 시스템보다, 실수는 빨리 터뜨리는 쪽이 실무에서 낫다고 주장한다. 다만 기존 테이블을 바로 STRICT로 바꾸기 어렵고, SQLite 3.37.0 이상에서만 쓸 수 있다는 제약도 있다.

backend

왜 아직도 Lisp를 배워볼 만한가

Lisp는 괄호가 많은 이상한 언어처럼 보이지만, 핵심은 문법이 아니라 언어 자체를 확장할 수 있다는 점에 있음. 매크로, 코드-데이터 동일성, REPL 중심 개발이 합쳐지면 프로그램을 '작성'한다기보다 살아 있는 시스템을 계속 진화시키는 방식으로 개발하게 됨.

backend

EDB 포스트그레스 AI, 포레스터 멀티모델 데이터 플랫폼 리더 선정

EDB의 AI 데이터 플랫폼 EDB 포스트그레스 AI가 2026년 2분기 포레스터 웨이브 멀티모델 데이터 플랫폼 보고서에서 리더로 선정됐음. 트랜잭션, 분석, AI 워크로드를 하나의 플랫폼에서 다루는 흐름이 강해지는 가운데, EDB는 전략과 현재 제공 기능 모두에서 높은 평가를 받았다고 밝힘.

backend

Bun, Zig에서 Rust로 갈아탔다: 11일짜리 초대형 런타임 포팅 실험

Bun 팀이 53만 줄이 넘는 Zig 코드베이스를 Rust로 기계적으로 포팅했고, Bun v1.4.0부터 Rust 기반으로 전환될 예정임. 핵심 이유는 성능보다 안정성이었고, use-after-free, double-free, 메모리 누수 같은 문제를 컴파일러와 타입 시스템으로 더 빨리 잡기 위해서였음. Claude Code 워크플로 64개를 병렬로 돌려 11일 만에 전 플랫폼 테스트 통과까지 밀어붙인 사례라, LLM 기반 대규모 코드 마이그레이션의 꽤 강한 신호탄임.