텔레스코프
텔레스코프 (Telescopes)
텔레스코프는 각 변수가 괄호로 둘러싸인, 타입으로 주석된 변수 바인딩의 비어 있지 않은 수열이에요.
예를 들어 (x : Nat) (y : Bool) (z : Bool)은 텔레스코프예요. 타입이 같은 인접 변수는 타입 주석을 공유할 수 있어요. 예를 들어 같은 텔레스코프를 동등하게 (x : Nat) (y z : Bool)로 쓸 수 있어요.
각 변수의 타입은 텔레스코프의 이전 변수에 의존할 수 있어요. 예를 들어 (A : Set) (n : Nat) (v : Vec A n).
참고: 이 용어는 de Bruijn [1]에서 유래했어요: "물론 이 단어는 서로 미끄러져 들어가는 세그먼트로 이루어진 구식 도구에서 영감을 받았다." 각 변수 바인딩은 텔레스코프의 한 세그먼트에 해당하며, 이전 세그먼트로 미끄러져 들어갈(즉 의존할) 수 있어요.
텔레스코프는 Agda 문법의 다음 부분에 나타나요:
- 함수 타입
- 데이터 타입과 레코드 타입의 선언
- 매개변수화 모듈의 선언
postulate
f : (A : Set) (n : Nat) (v : Vec A n) → Nat
data D (A : Set) (n : Nat) (v : Vec A n) : Set where
-- ...
module M (A : Set) (n : Nat) (v : Vec A n) where
-- ...
데이터 타입과 레코드 타입 및 매개변수화 모듈의 텔레스코프에서는 변수 바인딩의 타입을 생략하는 것이 허용돼요. 이는 변수에 _ 타입을 주는 것과 동등해요 (암시 인자 참고).
data D' A n (v : Vec A n) : Set where
-- ...
module M' A n (v : Vec A n) where
-- ...
함수 타입에서는 모듈 텔레스코프가 forall 또는 ∀로 시작하면 변수 바인딩의 타입을 생략할 수 있어요.
postulate
f' : ∀ A n (v : Vec A n) → Nat
레코드 타입(데이터 타입은 아님)의 변수를 바인딩할 때, 바인딩된 변수를 패턴 매칭으로 분해하는 것이 가능해요:
module N ((x , y) : Nat × Bool) where
-- ...
텔레스코프의 변수 바인딩은 암시적 또는 instance 인자일 수 있어요. 예를 들어:
postulate
mconcat : {A : Set} {{monoidA : Monoid A}} → List A → A
또한 비관련(irrelevant)이거나 다른 모달리티를 가질 수 있어요. 예를 들어:
postulate
div : (m n : Nat) .(nz : NonZero n) → Nat
바인딩 위치에서의 부조리 불가 패턴 (Irrefutable Patterns in Binding Positions)
Agda 2.6.1부터, 텔레스코프의 모든 바인딩 자리에서 부조리 불가(irrefutable) 패턴을 사용해 레코드 타입의 바인딩된 값을 분해할 수 있어요. 의존 쌍의 두 번째 projection의 타입은 예를 들어 자연스럽게 첫 번째 projection의 값을 언급해요. 그 타입은 부조리 불가 패턴을 사용해 직접 정의할 수 있어요:
proj₂ : ((a , _) : Σ A B) → B a
그리고 이 두 번째 projection은 쌍을 분해하는 이런 부조리 불가 패턴 중 하나를 사용한 람다 추상화로 구현할 수 있어요:
proj₂ = λ (_ , b) → b
as-패턴을 사용하면 인자에 이름을 붙이면서 동시에 분해할 수 있어요. 예를 들어 임의의 쌍이 첫 번째와 두 번째 projection의 쌍과 같다는 것, 즉 일반적으로 eta-equality라고 불리는 속성을 증명할 수 있어요:
eta : (p@(a , b) : Σ A B) → p ≡ (a , b)
eta p = refl
Agda 2.9.0부터, 부조리 불가 패턴은 분해된 레코드가 eta-equality를 가질 것을 요구해요. Σ는 그렇지만, 예를 들어 공유도 레코드나 no-eta-equality로 선언된 레코드는 그렇지 않아요. eta-equality가 없으면 부조리 불가 패턴은 ShouldBeEtaRecordPattern 경고를 촉발해요.
텔레스코프에서의 Let 바인딩 (Let Bindings in Telescopes)
함수 타입과 매개변수화 모듈(데이터 타입과 레코드 타입은 아님)의 텔레스코프는 let 바인딩도 포함할 수 있어요. 이런 방식으로 사용될 때 let-바인딩은 괄호로 둘러싸여야 하고 문법의 in 부분은 생략돼요. 예를 들어:
postulate
g : (x : Nat) (let y = x + x) (v : Vec Nat y) → Nat
모듈 텔레스코프의 let-바인딩된 변수는 전체 모듈에서 사용할 수 있어요. 예를 들어:
module O (X : Set) (let LX = List X) (l : LX) where
extend : LX → LX
extend m = l ++ m
일반적으로 유효한 let-바인딩은 텔레스코프에서도 사용할 수 있어요. 예를 들어 let-바인딩으로 레코드 타입에 패턴 매칭하는 것이 가능해요:
postulate
h : (f : Nat → (Bool × Bool)) (let (x0 , y0) = f 0) (tx : IsTrue x0) → IsTrue y0
또 다른 주목할 만한 예는 텔레스코프에서 모듈을 여는 것이에요:
module M1 (X : Set) (let open M X) where
이것은 let 없이 그냥 open으로 더 간결하게 쓸 수도 있어요:
module M2 (X : Set) (open M X) where
참고 문헌 (References)
[1] N.G. de Bruijn. "Telescopic mappings in typed lambda calculus." Information and Computation, Volume 91, Issue 2, 1991.