Without K
Without K
--without-K 옵션은 UIP(동일성 증명의 유일성)를 지원하지 않는 타입 이론 버전, 예를 들어 HoTT(호모토피 타입 이론)와의 호환성을 보장하기 위해 Agda의 타입 체킹 알고리즘에 몇 가지 제한을 추가해요.
--with-K 옵션을 사용해 파일에서 전역 --without-K를 오버라이드할 수 있는데, 프래그마 {-# OPTIONS --with-K #-}를 추가하면 돼요. 이 옵션은 기본적으로 활성화되어 있어요.
참고: Agda 2.6.3 이전에는
--cubical-compatible플래그가 존재하지 않았고,--without-K가 Cubical Agda 특정 코드의 (내부) 생성을 암시하기도 했어요. 구체적인 사항은 Cubical compatible을, 근거는 #5843을 참고하세요.
참고:
--without-K를 사용할 때는 지워진 유니벌런스(erased univalence)를 postulate하는 것이 안전하지 않아요: 그 이론은 아마 일관적이겠지만, 런타임에서 잘못된 결과를 얻을 수 있어요. 대신 Cubical compatible 플래그를 사용해야 해요. 이 제한에 대한 자세한 내용은 #4784를 참고하세요.
패턴 매칭에 대한 제한 (Restrictions on pattern matching)
--without-K 옵션이 활성화되면 Agda는 특정 케이스 분할만 받아들여요. 더 구체적으로, 케이스 분할을 검사하는 통일 알고리즘은 x = x 형태의 방정식을 풀기 위해 삭제(delete) 규칙을 사용할 수 없어요.
예를 들어 K 규칙의 명백한 구현은 받아들여지지 않아요:
K : {A : Set} {x : A} (P : x ≡ x → Set) →
P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p
인자 x≡x에 대해 생성자 refl로 패턴 매칭하면 x가 x와 통일되는데, --without-K가 활성화되면 삭제 규칙을 사용할 수 없으므로 이는 실패해요.
반면 J 규칙의 명백한 구현은 받아들여져요:
J : {A : Set} (P : (x y : A) → x ≡ y → Set) →
((x : A) → P x x refl) → (x y : A) (x≡y : x ≡ y) → P x y x≡y
J P p x .x refl = p x
인자 x≡y에 대해 생성자 refl로 패턴 매칭하면 x가 y와 통일돼요. 이는 Christine Paulin-Mohring 버전의 J 규칙에도 동일하게 적용돼요:
J′ : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set) →
P x refl → (y : A) (x≡y : x ≡ y) → P y x≡y
J′ P p ._ refl = p
자세한 내용은 Jesper Cockx의 박사 논문 'Dependent Pattern Matching and Proof-Relevant Unification' [Cockx (2017)]을 참고하세요.
종료 검사에 대한 제한 (Restrictions on termination checking)
--without-K가 활성화되면 Agda의 종료 검사기는 구조적 하강(structural descent)을 데이터 타입이나 Size로 끝나는 인자로 제한해요. 마찬가지로 가드성(guardedness)도 결과 타입이 데이터 또는 레코드 타입일 때만 추적돼요:
data ⊥ : Set where
mutual
data WOne : Set where wrap : FOne → WOne
FOne = ⊥ → WOne
postulate iso : WOne ≡ FOne
noo : (X : Set) → (WOne ≡ X) → X → ⊥
noo .WOne refl (wrap f) = noo FOne iso f
noo는 타입 X에서 구조적 하강 f < wrap f가 --without-K에서 할인되므로 거부돼요:
data Pandora : Set where
C : ∞ ⊥ → Pandora
postulate foo : ⊥ ≡ Pandora
loop : (A : Set) → A ≡ Pandora → A
loop .Pandora refl = C (♯ (loop ⊥ foo))
loop는 가드성이 타입 A에서 --without-K로 추적되지 않으므로 거부돼요.
이슈 #1023, #1264, #1292를 참고하세요.
유니버스 레벨에 대한 제한 (Restrictions on universe levels)
--without-K가 활성화되면 일부 인덱스된 데이터 타입은 더 높은 유니버스 레벨에서 정의되어야 해요. 특히 모든 인덱스의 타입은 데이터 타입의 sort에 맞아야 해요.
예를 들어 보통(즉 --with-K)에는 Agda가 다음 동일성 정의를 허용해요:
data _≡₀_ {ℓ} {A : Set ℓ} (x : A) : A → Set where
refl : x ≡₀ x
하지만 --without-K에서는 더 높은 유니버스 레벨에서 정의되어야 해요:
data _≡′_ {ℓ} {A : Set ℓ} : A → A → Set ℓ where
refl : {x : A} → x ≡′ x