Type Theory With Erasure

콘스탄틴 테오카리스와 에드윈 브레이디의 논문 "Type Theory With Erasure"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

의존적 타입을 갖는 프로그래밍 언어 (Agda, Idris, Rocq 등) 에서 타입은 종종 값에 의존합니다. 이는 근본적인 모호성을 야기합니다: 프로그램의 어떤 부분이 런타임에서 계산적으로 관련성이 있으며, 어떤 부분이 컴파일 중에 안전하게 소거될 수 있는가?

• 현재의 접근법: 기존 솔루션들은 종종 **양적 타입 이론 (Quantitative Type Theory, QTT)**에 의존합니다. QTT 는 변수 사용량을 추적하기 위해 양적 반환 (quantitative semiring, 예: $\{0 < \omega\}$) 을 사용합니다. 효과적이기는 하지만, QTT 는 부분 구조적 제약과 선형성에 관한 복잡성을 도입합니다. 다른 접근법들은 "유령 분류 (ghost sorts)"나 휴리스틱 전체 프로그램 분석을 사용하는데, 이는 복잡한 의존적 타입에 대해 취약하고 예측 불가능할 수 있습니다.
• 격차: 표준 타입 이론의 메타이론과 원활하게 통합되고, 코드 추출을 지원하며, 복잡한 양적 의미론에 의존하지 않고 명확한 의미론적 기초를 제공하는 구조적, 모듈식, 그리고 축소 (reduction) 가 없는 소거 (erasure) 형식이 필요합니다.

2. 방법론

저자들은 **제 2 차 일반 대수적 이론 (Second-Order Generalised Algebraic Theory, SOGAT)**으로 형식화된 소거를 갖는 타입 이론의 구조적 버전을 제안합니다.

• 합성 위상 구분 (Synthetic Phase Distinction): 양적 반환을 사용하는 대신, 저자들은 합성 명제인 **소거 마커 #**를 사용하여 소거를 위상 구분으로 인코딩합니다.
  • 문맥 $\Gamma$가 명제 $\#$를 포함하는 경우 (즉, $\# \in \Gamma$), 해당 문맥은 "소거된" 것으로 간주됩니다.
  • 이는 런타임 모드 ($\omega$) 와 소거 모드 ($0$) 사이의 구분을 생성합니다.
  • 핵심적으로, $\#$는 진리값이 없는 명제입니다. 임의로 구성되거나 소거될 수 없습니다. 이는 항들을 모드 간에 강제 변환 (coerce) 할 수 있게 하는 마커로 작용합니다.
• 강제 변환 메커니즘: 이 이론은 두 가지 강제 변환을 도입합니다:
  • 소거 ($\#$): 문맥에 $\#$가 확장된 상태에서 항 $a$가 타입 $A$를 갖는다면, 이를 소거된 항으로 강제 변환할 수 있습니다 ($\# a : 0: A$).
  • **상승 (\$):** 항$a$가 소거된 경우,$#$에 대한 가정 하에 이를 런타임 항으로 상승시킬 수 있습니다 ($\$a : \omega: A$).
  • 이들은 정의상 동등성 (definitional equality) 을 기준으로 상호 역함수이며, 소거된 항이 런타임 데이터에 의존하지 않도록 보장합니다.
• 모듈식 SOGAT 형식화: 이 이론은 Martin-Löf 타입 이론 (MLTT) 을 확장하는 SOGAT 로 정의됩니다. 이를 통해 저자들은 범주론적 의미론 (functorial semantics) 과 가족이 있는 범주 (Categories with Families, CwFs) 를 통한 모델 구성을 포함한 기존 SOGAT 의 메타이론을 활용할 수 있습니다.

3. 주요 기여

A. 이론적 형식화

• SOGAT 정의: 이 논문은 TT0(소거를 갖는 타입 이론) 을 SOGAT 로 정의합니다. 여기에는 모드 $\{0, \omega\}$로 색인된 타입 ($Ty$), 항 ($Tm$), 그리고 소거 마커 ($#$) 가 포함됩니다.
• 유도된 소거 단편: 이론의 중요한 기여는 모든 항 생성자 (term former) 에 대한 소거된 버전을 명시적으로 정의할 필요가 없다는 점입니다 (예: $\Pi_0, \Sigma_0$). $\#$가 있는 문맥과 없는 문맥 사이의 동형성으로 인해, 전체 소거 단편은 런타임 단편에서 자동으로 유도됩니다.
• 귀납적 타입: 이 프레임워크는 특정 인자 (예: 인덱스) 를 소거된 것으로 표시할 수 있는 귀납적 타입을 지원합니다. 또한 생성자 자체가 오직 소거 모드에서만 존재할 수 있는 "이국적인 (exotic)" 귀납적 타입을 처리합니다.

B. 의미론적 모델

• Fam(Set) 모델: 저자들은 집합의 가족 (families of sets) 범주 ($Fam(Set)$) 에서 표준 모델을 구성합니다.
  • 이 모델에서 객체는 쌍 $(X_0, X_1)$이며, 여기서 $X_0$는 소거된 데이터를, $X_1$은 런타임 데이터를 나타냅니다.
  • 소거 마커 $\#$는 "작은 명제 (tiny proposition)"로 해석됩니다 (지수화 $\phi$가 기본 구성 요소를 분리하는 객체 $\phi$).
  • 이 모델은 작은 명제를 갖춘 임의의 **그로텐디크 토포스 (Grothendieck topos)**로 일반화됩니다.
• 압축된 유니버스 (Squashed Universes): 소거된 문맥에서 유니버스를 처리하기 위해, 저자들은 **"압축된 유니버스"($\sqrt{\phi}U$)**를 도입합니다. 이는 표준 유니버스의 구조를 유지하지만, 섬유 (fibers) 가 수축 가능 (contractible) 하다는 조건을 만족하는 $\phi$-모달 객체들입니다. 이를 통해 런타임 데이터를 운반하지 않고도 소거된 문맥에서 존재할 수 있습니다.

C. 코드 추출 및 정확성

• 비타입 람다 계산 추출: 저자들은 TT0 프로그램을 **비타입 람다 계산 (untyped lambda calculus)**으로 추출하는 모델을 구성합니다.
  • 런타임 항은 람다 항으로 매핑됩니다.
  • 소거된 항은 종단 객체 (terminal object) 로 매핑되어 (실제로 사라짐).
  • 소거된 변수를 가진 문맥은 그렇지 않은 문맥과 동형입니다.
• 글루링 및 논리적 관계: 정확성을 증명하기 위해, 저자들은 코드 추출 모델과 표준 집합론적 모델 사이의 논리적 관계를 구성하기 위해 **글루링 (gluing)**을 사용합니다.
  • 정리 27 (비간섭성): 모든 소거된 함수는 런타임에서 상수임을 증명합니다. 만약 함수가 소거된 인자를 취한다면, 그 출력은 런타임에서 그 인자에 의존할 수 없습니다.
  • 정리 25 및 26: 카논성 (canonicity) 과 추출된 코드가 의미론적 해석을 추적함을 증명합니다.

D. 구현

• 엘라보레이터 (Elaborator): Agda 로 간단한 엘라보레이터가 구현되었습니다. 이는 고수준 언어 (Idris/Agda 와 유사하며 0 및 @0 주석이 있음) 를 입력받아 핵심 SOGAT 로 엘라보레이션합니다.
• 패턴 통일 (Pattern Unification): 저자들은 핵심이 구조적이기 때문에, 복잡한 양적 검사나 소거된 메타변수를 위한 특수한 일반화 메커니즘이 필요 없이 표준 패턴 통일 알고리즘을 재사용할 수 있음을 보여줍니다. 이는 현재 Agda 와 Idris 구현체에서 발견되는 문제들을 해결합니다.

4. 결과

• 보존성: 이 이론은 MLTT 에 대해 **보존적 (conservative)**임이 증명되었습니다. 소거를 추가해도 타입 이론의 증명력이 증가하지 않습니다. TT0 에서 증명 가능한 모든 정리는 표준 MLTT 에서도 증명 가능합니다.
• 독립성: 소거된 데이터는 런타임 데이터와 독립임이 증명되었습니다. 문맥 $\Gamma$의 소거된 항은 "영화된 (zeroed)" 문맥 $0\Gamma$(모든 모드가 0 으로 설정됨) 의 소거된 항과 유일하게 대응됩니다.
• 추출의 정확성: 글루링 증명은 추출 과정이 계산적 행동을 보존하고 관련 없는 데이터를 올바르게 소거함을 확인시켜 주며, 생성된 코드가 안전하고 효율적임을 보장합니다.

5. 의의

• 구조적 명확성: 양적 반환에서 합성 위상 구분으로 이동함으로써, 이 논문은 소거를 위한 더 깨끗하고 모듈식인 기초를 제공합니다. 이는 소거의 개념을 리소스 추적의 메커니즘과 분리합니다.
• 구현 지침: 구조적 접근법은 타입 체커와 엘라보레이터의 구현을 단순화합니다. 통일 과정에서 임시방편적인 양적 검사가 필요 없어지며, 이는 Idris 2 및 Agda 와 같은 기존 시스템의 버그를 잠재적으로 수정할 수 있습니다.
• 의미론적 기초: 그로텐디크 토포스와 작은 명제의 사용은 소거를 더 넓은 범주 논리와 연결하여, 메타이론적 증명을 위해 **합성 테이트 계산 가능성 (Synthetic Tait Computability)**을 사용할 수 있게 합니다.
• 미래 확장: 이 프레임워크는 확장 가능하도록 설계되었으며, 런타임 타입, 다중 위상 구분 (스테이징/메타프로그래밍용), 그리고 Cubical Type Theory 와의 통합에 대한 잠재적인 미래 작업을 지원합니다.

요약하자면, 이 논문은 소거를 갖는 타입 이론에 대한 엄격하고 구조적이며 의미론적으로 기초를 둔 접근법을 제시하며, 이론적 보장 (보존성, 비간섭성) 과 컴파일러 구현 및 코드 추출을 위한 실용적 이점을 모두 제공합니다.