선언된 변수의 일반화

선언된 변수의 일반화 (Generalization of Declared Variables)

이 문서는 다음 주제를 다뤄요:

• 개요 (Overview)
• 중첩 일반화 (Nested generalization)
• 일반화된 바인딩의 배치 (Placement of generalized bindings)
• Instance와 비관련 변수 (Instance and irrelevant variables)
• 변수의 임포트와 익스포트 (Importing and exporting variables)
• 상호작용 (Interaction)
• 모달리티 (Modalities)

개요 (Overview)

버전 2.6.0부터 Agda는 타입에서 변수에 대한 암시적 일반화를 지원해요. 일반화될 변수는 variable 블록에서 타입과 함께 선언되어야 해요. 예를 들어:

variable
  ℓ : Level
  n m : Nat

data Vec (A : Set ℓ) : Nat → Set ℓ where
  []  : Vec A 0
  _∷_ : A → Vec A n → Vec A (suc n)

여기서 매개변수 ℓ과 _∷_의 타입에 있는 n은 명시적으로 바인딩되지 않지만, 일반화 가능한 변수로 선언되어 있으므로 이들에 대한 바인딩이 자동으로 삽입돼요. 레벨 ℓ은 데이터 타입의 매개변수로, n은 _∷_의 인자로 추가돼요. 결과 선언은 다음과 같아요:

data Vec {ℓ : Level} (A : Set ℓ) : Nat → Set ℓ where
  []  : Vec A 0
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

바인딩이 어디에 삽입되는지에 대한 자세한 내용은 아래의 일반화된 바인딩의 배치를 참고하세요.

변수는 최상위 타입 시그니처, 모듈 텔레스코프, 레코드와 데이터 타입 매개변수 텔레스코프에서 일반화돼요.

이 기능과 관련된 이슈는 이슈 트래커에서 generalize로 표시돼요.

중첩 일반화 (Nested generalization)

변수를 일반화할 때, 그 타입의 일반화 가능한 변수들도 함께 일반화돼요. 예를 들어 A를 어떤 레벨 ℓ의 타입으로 선언할 수 있어요:

variable
  A : Set ℓ

이제 A가 타입에서 언급되면 레벨 ℓ도 함께 일반화돼요:

-- id : {A.ℓ : Level} {A : Set ℓ} → A → A
id : A → A
id x = x

중첩은 임의로 깊을 수 있어서:

variable
  x : A

refl′ : x ≡ x
refl′ = refl

는 다음으로 확장돼요:

refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x

이름이 어떻게 선택되는지는 아래의 중첩 변수의 명명을 참고하세요.

중첩 변수가 반드시 일반화되는 것은 아니에요. 이 예에서 A의 유니버스 레벨이 고정되어 있으면 일반화할 것이 없어요:

postulate
  -- pure : {A : Set} {F : Set → Set} → A → F A
  pure : {F : Set → Set} → A → F A

자세한 내용은 해결되지 않은 메타변수에 대한 일반화를 참고하세요.

참고: 중첩된 일반화 변수는 각 변수에 로컬이에요. 따라서 다음과 같이 선언하면:

variable
  B : Set ℓ

A와 B는 여전히 서로 다른 레벨에서 일반화될 수 있어요. 예를 들어:

-- _$_ : {A.ℓ : Level} {A : Set A.ℓ} {B.ℓ : Level} {B : Set B.ℓ} → (A → B) → A → B
_$_ : (A → B) → A → B
f $ x = f x

해결되지 않은 메타변수에 대한 일반화 (Generalization over unsolved metavariables)

중첩 변수에 대한 일반화는 각 중첩 변수에 대한 메타변수를 만든 다음 타입 체킹 후에도 여전히 해결되지 않은 그러한 메타에 대해 일반화함으로써 구현돼요. 이것이 이전 섹션의 pure 예제가 작동하게 하는 이유예요: ℓ에 대해 만들어진 메타변수는 레벨 0으로 해결되어 일반화되지 않아요.

이런 일이 발생하는 대표적인 경우는 서로 다른 중첩 변수 사이의 의존성이 있을 때예요. 예를 들어:

postulate
  Con : Set

variable
  Γ Δ Θ : Con

postulate
  Sub : Con → Con → Set

  idS : Sub Γ Γ
  _∘_ : Sub Γ Δ → Sub Δ Θ → Sub Γ Θ

variable
  δ σ γ : Sub Γ Δ

postulate
  assoc : δ ∘ (σ ∘ γ) ≡ (δ ∘ σ) ∘ γ

assoc의 타입에서 각 치환은 그 문맥에 대해 두 개의 중첩 변수 메타를 얻지만, _∘_의 타입은 인자의 문맥이 일치해야 하므로 이러한 메타 중 일부가 해결돼요. 결과 타입은:

assoc : {δ.Γ δ.Δ : Con} {δ : Sub δ.Γ δ.Δ} {σ.Δ : Con} {σ : Sub δ.Δ σ.Δ}
        {γ.Δ : Con} {γ : Sub σ.Δ γ.Δ} → (δ ∘ (σ ∘ γ)) ≡ ((δ ∘ σ) ∘ γ)

여기서 이름에서 σ.Γ이 δ.Δ와 통일되었고 γ.Γ가 σ.Δ와 통일되었음을 볼 수 있어요. 일반적으로 두 메타변수를 통일할 때 "가장 젊은" 것이 제거되므로 δ.Δ와 σ.Δ가 타입에 남는 것들이에요.

중첩 일반화 변수에 대한 메타변수가 부분적으로 해결되면 남은 메타들이 일반화돼요. 예를 들어:

variable
  xs : Vec A n

head : Vec A (suc n) → A
head (x ∷ _) = x

-- lemma : {xs.n.1 : Nat} {xs : Vec Nat (suc xs.n.1)} → head xs ≡ 1 → (0 < sum xs) ≡ true
lemma : head xs ≡ 1 → (0 < sum xs) ≡ true

lemma의 타입에서 xs의 길이에 대한 메타변수가 만들어지고, 적용 head xs가 그것을 어떤 새 메타변수 _n에 대해 suc _n으로 정제해요. _n에 더 이상의 제약이 없으므로 일반화되어 주석에 주어진 타입을 만들게 돼요. 이름 xs.n.1이 어떻게 선택되는지는 아래의 중첩 변수의 명명을 참고하세요.

참고: 중첩 변수에서 비롯된 메타변수만 일반화돼요. 예외는 variable 블록에서 모든 해결되지 않은 메타가 중첩 변수로 바뀌는 경우예요. 이는 다음을 쓴다는 뜻이에요:

variable
  A : Set _

중첩 변수의 명명(아래 참고)까지는 A : Set ℓ과 동등해요.

중첩 변수의 명명 (Naming of nested variables)

중첩된 일반화 변수의 일반적인 명명 체계는 parentVar.nestedVar이에요. 따라서 항등 함수의 경우:

id : A → A

는 다음으로 확장돼요:

id : {A.ℓ : Level} {A : Set ℓ} → A → A

레벨 변수의 이름은 A.ℓ이에요. 그 이유는 중첩 변수의 이름이 ℓ이고 그 부모가 이름 붙은 변수 A이기 때문이에요. 여러 중첩 레벨에 대해 부모는 위의 refl′ 경우처럼 또 다른 중첩 변수가 될 수 있어요:

refl′ : {x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x : x.A} → x ≡ x

중첩 일반화 변수가 더 많은 메타를 포함하는 항으로 해결되면, 위의 lemma 예에서 설명한 대로 이러한 메타들이 일반화돼요. 새 변수의 이름은 parentName.i 형태로, 여기서 parentName은 해결된 변수의 이름이고 i는 해에 나타나는 순서로 1부터 시작하는 메타 번호예요.

변수가 variable 블록의 자유 해결되지 않은 메타변수에서 오면(이 참고 참고), 그 이름은 다음과 같이 선택돼요:

• 함수에 대한 레이블된 인자이면 레이블이 이름으로 사용되고,
• 그렇지 않으면 타입의 무명 변수 목록에서 왼쪽에서 오른쪽으로의 인덱스(1부터 시작)가 이름이에요.

그런 다음 그 타입에 나타나는 이름 붙은 변수를 기반으로 계층적 이름이 주어져요. 예를 들어:

postulate
  V : (A : Set) → Nat → Set
  P : V A n → Set

variable
  v : V _ _

postulate
  thm : P v

여기서 v의 타입에 두 개의 무명 변수가 있어요, 즉 V에 대한 두 인자예요. 첫 번째 인자는 V의 정의에서 레이블 A를 가지므로 이 변수는 이름 v.A를 얻어요. 두 번째 인자는 레이블이 없으므로 v의 타입에서 두 번째 무명 변수이므로 이름 v.2를 얻어요.

변수가 부분적으로 인스턴스화된 중첩 변수에서 오면 메타변수의 이름이 한정되지 않고 사용돼요.

참고: 현재는 함수에 매개변수를 줄 때 계층적 이름을 사용하는 것이 허용되지 않아요. 이슈 #3208을 참고하세요.

일반화된 바인딩의 배치 (Placement of generalized bindings)

일반화된 변수를 배치하는 데 다음 규칙이 사용돼요:

• 일반화된 변수는 타입 시그니처나 텔레스코프의 앞에 배치돼요.
• 다른 타입 시그니처 안에 나타나는 타입 시그니처, 예를 들어 let 바인딩이나 의존 함수 인자에 있는 것들은 일반화되지 않아요. 대신 그러한 타입의 일반화 가능한 변수는 부모 시그니처에서 일반화돼요.
• 더 일찍 언급된 변수는 더 늦게 언급된 변수보다 앞에 배치되며, 중첩 변수는 부모와 함께 언급된 것으로 간주돼요.

참고: 이는 암시적으로 양자화된 변수가 명시적으로 양자화된 변수에 의존할 수 없다는 뜻이에요. 이 제한을 해제하는 기능 요청은 이슈 #3352를 참고하세요.

인덱스된 데이터 타입 (Indexed datatypes)

데이터 타입 매개변수와 인덱스를 일반화할 때 변수는 인덱스에만 언급되면 인덱스로, 그렇지 않으면 매개변수로 바뀌어요.

예를 들어:

data All (P : A → Set) : Vec A n → Set where
  []  : All P []
  _∷_ : P x → All P xs → All P (x ∷ xs)

여기서 A는 매개변수로, n은 인덱스로 일반화돼요. 즉 결과 시그니처는:

data All {A : Set} (P : A → Set) : {n : Nat} → Vec A n → Set where

Instance와 비관련 변수 (Instance and irrelevant variables)

일반화된 변수는 기본적으로 암시 인자로 도입되지만, 변수의 선언에 주석을 달아 instance 인자나 비관련 인자로 바꿀 수 있어요:

record Eq (A : Set) : Set where
  field eq : A → A → Bool

variable
  {{EqA}} : Eq A   -- generalized as an instance argument
  .ignore : A      -- generalized as an irrelevant (implicit) argument

변수는 절대 명시적 인자로 일반화되지 않아요.

변수의 임포트와 익스포트 (Importing and exporting variables)

일반화 가능한 변수는 다른 선언된 기호(함수, 데이터 타입 등)와 같은 방식으로 취급되며, 모듈 사이의 임포트와 익스포트에 같은 메커니즘을 사용해요. 이는 private으로 표시되지 않는 한 모듈에서 익스포트된다는 뜻이에요.

상호작용 (Interaction)

대화형으로 타입을 개발할 때, 이미 일반화된 경우 일반화 가능한 변수를 홀에서 사용할 수 있어요. 하지만 대화형으로 새 일반화를 도입하는 것은 불가능해요. 예를 들어:

works : (A → B) → Vec A n → Vec B {!n!}
fails : (A → B) → Vec A {!n!} → Vec B {!n!}

works에서는 홀에 n을 줄 수 있어요. 인자 벡터에서의 n의 발생으로 바인딩이 도입되었기 때문이에요. 반면 fails에서는 n에 대한 참조가 없어서 두 홀 모두 대화형으로 채울 수 없어요.

모달리티 (Modalities)

일반화 가능한 변수를 선언할 때 모달리티를 줄 수 있어요:

variable
  @0 o : Nat

일반화 과정에서 일반화 가능한 변수는 선언된 모달리티를 얻고, 다른 변수는 항상 기본 모달리티를 얻어요.

더 알아보기 (Learn more)

• Agda 문서: 선언된 변수의 일반화 원문