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

리파인먼트 타입 (Refinement types) — 논리적 술어 (logical predicates)로 한정된 타입 — 은 Liquid Haskell, F*, Dafny와 같은 언어에서 경량 검증 (lightweight verification)을 위해 효과적임이 입증되었습니다. 그러나 이러한 시스템에서 리파인먼트 (refinements)는 별도의 명세 언어 (specification language)로 작성되거나, 호스트 언어의 타입 시스템 (type system)과 단절된 이차적 주석 (second-class annotations)으로 취급됩니다. 이러한 단절은 사용성 장벽을 만듭니다. 프로그래머는 두 가지 정신 모델 (mental models)을 유지해야 하며, 리파인먼트는 타입 추론 (type inference), 하위 타입 (subtyping), 또는 오버로딩 (overloading)과 같은 기능과 상호작용할 수 없습니다. 본 논문에서는 Scala 3를 위한 일급 리파인먼트 타입 (first-class refinement types)의 설계를 제시하며, 여기서 리파인먼트는 기존 언어 기능과 함께 하위 타입, 추론, 패턴 매칭 (pattern matching)에 참여하는 일반적인 타입입니다. 우리는 의존 함수 타입 (dependent function types), 경계 다형성 (bounded polymorphism), 양의 등가 재귀 타입 (positive equi-recursive types), 합집합 및 교집합 타입 (union and intersection types), 그리고 리파인먼트 타입을 결합하여, 연료 제한 정의적 인터프리터 (fuel-bounded definitional interpreter)와 의미론적 타이핑 (semantic typing)을 사용하는 부분 정당성 의미론 (partial-correctness semantics) 하에서 Rocq로 기계화된 핵심 계산법 (core calculus)의 타입 건전성 (type soundness)을 증명합니다. 마지막으로, 우리는 술어 함의 (predicate entailment)를 위한 경량 e-graph 기반 솔버 (e-graph-based solver)를 포함하여, Scala 3 컴파일러의 프로토타입 확장으로서 우리의 설계를 구현합니다.