Flat 모달리티
Flat 모달리티 (Flat Modality)
@♭/@flat 속성은 멱등 공모나드(idempotent comonadic) 모달리티로서, Spatial Type Theory와 Crisp Type Theory를 모델로 삼았어요. 이것은 필요성 모달리티(necessity modality)와 비슷해요.
이 속성은 감염성 플래그 --cohesion을 사용하여 활성화돼요.
임의의 (@♭ A : Set l)에 대해 귀납적 정의를 통해 ♭ A를 타입으로 정의할 수 있어요:
data ♭ {@♭ l : Level} (@♭ A : Set l) : Set l where
con : (@♭ x : A) → ♭ A
counit : {@♭ l : Level} {@♭ A : Set l} → ♭ A → A
counit (con x) = x
@♭ 인자를 제공할 때는 다른 @♭ 변수들만 사용할 수 있고, 나머지 변수들은 문맥에서 @⊤로 표시돼요.
예를 들어 다음은 타입 체크되지 않아요:
unit : {@♭ l : Level} {@♭ A : Set l} → A → ♭ A
unit x = con x
@♭에서의 패턴 매칭 (Pattern Matching on @♭)
기본적으로 @♭로 표시된 인자에 대한 매칭은 금지되어 있지만, --flat-split 옵션을 사용하여 활성화할 수 있어요.
@♭ 인자에 매칭하면 flat 상태가 생성자의 인자들로 전파돼요:
data _⊎_ (A B : Set) : Set where
inl : A → A ⊎ B
inr : B → A ⊎ B
flat-sum : {@♭ A B : Set} → (@♭ x : A ⊎ B) → ♭ A ⊎ ♭ B
flat-sum (inl x) = inl (con x)
flat-sum (inr x) = inr (con x)
@♭ 변수를 정제(refine)할 때 동일성도 @♭로 제공되어야 해요:
flat-subst : {@♭ A : Set} {P : A → Set} (@♭ x y : A) (@♭ eq : x ≡ y) → P x → P y
flat-subst x .x refl p = p
단순히 (eq : x ≡ y)를 쓰면 코드가 거부돼요.
큐빅 Agda에서 @♭로 표시된 인자에 매칭하는 함수는 UnsupportedIndexedMatch 경고(인덱스된 귀납 타입 참고)를 촉발하고 코드가 제대로 계산되지 않을 수 있다는 점을 주의하세요.
Sharp 모달리티 (The Sharp Modality)
--cohesion 플래그는 Cohesive Homotopy Type Theory에 제시된 대로 sharp 모달리티도 활성화해요.
@♯/@sharp 주석은 멱등 모나딕 모달리티로서, @♭ 모달리티의 우측 수반자(right adjoint)예요.
♯를 다음과 같은 레코드 타입으로 정의할 수 있어요:
record ♯ {l} (@♯ A : Set l) : Set l where
constructor conSharp
field
@♯ ε : A
open ♯
_ : ∀ {@♭ l} {@♭ A : Set l} → @♭ ♯ A → A
_ = ε
@♯ 인자를 제공할 때는 모든 @⊤가 아닌 변수가 @♭로 주석 처리돼요. 레코드로서 코패턴 매칭(copattern matching)으로 ♯의 원소를 정의할 수 있어요. ε로 코패턴 매칭한 후에는 문맥의 모든 변수가 crisp(단단해)져요. 예를 들어 다음에서는 ♭의 생성자에서 a를 사용할 수 있어요:
unit : ∀ {@♭ A : Set} → A → ♯ (♭ A)
unit a .ε = con a