불투명 정의
불투명 정의 (Opaque definitions)
불투명 정의는 Agda 정의의 펼침(unfolding)을 제어하기 위한 메커니즘으로, 목표의 가독성과 성능 모두를 돕는 데 목적이 있어요. 추상 정의(abstract definitions)처럼 불투명 정의는 일반적으로 펼쳐지지 않지만, 추상 정의와 달리 사용하는 지점에서 불투명성을 선택적으로 제어할 수 있어요.
우리의 펼침 제어 구현은 Gratzer 등이 'Controlling unfolding in type theory'에서 소개한 이론에 기반하지만, (큐빅) 확장 타입에 의존하지 않고 전적으로 정교화(elaborator) 수준에서 처리돼요.
개요 (Overview)
함수 정의(사용자가 작성했거나 반사(reflection)로 생성된)는 불투명으로 표시할 수 있어요. 불투명 블록 밖에서는 이들은 postulate처럼 동작해요.
불투명 블록은 (관련 없는 모듈에서도) 펼침 절(unfolding clauses)을 가질 수 있어요. 이를 통해 사용자는 로컬에서 투명하게 취급되어야 할 이름 선택을 나열할 수 있어요.
불투명 정의는 (그렇지 않으면 펼쳐질 불투명 블록 안에서도) 타입 시그니처에서 축약되지 않아요.
불투명 정의 펼치기 (Unfolding opaque definitions)
정수를 추상 setoid로 구현한 것을 생각해 봐요: 기본 표현은 차이를 나타내는 자연수 쌍으로 주어지지만, 일상적으로는 ℤ를 그 자체의 타입으로 다루고 싶어요.
우리의 핵심 모듈이 다음 연산들을 정의할 수 있어요:
module Integer where
opaque
ℤ : Set
ℤ = Nat × Nat
_≡ℤ_ : (x y : ℤ) → Set
(p , n) ≡ℤ (p' , n') = (p + n') ≡ (p' + n)
infix 10 _≡ℤ_
0ℤ : ℤ
0ℤ = 0 , 0
1ℤ : ℤ
1ℤ = 1 , 0
_+ℤ_ : (x y : ℤ) → ℤ
(p , n) +ℤ (p' , n') = (p + p') , (n + n')
_*ℤ_ : (x y : ℤ) → ℤ
(a , b) *ℤ (c , d) = ((a * c) + (b * d)) , ((a * d) + (b * c))
infixl 20 _+ℤ_
infixl 30 _*ℤ_
-ℤ_ : ℤ → ℤ
-ℤ (p , n) = (n , p)
이제 정수가 _≡ℤ_ 동일성 개념 아래에서 환(ring)을 이룬다는 것을 증명하고 싶어해요. 관련된 자연수 방정식 중 일부는 꽤 지저분해서, 세미링 방정식 솔버 없이는 증명하기 매우 어려울 것이에요. 하지만 그런 솔버는 반사(reflection) 메커니즘에 의존해서, Integer 모듈이 환을 이룬다는 것을 증명하는 데 관심 없는 사람들에게는 의존 트리를 부풀릴 거예요.
다행히 ℤ가 abstract가 아니라 opaque이기 때문에, Integer-ring 같은 다른 모듈은 ℤ의 정의를 펼치는 불투명 블록에서 자신의 증명을 제공할 수 있어요:
module Integer-ring where
open Integer
opaque
unfolding ℤ
distlℤ : ∀ x y z → x *ℤ (y +ℤ z) ≡ℤ x *ℤ y +ℤ x *ℤ z
distlℤ (a , b) (c , d) (e , f) = use-nat-solver where postulate
use-nat-solver
: a * (c + e) + b * (d + f) + (a * d + b * c + (a * f + b * e))
≡ a * c + b * d + (a * e + b * f) + (a * (d + f) + b * (c + e))
distlℤ의 정의가 unfolding ℤ 절이 있는 불투명 블록 안에 있으므로, ℤ의 불투명성과 ℤ의 불투명 블록이 펼치는 모든 이름들(아래 참고)을 꿰뚫어 볼 수 있어요.
실제로 무엇이 펼쳐지나요? (What actually unfolds?)
불투명 블록이 검사될 때, Agda는 펼칠 수 있는 이름의 집합을 사전에 계산해요. 이 집합은 정의별이 아니라 블록별이에요. 펼침 절이 불투명 이름을 언급하면, 그 이름들과 관련된 펼침 집합이 현재 블록에 추가돼요.
다음은 이 규칙들의 동작을 보여줘요:
불투명 블록의 어떤 이름을 펼치면 그 블록의 다른 이름들도 펼쳐지게 돼요. 예:
module _ where private
opaque
x : Nat
y : Nat
x = 3
y = 4
opaque
unfolding x
_ : y ≡ 4
_ = refl
여기서는 x만 요청했지만 y도 펼침에 이용 가능해요.
절이 가져오는 펼침 집합이 블록에 연관되어 있으므로 펼침은 전이적이에요:
module _ where private
opaque
x : Nat
x = 3
opaque
unfolding x
y : Nat
y = 4 + x
opaque
unfolding y
_ : y ≡ 7
_ = refl
어휘적으로 중첩된 불투명 블록은 자식 블록이 정의될 때 그 이름이 스코프에 없어도 부모 블록의 이름을 펼칠 수 있어요:
module _ where private
opaque
x : Nat
x = 3
opaque
y : Nat
y = 4
_ : x ≡ 3
_ = refl
z : Nat
z = 5
opaque
unfolding y
_ : z ≡ 5
_ = refl
y를 정의하는 불투명 블록이 부모 블록을 "분할"하지 않기 때문에 x와 z가 같은 불투명 블록의 직접 자식이기 때문이에요.
여러 펼침 절이 지원되며, 절마다 두 개 이상의 이름을 펼치는 것도 지원돼요. 후자의 문법은 단순히 공백으로 구분된 이름 목록이며, 이들은 모호하지 않은 함수를 가리켜야 해요:
module _ where private
opaque
x : Nat
x = 3
opaque
y : Nat
y = 4
opaque
z : Nat
z = 5
opaque
unfolding x y
unfolding z
_ : x + y + z ≡ 12
_ = refl
마지막으로, 펼침 절은 새로운 레이아웃 문맥을 도입하지 않아서 다음은 합법적이에요. y가 x의 왼쪽에 나타나지만 여전히 같은 펼침 절에 붙어 있다는 점에 주의하세요. 이를 통해 사용자는 펼침 집합을 자신이 선호하는 방식으로 배치할 수 있어요:
opaque
unfolding x
y
unfolding z
_ : x + y + z ≡ 12
_ = refl
다른 정의 뒤에 펼침 절이 나타나거나 불투명 블록 밖에 나타나는 것은 문법 오류예요.
모듈 단위로 취급되는 abstract 블록과 달리 불투명 블록은 위 규칙에 따라서만 이름을 펼친다는 점에 주의하세요:
module _ where private
opaque
x : Nat
x = 3
-- opaque
-- _ : x ≡ 3
-- _ = refl
-- 실패: x != 3 of type Nat
타입에서의 펼침 (Unfolding in types)
펼침 절이 불투명 블록 안의 타입 시그니처에는 적용되지 않는다는 점에 주의하세요. abstract 블록과 마찬가지로 이는 구현 세부 사항의 새어나감을 막지만, 불투명 블록이 정의한 이름의 타입이 불투명 블록 밖에서도 유효하게 유지되도록 보장하는 데도 필요해요. 다음을 생각해 봐요:
opaque
S : Set₁
S = Set
foo′ : S
foo′ = Nat
opaque
unfolding foo′
-- bar′ : foo′
-- bar′ = 123
-- 오류: S는 sort여야 하는데 그렇지 않음
bar′의 정의가 허용된다면 문맥에 bar′ : foo′가 있게 돼요. 관련 불투명 블록 밖에서 foo′는 타입이 아니에요. 그 이유는 foo′ : S이고 S는 sort가 아니기 때문이에요. 이 경우 정렬(sort) 타입을 가진 보조 정의를 사용하는 것이 필요해요:
-- foo′를 정의로 올리기:
ty′ : Set
ty′ = foo′
bar′ : ty′
bar′ = 123
ty′ : Set이 명백히 잘 형성된 타입이므로 이 불투명 블록 밖에서도 bar′ : ty′를 문맥에 추가하는 데 문제가 없어요.
서지 (Bibliography)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, and Lars Birkedal; "Controlling unfolding in type theory".