비관련성
비관련성 (Irrelevance)
버전 2.2.8부터 Agda는 비관련성(irrelevancy) 주석을 지원해요. 일반적인 규칙은 점(.)으로 앞에 붙은 어떤 것이든 비관련으로 표시된다는 것이에요. 이는 그것이 타입 체크만 되고 결코 평가되거나 동등성으로 비교되지 않는다는 뜻이에요. 비관련으로 표시된 인자는 컴파일러에 의해 지워져요(erased).
비관련성 주석은 기본적으로 활성화돼요. --irrelevance/--no-irrelevance 옵션으로 활성화/비활성화할 수 있어요.
참고: 이 섹션은 컴파일 타임 비관련성에 관한 것이에요. Agda는 컴파일러에 의해 지워져야 하지만 컴파일 타임에는 여전히 관련적일 수 있는 인자에 사용될 수 있는 런타임 비관련성(Run-time Irrelevance)이라는 더 약한 형태의 비관련성도 지원해요.
참고:
Prop유니버스는 함수 인자와 선언을 비관련으로 표시할 필요가 없는 대안적 형태의 비관련성을 제공해요.
동기 부여 예제 (Motivating example)
비관련성의 의도된 사용 사례 중 하나는 정렬된 리스트 같은 증명이 내장된 데이터 구조예요.
data _≤_ : Nat → Nat → Set where
zero≤ : {n : Nat} → zero ≤ n
suc≤suc : {m n : Nat} → m ≤ n → suc m ≤ suc n
postulate
p₁ : 0 ≤ 1
p₂ : 0 ≤ 1
module No-Irrelevance where
data SList (bound : Nat) : Set where
[] : SList bound
scons : (head : Nat)
→ (head ≤ bound)
→ (tail : SList head)
→ SList bound
보통 증명이 내장된 데이터 타입을 정의할 때 우리는 이 증명들의 값에 대해 추론해야 해요. 예를 들어 같은 원소를 가지지만 서로 다른 증명을 가진 두 리스트 l₁과 l₂가 있다고 가정해 봐요:
l₁ : SList 1
l₁ = scons 0 p₁ []
l₂ : SList 1
l₂ = scons 0 p₂ []
이제 l₁과 l₂가 같다는 것을 증명하고 싶다고 가정해 봐요:
l₁≡l₂ : l₁ ≡ l₂
l₁≡l₂ = refl
그렇게 쉽지 않아요! Agda가 오류를 줘요:
p₁ != p₂ of type 0 ≤ 1
when checking that the expression refl has type l₁ ≡ l₂
p₁과 p₂가 관련적일 때는 refl로 l₁ ≡ l₂를 보여줄 수 없어요. 대신 0 ≤ 1의 증명들에 대해 추론해야 해요.
postulate
proof-equality : p₁ ≡ p₂
이제 이 동등성으로 재작성하여 l₁ ≡ l₂를 증명할 수 있어요:
l₁≡l₂ : l₁ ≡ l₂
l₁≡l₂ rewrite proof-equality = refl
증명의 동등성에 대해 추론하는 것은 곧 짜증나게 돼요. 여기서 우리는 이런 증명에 대한 추론을 피하고 싶어요 — 이 경우 우리는 head ≤ bound의 증명이 존재한다는 것만 신경 쓰므로, 어떤 증명이든 충분해요. 비관련성 주석을 사용해 Agda에게 증명의 값에 신경 쓰지 않는다는 것을 알려줄 수 있어요:
data SList (bound : Nat) : Set where
[] : SList bound
scons : (head : Nat)
→ .(head ≤ bound) -- 점에 주목!
→ (tail : SList head)
→ SList bound
scons 시그니처의 비관련 타입의 효과는, Agda가 그것이 올바른 타입을 가짐을 확인한 후에는 scons의 두 번째 인자가 결코 검사되지 않는다는 것이에요. 타입 체커는 동등성을 검사할 때 비관련 인자를 무시하므로, 두 리스트는 서로 다른 증명을 포함하더라도 같을 수 있어요:
l₁ : SList 1
l₁ = scons 0 p₁ []
l₂ : SList 1
l₂ = scons 0 p₂ []
l₁≡l₂ : l₁ ≡ l₂
l₁≡l₂ = refl
비관련 함수 타입 (Irrelevant function types)
우선 비관련 비-의존 함수 타입을 생각해 봐요:
f : .A → B
이 타입은 f가 계산적으로 그 인자에 의존하지 않음을 함의해요.
비관련 인자에 할 수 있는 것 (What can be done to irrelevant arguments)
예제 1. 두 개의 서로 다른 인자에 대한 알려지지 않은 비관련 함수의 두 적용이 같다는 것을 증명할 수 있어요.
-- 두 번째 인자를 사용하지 않는 알려지지 않은 함수
postulate
f : {A B : Set} -> A -> .B -> A
-- 두 번째 인자는 동등성에 대해 비관련
proofIrr : {A : Set}{x y z : A} -> f x y ≡ f x z
proofIrr = refl
예제 2. 비관련 인자를 다른 비관련 함수의 인자로 사용할 수 있어요.
id : {A B : Set} -> (.A -> B) -> .A -> B
id g x = g x
예제 3. 빈 타입의 비관련 인자에 부정 패턴 ()으로 매칭할 수 있어요.
data ⊥ : Set where
zero-not-one : .(0 ≡ 1) → ⊥
zero-not-one ()
비관련 인자에 할 수 없는 것 (What can’t be done to irrelevant arguments)
예제 1. 비-관련 문맥에서 비관련 값을 사용할 수 없어요.
bad-plus : Nat → .Nat → Nat
bad-plus n m = m + n
Variable m is declared irrelevant, so it cannot be used here
when checking that the expression m has type Nat
예제 2. 함수의 반환 타입을 비관련으로 선언할 수 없어요.
bad : Nat → .Nat
bad n = 1
Invalid dotted expression
when checking that the expression .Nat has type Set _47
예제 3. 비관련 값에 패턴 매칭할 수 없어요.
badMatching : Nat → .Nat → Nat
badMatching n zero = n
badMatching n (suc m) = n
Cannot pattern match against irrelevant argument of type Nat
when checking that the pattern zero has type Nat
예제 4. 비관련 레코드에 매칭할 수도 없어요 (레코드 타입 참고).
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
fst : A
snd : B fst
irrElim : {A : Set} {B : A → Set} → .(Σ A B) → _
irrElim (a , b) = ?
Cannot pattern match against irrelevant argument of type Σ A B
when checking that the pattern a , b has type Σ A B
이것이 허용되면 b는 타입 B a를 가질 텐데, a는 비관련이므로 이 타입은 심지어 잘 형성조차 되지 않아요!
비관련 선언 (Irrelevant declarations)
Postulate와 함수는 이름을 선언할 때 점을 이름 앞에 붙이면 비관련으로 표시할 수 있어요. 비관련 정의는 비관련 함수 타입 .A → B의 함수의 인자로만 사용될 수 있어요.
예제:
.irrFunction : Nat → Nat
irrFunction zero = zero
irrFunction (suc n) = suc (suc (irrFunction n))
postulate
.assume-false : (A : Set) → A
중요한 예는 비관련성 공리 irrAx예요:
postulate
.irrAx : ∀ {ℓ} {A : Set ℓ} -> .A -> A
이 공리는 Agda 내부에서 증명할 수 없지만, 비관련성으로 작업할 때 매우 자주 유용해요. 비관련성 공리는 일종의 비-구성적 선택(non-constructive choice)이에요.
비관련 레코드 필드 (Irrelevant record fields)
레코드 필드(레코드 타입 참고)는 레코드 타입을 정의할 때 이름 앞에 점을 붙이면 비관련으로 표시할 수 있어요. 비관련 필드에 대한 투영(projection)은 --irrelevant-projections 옵션이 주어질 때만 생성돼요 (Agda > 2.5.4부터).
예제 1. 특정 속성을 만족하는 숫자 쌍을 포함하는 레코드 타입.
record InterestingNumbers : Set where
field
n : Nat
m : Nat
.prop1 : n + m ≡ n * m + 2
.prop2 : suc m ≤ n
예제 2. 임의의 타입 A에 대해 모든 원소가 같은 '압축된(squashed)' 버전 Squash A를 정의할 수 있어요.
record Squash (A : Set) : Set where
constructor squash
field
.unsquash : A
open Squash
.example : ∀ {A} → Squash A → A
example x = unsquash x
예제 3. 비관련 멤버십 증명이 있는 P x를 만족하는 x : A의 부분집합을 정의할 수 있어요.
record Subset (A : Set) (P : A -> Set) : Set where
constructor _#_
field
elem : A
.certificate : P elem
.certificate : {A : Set}{P : A -> Set} -> (x : Subset A P) -> P (Subset.elem x)
certificate (a # p) = irrAx p
예제 4. 비관련 투영은 비관련성 공리로 정당화돼요.
.unsquash' : ∀ {A} → Squash A → A
unsquash' (squash x) = irrAx x
.irrAx' : ∀ {A} → .A → A
irrAx' x = unsquash (squash x)
비관련성 공리처럼 비관련 투영은 축약될 수 없어요.
의존 비관련 함수 타입 (Dependent irrelevant function types)
비-의존 함수처럼 의존 함수도 비관련으로 만들 수 있어요. 기본 문법은 다음 예제들과 같아요:
f : .(x y : A) → B
f : .{x y z : A} → B
f : .(xs {ys zs} : A) → B
f : ∀ x .y → B
f : ∀ x .{y} {z} .v → B
f : .{{x : A}} → B
선언
f : .(x : A) → B[x]
f x = t[x]
은 x가 t[x]와 B[x] 양쪽 모두에서 비관련이어야 함을 요구해요. 예를 들어 B[x] = C x(여기서 C : .A → Set)이면 가능해요.
의존 비관련성은 Squash 타입의 제거자(eliminator)를 정의할 수 있게 해줘요:
elim-Squash : {A : Set} (P : Squash A → Set)
(ih : .(a : A) → P (squash a)) →
(a⁻ : Squash A) → P a⁻
elim-Squash P ih (squash a) = ih a
이것은 (ih : (a : A) → P (squash a))로는 타입 체크되지 않는다는 점에 주의하세요.
비관련 인스턴스 인자 (Irrelevant instance arguments)
일반 인스턴스 인자와 달리, 비관련 인스턴스 인자(인스턴스 인자 참고)는 유일한 해를 요구하지 않아요.
record ⊤ : Set where
instance constructor tt
NonZero : Nat → Set
NonZero zero = ⊥
NonZero (suc _) = ⊤
pred′ : (n : Nat) .{{_ : NonZero n}} → Nat
pred′ zero {{}}
pred′ (suc n) = n
find-nonzero : (n : Nat) {{x y : NonZero n}} → Nat
find-nonzero n = pred′ n