극성 주석

극성 주석 (Polarity Annotations)

Agda는 함수 인자와 데이터 타입 매개변수에 그들의 극성(polarity)을 명시적으로 주석으로 다는 것을 지원해요. 이는 양성 검사기가 양성을 추론하는 데 사용할 수 있는 모달리티 시스템(modality system)을 사용해요. 이 실험적 기능은 --polarity 옵션으로 활성화해야 해요. 다음은 타입 체크되는 다양한 주석의 샘플 사용 예시예요:

strictly-positive : @++ Set → Set
strictly-positive A = Nat → A

positive : @+ Set → Set
positive A = (A → Nat) → A

negative : @- Set → Set
negative A = A → Nat

mixed : @mixed Set → Set
mixed A = A → A

unused : @unused Set → Set
unused A = Nat

ex : @- Set → Set
ex A = negative (positive A)

ex2 : @mixed Set → Set
ex2 A = mixed (strictly-positive A)

ex3 : @++ Set → Set
ex3 A = unused (negative A)

다음 코드는 타입 체크되지 않아요:

ex3 : @++ Set → Set
ex3 A = mixed (strictly-positive A)

표준 용도는 임의의 엄격 양성 타입 형성자(type-former)의 고정점을 정의하는 것이에요 (이미 Agda에서 귀납 타입이 정의 가능하기 위한 기준이며, 엄격 양성을 참고하되, 극성 모달리티는 이 기준을 타입 시스템에 내면화해요):

data Mu (F : @++ Set → Set) : Set where
  fix : F (Mu F) → Mu F

위 예에서 F가 자신의 인자를 엄격하게 양으로 사용하도록 지정되었기 때문에, 양성 검사기는 Mu F에 대한 재귀 호출이 엄격 양성 위치에 있다는 것을 알므로 생성자에 대한 인자로 F (Mu F)를 허용해요.

@++로 주석된 인자를 받는 함수를 정의할 때, 타이핑 규칙은 그 인자들이 화살표의 왼쪽에 실제로 나타날 수 없음을 보장해요. 다음 올바른 예처럼 인자를 사용하지 않는 함수에 대한 인자로 화살표 왼쪽에 구문적으로 나타날 수는 있어요:

const : @unused Set → Set
const _ = Nat

typechecks : @++ Set → Set
typechecks A = const A → Nat

극성 모달리티 (The polarity modality)

Agda는 모달 시스템을 사용해 극성 주석을 구현해요. 다음은 서로 다른 모달리티와 그 의미예요:

표기	이름	가능한 사용
`@++`	엄격 양성 (Strictly positive)	pi/함수 타입의 도메인을 제외한 어디든
`@+`	양성 (Positive)	pi/함수 타입의 중첩 도메인의 짝수 개수 안
`@-`	음성 (Negative)	pi/함수 타입의 중첩 도메인의 홀수 개수 안
`@mixed`	혼합 (Mixed)	어디든
`@unused`	미사용 (Unused)	어디에도 없음

엄격 양성 타입은 예를 들어 [1]의 섹션 2.3에 설명된 구문적 조건이에요. (엄격 양성 없는) 매우 유사한 시스템이 [2]에 설명되었지만 모달리티 형식을 사용하지 않았어요.

Agda가 어떤 정의를 타입 체크할 때, 주석된 타입을 가진 람다 추상화로 바인딩된 변수들이 그 제한들을 만족하는지 보장해요. pi 타입의 코도메인을 검사할 때는 그러한 제한이 없다는 점에 주의하세요. 예를 들어 (@++ A : Set) → (A → A)는 완벽히 유효해요!

극성 주석은 함수 타입의 도메인과 데이터/레코드 타입 매개변수에만 나타날 수 있어요. 주석된 인자에 대한 패턴 매칭은 혼합 인자에 대해서만 지원돼요.

양성 검사 (Positivity checking)

Agda 양성 검사기는 타이핑 정보의 극성 주석을 사용해 분석을 강화하고 Mu 같은 타입을 받아들여요. 이는 양성 검사기가 그 정보 자체를 자동으로 추론하지 못할 때도 도움이 될 수 있어요. 다음은 주석 없이는 타입 체크되지 않는 조작된 예시예요:

apply-pattern-match : {A B : Set₁} → Nat → (@++ A → B) → @++ A → B
apply-pattern-match zero f = f
apply-pattern-match (suc n) f = f

id : {A : Set₁} → @++ A → A
id x = x

data D : Set where
  node : (u : Nat) → apply-pattern-match u id D → D

참고 문헌 (References)

[1] Michael Abbott, Thorsten Altenkirch, Neil Ghani, "Containers: Constructing strictly positive types", In Theoretical Computer Science, Volume 342, Issue 1, 2005, https://doi.org/10.1016/j.tcs.2005.06.002

[2] Andreas Abel, "Polarized Subtyping for Sized Types", In: Mathematical Structures in Computer Science, 2006, https://doi.org/10.1007/11753728_39

[3] Josselin Poiret, Lucas Escot, Joris Ceulemans, Malin Altenmüller, and Andreas Nuyts. 2023. Read the Mode and Stay Positive. In 29th International Conference on Types for Proofs and Programs (TYPES), https://lirias.kuleuven.be/retrieve/720869

더 알아보기 (Learn more)

Agda 문서: 극성 주석 원문