양성 검사
양성 검사 (Positivity Checking)
참고: 이것은 스텁(stub) 문서예요.
발생 분석 (Occurrence analysis)
기본적으로 Agda는 함수가 인자를 어떻게 사용하는지 분석해요. 예를 들어 Agda는 다음 코드에서 Vec이 자신의 Set 인자를 엄격하게 양으로 사용하므로 D가 엄격하게 양이라고 말할 수 있어요:
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
Vec : Set → Nat → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n
data D : Set where
c : ∀ n → Vec D n → D
하지만 이 분석은 특히 큰 상호(mutual) 블록에서 느릴 수 있어요. --no-occurrence-analysis 플래그로 끌 수 있어요.
이 분석은 미사용 함수 인자를 감지하는 데도 사용돼요. 예를 들어 Agda는 기본적으로 다음 코드에서 F의 마지막 인자가 미사용임을 알아차리고 반사성(reflexivity)의 사용을 받아들여요:
F : Bool → Set → Set
F true _ = Bool
F false _ = ⊤
_ : {b : Bool} → F b Bool ≡ F b ⊤
_ = refl
발생 분석의 대안은 극성을 사용하는 것이에요:
data _×_ (@++ A B : Set) : Set where
_,_ : A → B → A × B
Vec : @++ Set → Nat → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n
data D : Set where
c : ∀ n → Vec D n → D
F : Bool → @unused Set → Set
F true _ = Bool
F false _ = ⊤
_ : {b : Bool} → F b Bool ≡ F b ⊤
_ = refl
NO_POSITIVITY_CHECK 프래그마
프래그마는 데이터/레코드 정의와 상호 블록에 대한 양성 검사기를 꺼요. 이 프래그마는 Agda 2.5.1에서 추가됐어요.
프래그마는 데이터/레코드 정의 또는 상호 블록 앞에 와야 해요. 프래그마는 --safe 모드에서 사용할 수 없어요.
예:
단일 데이터 정의 건너뛰기:
{-# NO_POSITIVITY_CHECK #-}
data D : Set where
lam : (D → D) → D
단일 레코드 정의 건너뛰기:
{-# NO_POSITIVITY_CHECK #-}
record U : Set where
inductive; no-eta-equality
field ap : U → U
옛 스타일 상호 블록 건너뛰기. 데이터/레코드 정의 앞의 상호 블록 어딘가:
mutual
data D : Set where
lam : (D → D) → D
{-# NO_POSITIVITY_CHECK #-}
record U : Set where
inductive; no-eta-equality
field ap : U → U
옛 스타일 상호 블록 건너뛰기. mutual 키워드 앞:
{-# NO_POSITIVITY_CHECK #-}
mutual
data D : Set where
lam : (D → D) → D
record U : Set where
inductive; no-eta-equality
field ap : U → U
새 스타일 상호 블록 건너뛰기. 블록 안의 데이터/레코드의 선언이나 정의 앞 어디든:
record U : Set
data D : Set
record U where
inductive; no-eta-equality
field ap : U → U
{-# NO_POSITIVITY_CHECK #-}
data D where
lam : (D → D) → D
POLARITY 프래그마
극성 프래그마는 postulate에 붙일 수 있어요. 극성은 postulate의 인자가 어떻게 사용되는지를 표현해요. 다음 극성을 사용할 수 있어요:
_: 미사용 (Unused).++: 엄격 양성 (Strictly positive).+: 양성 (Positive).-: 음성 (Negative).*: 알려지지 않음/혼합 (Unknown/mixed).
극성 프래그마는 {-# POLARITY name <zero or more polarities> #-} 형태이고, 결합도 선언이 주어질 수 있는 곳이면 어디든 줄 수 있어요. 나열된 극성은 주어진 postulate의 인자(명시적/암시적/instance)에 왼쪽에서 오른쪽으로 적용돼요. 극성은 현재 모듈 매개변수에 대해서는 줄 수 없어요. postulate가 n개의 인자(모듈 매개변수 제외)를 받으면, 주어지는 극성의 수는 0과 n 사이(포함)여야 해요.
극성 프래그마는 재귀 타입에서 postulated 타입 형성자를 다음과 같은 방식으로 사용할 수 있게 해요:
postulate
∥_∥ : Set → Set
{-# POLARITY ∥_∥ ++ #-}
data D : Set where
c : ∥ D ∥ → D
겉보기에 무해해 보이는 postulate를 극성 프래그마와 함께 사용하면 빈 타입이 주민을 가짐을 증명할 수 있다는 점에 주의하세요:
postulate
_⇒_ : Set → Set → Set
lambda : {A B : Set} → (A → B) → A ⇒ B
apply : {A B : Set} → A ⇒ B → A → B
{-# POLARITY _⇒_ ++ #-}
data ⊥ : Set where
data D : Set where
c : D ⇒ ⊥ → D
not-inhabited : D → ⊥
not-inhabited (c f) = apply f (c f)
d : D
d = c (lambda not-inhabited)
bad : ⊥
bad = not-inhabited d
극성 프래그마는 안전 모드에서 허용되지 않아요.