모달리티
모달리티 (Modalities)
Agda는 여러 기능을 구현하기 위해 모달리티의 장치를 사용해요. 그것들이 모두 일반적으로 비슷한 구조를 가지지만, 이 모달리티 시스템들은 모두 같은 동작을 하고 같은 타이핑 규칙을 따르지는 않아요, 특히 정의와 모듈에 관해서는 그래요. 그것들은 두 스타일로 분류할 수 있어요: 위치 모달리티 시스템(Positional modality systems)과 순수 모달리티 시스템(Pure modality systems). Agda의 모달리티 시스템 목록은 다음과 같아요:
- 비관련성(Irrelevance) — 위치형, 점(dot) 접두사 또는
@irr/@irrelevant,@shirr/@shape-irrelevant,@relevant주석 사용. - 런타임 비관련성(Run-time Irrelevance) — 위치형,
@0과@ω사용. - 평면 모달리티(Flat Modality) — 순수형,
@♭과@⊤사용(전자는 후자는 사용자가 명시적으로 쓸 수 없음). - 극성 주석(Polarity Annotations) — 순수형,
@++,@+,@-,@mixed,@unused사용.
일반 모달리티 (General modalities)
모달리티 시스템은 화살표 타입의 정의역(domain)과 정의(where나 let 블록 같은 로컬 정의 포함)에 모달리티 주석을 추가하게 해줘요.
예를 들어 타입 @μ A → B의 함수는 그 인자를 μ-모달리티로 사용한다는 뜻이에요. μ=irr(비관련)이면 그 인자가 함수에게 비관련적이라는 뜻이에요! 정의에 대한 주석은 조금 더 복잡한데(그리고 모달리티 시스템에 따라 다르게 동작하지만), 첫 근사로 정의 @μ f : A는 μ-모달리티로만 사용할 수 있다고 생각하면 돼요.
변수가 예를 들어 패턴 매칭으로 바인딩될 때, Agda는 그것이 어떤 모달리티에서 사용 가능한지 기억하고, 변수가 호환되는 모달리티에서만 사용되는지 확인해요. 예를 들어 관련(relevant) 변수를 비관련적으로 사용할 수 있지만, 비관련 변수를 관련적으로 사용할 수는 없어요.
더 형식적으로, 모달리티 시스템은 다음으로 주어져요:
- 서로 다른 모달리티의 변수가 어떻게 사용될 수 있는지를 관리하는 모달리티의 정렬된 집합.
- 두 인자 모두에서 단조로운 이항 연산
*와 그 연산의 항등 모달리티id로 모달리티를 합성하는 방법. μ ≤ δ*ν인 경우에만δ \\ μ ≤ ν가 되도록 하는 연산\\로 모달리티를 왼쪽 나누는 방법.
사용자가 주석을 지정하지 않으면 기본 모달리티(항상 항등은 아님)가 할당돼요.
문맥 안의 변수 @μ x : A는 μ ≤ id이면 사용 가능하고, (@ν x : A) → B 타입의 항 f에 대해 f s의 부분항 s는 문맥의 모든 모달리티를 ν로 왼쪽 나눈 상태로 검사돼요.
위치 모달리티 시스템 (Positional modality systems)
위치 모달리티 시스템에서 다음과 같은 형태의 정의는
module M Γ where
@μ f : A
문맥이 ν로 나뉘어 ν \\ μ ≤ id가 되는 경우에만 사용될 수 있고, 그들의 타입은 Agda 사용자에게 @μ f : Γ → A로 보여요.
모달 시스템에 대해 "박스형 언박싱(boxed unboxing)"을 갖는 것은 unbox x = x로 @μ unbox : @μ A → A를 유도하는 능력이에요. 소거(erasure) 시스템은 박스형 언박싱을 가지며, --irrelevant-projections가 활성화되면 비관련성도 마찬가지로 가져요.
위치 모달 시스템이 "박스형 언박싱"을 가지면, @μ f : A 같은 정의는 먼저 문맥을 μ로 왼쪽 나눈 다음 검사돼요. 이것이 다음이 --irrelevant-projections로만 타입 체크되는 이유예요:
module M (@irr A : Set) where
@irr B : Set
B = A
이 모달리티 시스템들은 타입 체커가 현재 위치가 어떤 모달리티에 있는지 "기억"하기 때문에 위치형(positional)이라고 불려요.
순수 모달리티 시스템 (Pure modality systems)
앞선 시스템들과 반대로, 순수 모달리티 시스템에서는 다음과 같은 형태의 정의가
module M Γ where
@μ f : A
실제로 μ \\ Γ → A 타입의 최상위 정의와 동등해요. 이것이 다음이
module M (@unused A : Set) where
@unused B : Set
B = A
최상위 정의 M.B : @mixed Set → Set을 주는 이유예요.
최상위 정의 @μ f : A는 항상 먼저 문맥을 모달리티 μ로 왼쪽 나눈 다음 검사돼요.
정의는 그런 다음 문맥 텔레스코프에서 오는 모든 암시적으로 적용된 인자가 적절한 모달리티에서 실제로 사용 가능한 경우에만 사용될 수 있어요. 다음은 타입 체크되지 않아요:
module M (@++ A : Set) where
@unused B : Set
B = A → ⊤
@++ C : Set
C = B
그 이유는 B를 사용하는 시점에 그것을 문맥에 있는 @++ A에 암시적으로 적용하려고 시도하지만, B가 최상위 타입 @mixed Set → Set을 가지므로 이것이 동작하지 않기 때문이에요.