로컬 정의: let과 where
로컬 정의: let과 where (Local Definitions: let and where)
Agda에서 로컬 정의를 선언하는 방법은 두 가지가 있어요:
- let-표현식 (let-expressions)
- where-블록 (where-blocks)
let-표현식 (let-expressions)
let-표현식은 약어(abbreviation)를 정의해요. 이는 let으로 바인딩된 함수가 순수 람다 표현식으로서 말이 되어야 한다는 뜻이에요: 즉 재귀적일 수 없고, 귀납적 타입에 대한 패턴 매칭으로 정의될 수 없어요.
예제:
f : Nat
f = let h : Nat → Nat
h m = suc (suc m)
in h zero + h (suc zero)
하지만 아래에 설명된 대로 let으로 바인딩된 함수의 왼쪽 변에서 레코드 타입에 매칭하는 것은 가능해요:
g : Nat
g = let h : Nat × Nat → Nat
h (x , y) = x + y
in h (1 , 2)
let-표현식은 일반적으로 다음 형태를 가져요:
let f₁ : A₁₁ → … → A₁ₙ → A₁
f₁ x₁ … xₙ = e₁
…
fₘ : Aₘ₁ → … → Aₘₖ → Aₘ
fₘ x₁ … xₖ = eₘ
in e’
여기서 이전 정의는 이후 정의에서 스코프에 있어요. Agda가 추론할 수 있으면 타입 시그니처는 생략할 수 있어요.
타입 체킹 후, 이것의 의미는 단순히 치환 e’[f₁ := λ x₁ … xₙ → e; …; fₘ := λ x₁ … xₖ → eₘ]이에요. Agda는 let 바인딩을 치환해 버리므로, 그것들은 Agda가 출력하는 항이나 대화형 모드의 목표 표시에 나타나지 않아요.
경고: Agda가 사용하는 내부 문법에는 let-표현식이 구성체로 없어요. 그 결과 Agda는 타입 체킹 중 모든 let 바인딩 변수를 인라인해요. 특히 let 바인딩은 공유(sharing)를 도입하는 데 사용될 수 없어요.
레코드 패턴 let 바인딩 (Let binding record patterns)
레코드에 대해
record R : Set where
constructor c
field
f : X
g : Y
h : Z
다음 형태의 let 표현식은
let (c x y z) = t
in u
내부적으로 다음과 같이 번역돼요:
let x = f t
y = g t
z = h t
in u
이것은 R이 공유도(coinductive)로 선언되면 허용되지 않아요. R이 예를 들어 no-eta-equality로 선언되어서 eta-동등이 없으면 ShouldBeEtaRecordPattern 경고가 발생해요 (Agda 2.9.0부터).
로컬로 모듈 열기 (Let expressions)
let-표현식은 모듈을 로컬로 여는 데 사용될 수 있어요. 예를 들어:
let z = x + y
open M z
in u -- M의 정의 사용
where-블록 (where-blocks)
where-블록은 임의의 로컬 정의를 지원하므로 let-표현식보다 훨씬 더 강력해요. where는 어떤 함수 절(clause)에도 붙을 수 있어요.
where-블록은 일반적으로 다음 형태를 가져요:
clause
where
decls
또는
clause
module M where
decls
단순한 예는:
g ps = e
where
f : A₁ → … → Aₙ → A
f p₁₁ … p₁ₙ= e₁
…
…
f pₘ₁ … pₘₙ= eₘ
여기서 pᵢⱼ는 해당 타입의 패턴이고 eᵢ는 f의 발생을 포함할 수 있는 표현식이에요. where-표현식으로 정의된 함수는 패턴 매칭에 의한 일반 정의 규칙을 따라야 해요.
예제:
reverse : {A : Set} → List A → List A
reverse {A} xs = rev-append xs []
where
rev-append : List A → List A → List A
rev-append [] ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)
변수 스코프 (Variable scope)
where-블록의 부모 절(clause)의 패턴 변수는 스코프에 있어요; 이전 예에서 그것들은 A와 xs예요. 부모 절의 타입 시그니처로 바인딩된 변수는 스코프에 없어요. 이것이 숨은 바인더 {A}를 추가한 이유예요.
로컬 선언의 스코프 (Scope of the local declarations)
where-정의는 그것을 소유한 절(부모 절) 밖에서는 보이지 않아요. where-블록에 이름이 주어졌다면(모듈 M where 형태), 모듈 M이 부모 절 밖에서도 보이므로 정의는 M으로 한정되어 사용 가능해요. 익명 모듈의 특수한 형태(module _ where)는 부모 절 밖에서도 한정 없이 정의를 보이게 해요.
이름 있는 where-블록(module M where 형태)의 부모 함수가 private이면 모듈 M도 private이에요. 하지만 M 내부의 선언은 명시적으로 선언되지 않는 한 private이 아니에요. 따라서 다음 예제는 스코프 검사를 통과해요:
module Parent₁ where
private
parent = local
module Private where
local = Set
module Public = Private
test₁ = Parent₁.Public.local
마찬가지로 부모 함수에 대한 private 선언은 module _ where-블록 아래에 정의된 로컬 함수의 비공개에 영향을 주지 않아요:
module Parent₂ where
private
parent = local
module _ where
local = Set
test₂ = Parent₂.local
하지만 명시적으로 private으로 선언할 수는 있어요:
module Parent₃ where
parent = local
module _ where
private
local = Set
이제 Parent₃.local은 스코프에 없어요.
일반적인 where-블록의 부모에 대한 private 선언은 물론 로컬 정의에 영향을 주지 않아요. 그것들은 심지어 스코프에 있지도 않아요.
with나 rewrite 아래의 이름 있는 where-모듈 금지 (No named where-modules under with or rewrite)
Agda 2.9.0부터 with, rewrite, 또는 with p ← e를 통한 with-추상화를 사용하는 절은 이름 있는 where-모듈을 달 수 없어요. 다음은 NamedWhereModuleUnderWith 오류로 거부돼요:
f : Bool → Bool
f x with x
... | true = local
module M where -- Agda 2.9.0부터 거부됨
local = false
... | false = true
그 이유는 with-추상화가 M이 부모 모듈로부터 상속하는 모듈 매개변수의 타입을 바꿀 수 있기 때문이에요. 하지만 이 바뀐 매개변수는 소스 코드에서 보이지 않아서 혼동을 줄 수 있어요. 변경을 무시하는 것, 즉 원래 부모 모듈에서 상속된 모듈 매개변수로 M을 절 밖에서 사용 가능하게 만드는 것은 심지어 불일치로 이어져요.
일반적인 익명 where-블록은 이 제한의 영향을 받지 않고, with-추상화를 하지 않고 let 바인딩을 도입하는 using p ← e도 마찬가지예요:
ok : Bool → Bool
ok x with x
... | true = local
where
local = false
... | false = true
ok' : Bool → Bool
ok' x using y ← x = local
module M' where
local = y
절 밖에서 로컬 정의를 참조해야 한다면, 그것들을 적절한 모듈에 정의하거나 with-추상화를 헬퍼 함수로 옮겨야 해요.
속성 증명하기 (Proving properties)
때때로 부모 함수에 대한 증명에서 로컬 정의를 참조해야 할 때가 있어요. 이 경우 module ⋯ where 변형이 바람직해요.
reverse : {A : Set} → List A → List A
reverse {A} xs = rev-append xs []
module Rev where
rev-append : List A → List A → List A
rev-append [] ys = ys
rev-append (x :: xs) ys = rev-append xs (x :: ys)
이것은 로컬 함수에 다음과 같이 접근하게 해줘요:
Rev.rev-append : {A : Set} (xs : List A) → List A → List A → List A
대안으로, 우리가 작업 중인 모듈에 로컬 함수를 private으로 정의할 수 있어요; 그러면 이 모듈을 임포트하는 어떤 모듈에서도 보이지 않지만, 그것들에 대한 어떤 속성은 증명할 수 있게 해줘요.
private
rev-append : {A : Set} → List A → List A → List A
rev-append [] ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)
reverse' : {A : Set} → List A → List A
reverse' xs = rev-append xs []
더 많은 예제 (초보자용) (More Examples (for Beginners))
let-표현식 사용:
tw-map : {A : Set} → List A → List (List A)
tw-map {A} xs = let twice : List A → List A
twice xs = xs ++ xs
in map (\ x → twice [ x ]) xs
타입 정보를 덜 넣은 같은 정의:
tw-map' : {A : Set} → List A → List (List A)
tw-map' {A} xs = let twice : _
twice xs = xs ++ xs
in map (\ x → twice [ x ]) xs
where-표현식을 사용한 같은 정의:
tw-map'' : {A : Set} → List A → List (List A)
tw-map'' {A} xs = map (\ x → twice [ x ]) xs
where twice : List A → List A
twice xs = xs ++ xs
let을 사용한 더 적은 타입 정보:
h : Nat → List Nat
h zero = [ zero ]
h (suc n) = let sing = [ suc n ]
in sing ++ h n
where를 사용한 같은 정의:
h' : Nat → List Nat
h' zero = [ zero ]
h' (suc n) = sing ++ h' n
where sing = [ suc n ]
let의 여러 정의:
i : Nat → Nat
i n = let add2 : Nat
add2 = suc (suc n)
twice : Nat → Nat
twice m = m * m
in twice add2
where의 여러 정의:
fibfact : Nat → Nat
fibfact n = fib n + fact n
where fib : Nat → Nat
fib zero = suc zero
fib (suc zero) = suc zero
fib (suc (suc n)) = fib (suc n) + fib n
fact : Nat → Nat
fact zero = suc zero
fact (suc n) = suc n * fact n
let과 where 결합:
k : Nat → Nat
k n = let aux : Nat → Nat
aux m = pred (i m) + fibfact m
in aux (pred n)
where pred : Nat → Nat
pred zero = zero
pred (suc m) = m