Scala를 위한 일급 리파인먼트 타입 (First-Class Refinement Types)

요약

본 논문은 기존 언어들의 리파인먼트 타입이 가진 단절 문제를 해결하기 위해 Scala 3를 위한 일급 리파인먼트 타입 설계를 제안합니다. 제안된 시스템은 리파인먼트를 하위 타입, 타입 추론, 패턴 매칭 등 기존 언어 기능과 통합하여 프로그래머의 인지 부하를 줄입니다. 연구팀은 Rocq를 통해 핵심 계산법의 타입 건전성을 증명하였으며, e-graph 기반 솔버를 포함한 Scala 3 컴파일러 프로토타입 구현을 완료했습니다.

핵심 포인트

• 리파인먼트 타입을 별도의 명세 언어가 아닌 기존 타입 시스템과 통합된 일급 객체로 설계
• 하위 타입, 타입 추론, 패턴 매칭 등 Scala 3의 핵심 기능과 리파인먼트 타입 간의 상호작용 지원
• 의존 함수 타입, 경계 다형성, 합집합 및 교집합 타입을 결합한 정교한 타입 시스템 구축
• Rocq를 이용한 핵심 계산법의 타입 건전성(Type Soundness) 증명
• e-graph 기반의 경량 술어 함의(Predicate Entailment) 솔버 구현