With 추상화

With 추상화 (With-Abstraction)

• 사용법 (Usage)
• 일반화 (Generalisation)
• 중첩 with 추상화 (Nested with-abstractions)
• 동시 추상화 (Simultaneous abstraction)
• with 추상화를 숨김/비관련으로 만들기
• 패턴 반복에서 밑줄과 변수 사용하기
• 기각 불가능한 With (Irrefutable With)
• 좌변 let-바인딩 (Left-hand side let-bindings)
• Rewrite
• With-추상화 동등성 (With-abstraction equality)
• With-추상화의 대안 (Alternatives to with-abstraction)
• 종료 검사 (Termination checking)
• 성능 고려 사항 (Performance considerations)
• 기술적 세부사항 (Technical details)
• 예제 (Examples)
• 잘못 타입된 with 추상화 (Ill-typed with-abstractions)

With-추상화는 Conor McBride가 처음 도입했어 [McBride2004]. 함수의 좌변에 인자를 효과적으로 추가해서 중간 계산의 결과를 패턴 매칭할 수 있게 해줘.

사용법 (Usage)

가장 단순한 경우, with 구문은 중간 계산의 결과에 대해 판별하는 데만 사용할 수 있어. 예를 들어:

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
filter p (x ∷ xs)    | true  = x ∷ filter p xs
filter p (x ∷ xs)    | false = filter p xs

with-추상화를 포함한 절은 우변이 없어. 대신 그 뒤에 추가 인자를 좌변에 가진 여러 절이 이어지며, 원래 인자와는 세로 막대(|)로 구분돼.

새 절에서 원래 인자가 같으면 ... 문법을 사용할 수 있어:

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
...                  | true  = x ∷ filter p xs
...                  | false = filter p xs

이 경우 ...은 filter p (x ∷ xs)로 확장돼. 좌변을 풀어 써야 하는 경우는 세 가지야:

• 원래 인자에 대해 더 패턴 매칭을 하고 싶을 때
• 중간 결과에 대한 패턴 매칭이 다른 인자 중 일부를 세분화(refine)할 때 (점 패턴(Dot patterns) 참조)
• 중첩 with 추상화의 절들을 구분할 때 (아래 중첩 with 추상화 참조)

일반화 (Generalisation)

with-추상화의 힘은 목표 타입과 원래 인자들의 타입이 스크루티니(scrutinee)의 값에 대해 일반화된다는 사실에서 나와. 세부사항은 아래 기술적 세부사항을 참조해.

이 일반화는 with를 사용해 정의한 함수에 대한 속성을 증명해야 할 때 중요해. 예를 들어 위 filter 함수가 어떤 속성 P를 만족함을 증명하고 싶다고 하자. 리스트에 대해 패턴 매칭으로 시작하면 다음을 얻게 돼 (구멍 안에 목표 타입이 표시됨):

postulate P : ∀ {A} → List A → Set
postulate p-nil : ∀ {A} → P {A} []
postulate Q : Set
postulate q-nil : Q

proof : {A : Set} (p : A → Bool) (xs : List A) → P (filter p xs)
proof p []       = {! P [] !}
proof p (x ∷ xs) = {! P (filter p (x ∷ xs) | p x) !}

cons 경우에 우리는 filter p (x ∷ xs) | p x에 대해 P가 성립함을 증명해야 해. 이것은 막힌 with-추상화(stuck with-abstraction)의 문법이야 — p x의 값을 모르므로 filter는 축약될 수 없어. 이 문법은 인쇄에 사용되지만 유효한 Agda 코드로는 받아들여지지 않아. 이제 p x에 대해 with-추상화를 하지만 결과에 대해 패턴 매칭은 하지 않으면:

proof : {A : Set} (p : A → Bool) (xs : List A) → P (filter p xs)
proof p [] = p-nil
proof p (x ∷ xs) with p x
...                 | r   = {! P (filter p (x ∷ xs) | r) !}

여기서 목표 타입의 p x는 p x의 결과를 위해 도입된 변수 r로 바뀌었어. r에 대해 패턴 매칭을 하면 with-절들이 축약될 수 있게 돼:

proof : {A : Set} (p : A → Bool) (xs : List A) → P (filter p xs)
proof p [] = p-nil
proof p (x ∷ xs) with p x
...                 | true  = {! P (x ∷ filter p xs) !}
...                 | false = {! P (filter p xs) !}

목표 타입과 다른 인자들의 타입 모두 일반화되므로, 타입에 filter p xs를 포함하는 인자가 있어도 잘 작동해:

proof₂ : {A : Set} (p : A → Bool) (xs : List A) → P (filter p xs) → Q
proof₂ p [] _ = q-nil
proof₂ p (x ∷ xs) H with p x
...                    | true  = {! H : P (x ∷ filter p xs) !}
...                    | false = {! H : P (filter p xs) !}

이 일반화는 다른 with-추상화의 스크루티니로 제한되지 않아. 목표 타입과 인자 타입에서 그 용어의 모든 발생이 일반화돼.

이 일반화가 항상 타입적으로 올바른 것은 아니며 (때로는 난해한) 타입 오류를 일으킬 수 있다는 점에 주의해. 자세한 내용은 아래 잘못 타입된 with 추상화를 참조해.

중첩 with 추상화 (Nested with-abstractions)

With 추상화는 임의로 중첩될 수 있어. 이 경우 유의할 점은 ... 문법이 가장 가까운 with-추상화에 적용된다는 것이야. 예를 들어 아래 정의에서 ...을 사용하고 싶다고 하자:

compare : Nat → Nat → Comparison
compare x y with x < y
compare x y    | false with y < x
compare x y    | false    | false = equal
compare x y    | false    | true  = greater
compare x y    | true = less

모든 with-절에서 compare x y를 ...으로 다음과 같이 바꾸고 싶을 거야:

compare : Nat → Nat → Comparison
compare x y with x < y
...            | false with y < x
...                       | false = equal
...                       | true  = greater
...            | true = less    -- WRONG

그러나 이것은 틀려. 마지막 절에서 ...은 안쪽 with-추상화에 속하는 것으로 해석(공백은 고려되지 않음)되어 compare x y | false | true로 확장돼. 이 경우 좌변을 풀어 써야 해:

compare : Nat → Nat → Comparison
compare x y with x < y
...            | false with y < x
...                       | false = equal
...                       | true  = greater
compare x y    | true = less

동시 추상화 (Simultaneous abstraction)

단일 with-추상화에서 여러 용어에 대해 추상화할 수 있어. 이를 위해 용어를 세로 막대(|)로 구분해:

compare : Nat → Nat → Comparison
compare x y with x < y | y < x
...            | true  | _     = less
...            | _     | true  = greater
...            | false | false = equal

이 예에서 추상화된 용어의 순서는 중요하지 않지만, 일반적으로는 중요해. 구체적으로, 나중 용어의 타입은 앞선 용어의 값에 대해 일반화돼. 예를 들어:

postulate plus-commute : (a b : Nat) → a + b ≡ b + a
postulate P : Nat → Set

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t with a + b | plus-commute a b
thm a b t    | ab    | eq = {! t : P ab, eq : ab ≡ b + a !}

t의 타입과 plus-commute a b의 결과 eq의 타입 모두 a + b에 대해 일반화되었다는 점에 주의해. with-추상화의 용어들이 뒤집히면 그렇지 않게 돼. 이제 eq에 대해 패턴 매칭을 하면:

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t with   a + b  | plus-commute a b
thm a b t    | .(b + a) | refl = {! t : P (b + a) !}

따라서 구멍을 t로 채울 수 있어. 효과적으로 교환법칙 증명을 사용해 t의 타입에서 a + b를 b + a로 재작성한 거야. 이것은 유용한 것이어서 전용 문법이 있어. 아래 Rewrite를 참조해.

일반화의 한계는 추상화 시점에 보이는 용어의 발생만 일반화되지만, 우변을 채우거나 좌에서 더 매칭을 하기 시작하면 더 많은 인스턴스가 나타날 수 있다는 것이야. 예를 들어 q의 타입이 축약되기 위해 f n의 값에 매칭해야 하지만, f n에 대해 이야기하는 보조정리를 q에 적용하고 싶은 다음의 인위적인 예를 생각해 보자:

postulate
  R     : Set
  P     : Nat → Set
  f     : Nat → Nat
  lemma : ∀ n → P (f n) → R

Q : Nat → Set
Q zero    = ⊥
Q (suc n) = P (suc n)

proof : (n : Nat) → Q (f n) → R
proof n q with f n
proof n ()   | zero
proof n q    | suc fn = {! q : P (suc fn) !}

f n에 대해 일반화하면 더 이상 타입 P (f n)의 인자가 필요한 보조정리를 적용할 수 없어. 이 문제를 풀려면 보조정리를 with-추상화에 추가할 수 있어:

proof : (n : Nat) → Q (f n) → R
proof n q with f n    | lemma n
proof n ()   | zero   | _
proof n q    | suc fn | lem = lem q

이 경우 lemma n의 타입(P (f n) → R)이 f n에 대해 일반화되므로 마지막 절의 우변에서 q : P (suc fn)과 lem : P (suc fn) → R을 가지게 돼.

대안적 접근은 아래 With-추상화 동등성을 참조해.

with 추상화를 숨김/비관련으로 만들기 (Making with-abstractions hidden and/or irrelevant)

with 표현식에 숨김(hiding)과 비관련성(relevance) 주석을 추가하는 것이 가능해. 예를 들어:

module _ (A B : Set) (recompute : .B → .{{A}} → B) where

  _$_ : .(A → B) → .A → B
  f $ x with .{f} | .(f x) | .{{x}}
  ... | y = recompute y

이것은 매칭할 필요는 없지만 결과가 잘 타입되기 위해 추상화해야 하는 with-추상화를 숨기는 데 유용할 수 있어. 비관련 필드를 가진 레코드 타입의 필드에 대해 추상화하는 데에도 사용할 수 있어. 예를 들어:

record EqualBools : Set₁ where
  field
    bool1  : Bool
    bool2  : Bool
    .same : bool1 ≡ bool2
open EqualBools

example : EqualBools → EqualBools
example x with bool1 x | bool2 x | .(same x)
...     | true  | y′ | eq′ = record { bool1 = true;  bool2 = y′; same = eq′ }
...     | false | y′ | eq′ = record { bool1 = false; bool2 = y′; same = eq′ }

패턴 반복에서 밑줄과 변수 사용하기 (Using underscores and variables in pattern repetition)

생략표 ...을 사용할 수 없으면, with-절은 부모 절의 패턴을 반복(또는 세분화)해야 해. Agda 2.5.3 이후로는 그런 패턴들이 바인딩하는 변수가 필요하지 않으면 밑줄 _로 대체될 수 있어. 다음은 (약간 인위적인) 예야:

record R : Set where
  coinductive -- disallows matching
  field  f  :  Bool
         n  :  Nat

data P (r : R) : Nat → Set where
  fTrue  :  R.f r ≡ true  →  P r zero
  nSuc   :                   P r (suc (R.n r))

data Q : (b : Bool) (n : Nat) →  Set where
  true!  :             Q true zero
  suc!   :  ∀{b n}  →  Q b (suc n)

test : (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
test  r  nSuc       = suc!
test  r  (fTrue p)  with  R.f r
test  _  (fTrue ())    |  false
test  _  _             |  true  = true!  -- underscore instead of (isTrue _)

Agda 2.5.4 이후로는 패턴이 변수로도 대체될 수 있어:

f : List Nat → List Nat
f [] = []
f (x ∷ xs) with f xs
f xs0 | r = ?

변수 xs0은 값 .x ∷ .xs를 가진 let-바인딩 변수로 취급돼 (여기서 .x : Nat과 .xs : List Nat은 범위 밖). with-추상화가 변수의 타입을 바꿀 수 있으므로, 그런 let-바인딩 변수의 인스턴스화는 with-추상화 후에 다시 타입 검사된다.

기각 불가능한 With (Irrefutable With)

패턴이 기각 불가능(irrefutable)할 때, 전통적인 with 블록 대신 패턴 매칭 with를 사용할 수 있어. 이것은 "제대로 된" with 블록을 쓰기 전에 많은 관찰을 하게 해주는 가벼운 문법이야. 기본적인 기각 불가능 패턴의 예는 pred에 대한 다음 펼침 보조정리에서 볼 수 있어:

pred : Nat → Nat
pred zero    = zero
pred (suc n) = n

NotNull : Nat → Set
NotNull zero    = ⊥ -- false
NotNull (suc n) = ⊤ -- trivially true

pred-correct : ∀ n (pr : NotNull n) → suc (pred n) ≡ n
pred-correct n pr with suc p ← n = refl

위 코드 조각에서 우리는 n이 0과 같을 가능성을 상상할 필요가 없어: Agda는 증명 pr이 그런 경우를 완전히 배제하게 해준다는 것을 감지해.

이런 반전 절(inversion clause)에 사용되는 패턴은 임의일 수 있어. 예를 들어 길이가 0도 1도 아닌 벡터의 두 번째 원소를 뽑아내는 깊은 패턴을 가질 수 있어:

infixr 5 _∷_
data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

second : ∀ {n} {pr : NotNull (pred n)} → Vec A n → A
second vs with (_ ∷ v ∷ _) ← vs = v

위에서 본 동시 추상화의 예를 기억해. 동시 rewrite/패턴 매칭 with는 중첩된 것으로 이해해야 해. 즉, 첫 번째 경우 분석에 의해 도입된 타입 세분화가 다음 것들을 타입 검사하는 데 필요할 수 있어.

다음 예에서 focusAt에서 우리는 suc-+로 먼저 벡터 인자의 타입을 다듬었기 때문에 관심 있는 splitAt을 수행할 수 있어.

suc-+ : ∀ m n → suc m + n ≡ m + suc n
suc-+ zero    n                   = refl
suc-+ (suc m) n rewrite suc-+ m n = refl

infixr 1 _×_
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set _
A × B = Σ A (λ _ → B)

splitAt : ∀ m {n} → Vec A (m + n) → Vec A m × Vec A n
splitAt zero    xs       = ([] , xs)
splitAt (suc m) (x ∷ xs) with (ys , zs) ← splitAt m xs = (x ∷ ys , zs)

-- focusAt m (x₀ ∷ ⋯ ∷ xₘ₋₁ ∷ xₘ ∷ xₘ₊₁ ∷ ⋯ ∷ xₘ₊ₙ)
-- returns ((x₀ ∷ ⋯ ∷ xₘ₋₁) , xₘ , (xₘ₊₁ ∷ ⋯ ∷ xₘ₊ₙ))
focusAt : ∀ m {n} → Vec A (suc (m + n)) → Vec A m × A × Vec A n
focusAt m {n} vs rewrite suc-+ m n
                 with (before , focus ∷ after) ← splitAt m vs
                 = (before , focus , after)

임의로 많은 rewrite와 패턴 매칭 with 절을 번갈아 하고, 필요하면 그 후에도 여전히 with 추상화를 수행할 수 있어.

좌변 let-바인딩 (Left-hand side let-bindings)

기각 불가능한 with의 대안으로, 변수를 바인딩하거나 레코드 값의 단순 언패킹만 하면 될 때는 using-바인딩을 사용할 수 있어. 이것은 let-바인딩의 좌변 대응물이며, 같은 제한된 형태의 패턴 매칭을 지원해.

예를 들어, 위 섹션의 splitAt에 사용된 기각 불가능한 with는 using으로 바꿀 수 있어:

splitAt : ∀ m {n} → Vec A (m + n) → Vec A m × Vec A n
splitAt zero    xs       = ([] , xs)
splitAt (suc m) (x ∷ xs) using (ys , zs) ← splitAt m xs = (x ∷ ys , zs)

using으로 바인딩된 변수는 이후 with 절들에서 범위에 있으므로, 여러 중첩 with에 걸쳐 바인딩을 재사용할 수 있어:

contrived : ∀ m {n} → Vec A (m + n) → (Vec A m → Bool) → (Vec A n → Bool) → Bool
contrived m xs p q using (ys , zs) ← splitAt m xs
                   with p ys
... | true = true
... | false with q zs
...   | true  = false
...   | false = true

편의상, 여러 바인딩은 |로 구분할 수 있고, 이것은 using 키워드를 반복하는 것과 같은 의미를 가져: 왼쪽 바인딩이 오른쪽에 범위 내에 있어.

with와 rewrite와는 달리 using은 바인딩된 용어에 대해 어떤 추상화도 수행하지 않고, 단순히 지역 바인딩을 도입해. 이것은 목표 타입과 맥락이 크고 정규화하기 비싸며 추상화가 필요하지 않은 상황에서 기각 불가능한 with보다 훨씬 저렴하게 사용할 수 있게 해줘.

Rewrite

위의 동시 추상화 예를 기억해:

postulate plus-commute : (a b : Nat) → a + b ≡ b + a

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t with   a + b  | plus-commute a b
thm a b t    | .(b + a) | refl = t

방정식과 그 좌변에 대해 with-추상화함으로써 방정식으로 재작성하는 이 패턴은 충분히 흔해서 전용 문법이 있어:

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t rewrite plus-commute a b = t

rewrite 구문은 타입 lhs ≡ rhs(_≡_는 내장 동등성 타입)의 용어 eq를 받아, lhs와 eq의 with-추상화로 확장한 다음 eq의 결과를 refl에 매칭해:

f ps rewrite eq = v

  -->

f ps with lhs | eq
...    | .rhs | refl = v

rewrite 구문의 한계는 재작성 후에 인자들에 대해 더 이상 패턴 매칭을 할 수 없다는 것이야. 모든 것이 단일 절에서 일어나기 때문이지. 그러나 재작성 후에 with-추상화는 할 수 있어. 예를 들어:

postulate T : Nat → Set

isEven : Nat → Bool
isEven zero = true
isEven (suc zero) = false
isEven (suc (suc n)) = isEven n

thm₁ : (a b : Nat) → T (a + b) → T (b + a)
thm₁ a b t rewrite plus-commute a b with isEven a
thm₁ a b t | true  = t
thm₁ a b t | false = t

rewrite가 도입한 with-추상화된 인자(lhs와 eq)는 코드에서 보이지 않는다는 점에 주의해.

With-추상화 동등성 (With-abstraction equality)

용어 t에 대해 with-추상화를 하면 t와 그것의 값을 나타내는 새 인자 사이의 연결을 잃게 돼. 관심 있는 t의 모든 인스턴스가 추상화에 의해 일반화되는 한 괜찮지만, 위에서 봤듯이 항상 그런 것은 아니야. 그 예에서는 필요한 모든 인스턴스를 잡기 위해 동시 추상화를 사용했어.

그 대안은 Agda가 동등성 증명에서 with 절의 패턴들이 추상화한 표현식에서 나온 것임을 기억하게 하는 것이야. 이것은 in 키워드로 가능해.

다음의 인위적인 예에서 우리는 한 숫자가 다른 숫자의 두 배와 같은 두 숫자가 존재함을 증명하려고 해. 입력 m의 두 배를 계산해서 n이라고 부르자. 그다음 m, n을 포함한 중첩 쌍을 반환할 수 있고, 이제 m + m ≡ n 증명이 필요해. 다행히 n을 m + m으로 계산할 때 in eq를 사용했고 이 eq가 정확히 우리가 필요한 증명이야.

double : Nat → Σ Nat (λ m → Σ Nat (λ n → m + m ≡ n))
double m with n ← m + m in eq = m , n , eq

더 자연스러운 예로, filter(이 페이지 맨 위에서 정의)가 멱등(idempotent)임을 증명한다. 즉, 입력 리스트에 두 번 적용하는 것이 한 번만 적용하는 것과 같다는 것이야.

filter-filter p (x ∷ xs) 경우에서, p x의 결과에 대해 추상화한 다음 매칭하면 첫 번째 filter p (x ∷ xs) 호출이 축약될 수 있어.

원소 x가 유지되는 경우(즉 p x가 true)에, LHS의 두 번째 filter 호출이 같은 p x 검사를 계속 수행해. 우리가 p x ≡ true 증명을 eq에 보존했기 때문에, 이 동등성으로 재작성해서 그것도 축약시킬 수 있어.

이것은 상합치(congruence)와 귀납 가설에 호소해서 증명을 끝낼 수 있을 만큼 충분한 계산을 이끌어 내.

filter-filter : ∀ {A} p (xs : List A) → filter p (filter p xs) ≡ filter p xs
filter-filter p []       = refl
filter-filter p (x ∷ xs) with p x in eq
... | false = filter-filter p xs -- easy
... | true -- second filter stuck on `p x`: rewrite by `eq`!
  rewrite eq = cong (x ∷_) (filter-filter p xs)

With-추상화의 대안 (Alternatives to with-abstraction)

with-추상화는 매우 강력하지만, 쓸 수 없거나 쓰고 싶지 않은 경우가 있어. 예를 들어 우변의 표현식 안에 있으면 with-추상화를 쓸 수 없어. 그런 경우에는 몇 가지 대안이 있어.

패턴 람다 (Pattern lambdas)

Agda에는 원시 case 구문이 없지만, 패턴 람다를 사용해 흉내낼 수 있어. 먼저 case_of_ 함수를 다음과 같이 정의해:

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

그런 다음 이 함수를 두 번째 인자로 패턴 람다와 함께 사용해서 Haskell 스타일의 case 표현식을 얻을 수 있어:

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) =
  case p x of
  λ { true  → x ∷ filter p xs
    ; false → filter p xs
    }

이 case_of_ 버전은 비-의존 함수에만 작동해. 의존 함수의 경우 목표 타입이 대부분의 경우 추론되지 않지만, 명시적 B를 가진 변형을 사용할 수 있어:

case_returning_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
case x returning B of f = f x

의존 버전은 with-추상화처럼 스크루티니에 대해 일반화할 수 있게 해주지만, 수동으로 해야 해. 하지 못하게 하는 두 가지는 좌변의 인자에 대한 더 이상의 패턴 매칭과, case 표현식의 패턴에 의한 좌변 인자 세분화야. 예를 들어 Vec A n에 매칭하면 n이 nil과 cons 패턴에 의해 세분화될 거야.

보조 함수 (Helper functions)

내부적으로 with-추상화는 보조 함수로 번역되고(아래 기술적 세부사항 참조), 그 함수를 항상 직접 작성할 수 있어. 단점은 보조 함수의 타입 시그니처를 명시적으로 써야 한다는 것이지만, 다행히 Emacs 모드에는 with-함수의 타입을 생성하는 것과 같은 알고리즘으로 그것을 생성하는 명령(C-c C-h)이 있어.

종료 검사 (Termination checking)

종료 검사기는 번역된 보조 함수들에 대해 실행되므로, 종료 검사를 통과할 것처럼 보이는 일부 코드가 실제로는 통과하지 못해. 구체적으로 c₁ (c₂ x) ⟶ c₁ x 같은 호출 사슬에서 재귀 호출이 with-추상화 아래에 있을 때 그렇지. 이유는 보조 함수가 x만 받기 때문에 실제 호출 사슬은 c₁ (c₂ x) ⟶ x ⟶ c₁ x이고, 종료 검사기가 이것이 종료함을 볼 수 없기 때문이야. 예를 들어:

data D : Set where
  [_] : Nat → D

fails : D → Nat
fails [ zero  ] = zero
fails [ suc n ] with some-stuff
... | _ = fails [ n ]

이 문제를 우회하는 가장 쉬운 방법은 미리 재귀 호출에 대해 with-추상화를 수행하는 것이야:

fixed : D → Nat
fixed [ zero  ] = zero
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ = rec

함수가 더 많은 인자를 받으면 구조적으로 재귀적인 인자에 대한 부분 적용에 대해 추상화해야 할 수도 있어. 예를 들어,

fails : Nat → D → Nat
fails _ [ zero  ] = zero
fails _ [ suc n ] with some-stuff
... | m = fails m [ n ]

fixed : Nat → D → Nat
fixed _ [ zero  ] = zero
fixed _ [ suc n ] with (λ m → fixed m [ n ]) | some-stuff
... | rec | m = rec m

가능한 합병증은 이후의 with-추상화가 추상화된 재귀 호출의 타입을 바꿀 수 있다는 것이야:

T      : D → Set
suc-T  : ∀ {n} → T [ n ] → T [ suc n ]
zero-T : T [ zero ]

fails : (d : D) → T d
fails [ zero  ] = zero-T
fails [ suc n ] with some-stuff
... | _ with [ n ]
...   | z = suc-T (fails [ n ])

이전처럼 재귀 호출에 대해 추상화하려는 것은 이 경우 작동하지 않아.

still-fails : (d : D) → T d
still-fails [ zero ] = zero-T
still-fails [ suc n ] with still-fails [ n ] | some-stuff
... | rec | _ with [ n ]
...   | z = suc-T rec -- Type error because rec : T z

문제를 풀려면 그 타입을 망치는 with-추상화에 rec을 추가할 수 있어. 이렇게 하면 그 타입이 바뀌는 것을 막을 수 있어:

fixed : (d : D) → T d
fixed [ zero ] = zero-T
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ with rec | [ n ]
...   | _ | z = suc-T rec

성능 고려 사항 (Performance considerations)

with-추상화의 일반화 단계는 스크루티니의 모든 인스턴스가 일반화되도록 하기 위해 스크루티니와 목표 타입 및 인자 타입을 정규화해야 해. 일반화는 타입이 틀리지 않았는지 확인하기 위해 타입 검사도 해야 돼. 이것은 다음과 같은 경우 with-추상화 타입 검사에 비용이 들게 해:

• 정규화가 비쌀 때
• 정규화된 목표 및 인자 타입이 커서 스크루티니의 인스턴스를 찾는 것이 비쌀 때
• 타입이 커서 일반화 타입 검사가 비싸거나, 검사가 무거운 계산을 수반할 때

이런 경우 위의 with-추상화 대안을 살펴볼 가치가 있어.

기술적 세부사항 (Technical details)

내부적으로 with-추상화는 보조 함수로 번역돼 — Core 언어에는 with-추상화가 없어. 이 번역은 다음과 같이 진행돼. with-추상화가 주어지면

• 스크루티니들의 타입을 추론해.
• 맥락을 Δ₁과 Δ₂로 분할해. 여기서 Δ₁은 모든 tᵢ에 대해 스크루티니들이 잘 타입되는 가장 작은 맥락이야.
• 분할이 split일 필요는 없다는 점에 주의해. Δ₂는 Δ₁의 (잘 형성된) 재배열일 수 있어.
• tᵢ들에 대해 일반화해, tᵢ의 정규형이 x들을 포함하지 않도록 Δ₁ → Set의 타입을 계산해. 보조 함수의 타입은 그 후에야 결정돼.
• 일반화가 타입적으로 올바른지 확인해 (아래 참조, 보장되지 않음).
• f와 상호 재귀적인 함수 f'를 정의를 가지고 추가해. 여기서 패턴들은 Δ₂의 변수에 대응하는 f의 패턴들이야. Δ₁과 Δ₂로의 분할의 가능한 재배열로 인해 패턴들이 어떻게 나타나는지와 다른 순서일 수 있다는 점에 주의해.
• with-추상화를 f' 호출로 대체해 최종 정의를 만들어. 여기서 변수들은 각각 대응하는 인자들이야.

예제 (Examples)

아래는 몇 가지 with-추상화와 그 번역의 예야.

postulate
   A     : Set
   _+_   : A → A → A
   T     : A → Set
   mkT   : ∀ x → T x
   P     : ∀ x → T x → Set

-- the type A of the with argument has no free variables, so the with
-- argument will come first
f₁ : (x y : A) (t : T (x + y)) → T (x + y)
f₁ x y t with x + y
f₁ x y t    | w = {!!}

-- Generated with function
f-aux₁ : (w : A) (x y : A) (t : T w) → T w
f-aux₁ w x y t = {!!}

-- x and p are not needed to type the with argument, so the context
-- is reordered with only y before the with argument
f₂ : (x y : A) (p : P y (mkT y)) → P y (mkT y)
f₂ x y p with mkT y
f₂ x y p    | w = {!!}

f-aux₂ : (y : A) (w : T y) (x : A) (p : P y w) → P y w
f-aux₂ y w x p = {!!}

postulate
  H : ∀ x y → T (x + y) → Set

-- Multiple with arguments are always inserted together, so in this case
-- t ends up on the left since it’s needed to type h and thus x + y isn’t
-- abstracted from the type of t
f₃ : (x y : A) (t : T (x + y)) (h : H x y t) → T (x + y)
f₃ x y t h with x + y | h
f₃ x y t h    | w₁    | w₂ = {! t : T (x + y), goal : T w₁ !}

f-aux₃ : (x y : A) (t : T (x + y)) (h : H x y t) (w₁ : A) (w₂ : H x y t) → T w₁
f-aux₃ x y t h w₁ w₂ = {!!}

-- But earlier with arguments are abstracted from the types of later ones
f₄ : (x y : A) (t : T (x + y)) → T (x + y)
f₄ x y t with x + y | t
f₄ x y t    | w₁    | w₂ = {! t : T (x + y), w₂ : T w₁, goal : T w₁ !}

f-aux₄ : (x y : A) (t : T (x + y)) (w₁ : A) (w₂ : T w₁) → T w₁
f-aux₄ x y t w₁ w₂ = {!!}

-- With-abstraction equality
g : (x : A) → T x
g x with mkT x in eq
g x | w = {!!}

g-aux : (x : A) (w : T x) → mkT x ≡ w → T x
g-aux x w eq = {!!}

-- The equality argument is generalised over by further with-abstractions
g₁ : (x : A) → P x (g x)
g₁ x with mkT x in eq
g₁ x | w = {!!}

g-aux₁ : (x : A) (w : T x) (eq : mkT x ≡ w) → P x (g-aux x w eq)
g-aux₁ x w eq = {!!}

잘못 타입된 with 추상화 (Ill-typed with-abstractions)

위에서 언급했듯이, 일반화가 항상 잘 타입된 결과를 만들어내는 것은 아니야. 이것은 목표나 인자 타입의 부분식의 타입에 나타나는 용어에 대해 추상화할 때 발생해. 가장 단순한 예는 의존 쌍의 첫 번째 성분에 대해 추상화하는 것이야. 예를 들어:

postulate
  A : Set
  B : A → Set
  H : (x : A) → B x → Set

bad-with : (p : Σ A B) → H (fst p) (snd p)
bad-with p with fst p
...           | _ = {!!}

여기서 fst p에 대해 일반화하면 잘못 타입된 적용 H w (snd p)가 생기고 다음 타입 오류를 얻게 돼:

fst p != w of type A
when checking that the type (p : Σ A B) (w : A) → H w (snd p) of
the generated with function is well-formed

이 메시지는 즉각적인 문제(fst p != w)와 with-함수의 전체 타입만 인쇄하므로 해석하기 다소 어려울 수 있어. 오류가 발생한 타입의 위치를 가리키는 더 정보가 많은 오류를 얻으려면, 오류 메시지에서 with-함수 타입을 복사해서 별도로 타입 검사해 볼 수 있어.

[McBride2004] C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 2004. http://strictlypositive.org/vfl.pdf.

더 알아보기 (Learn more)

• Agda 문서: with-abstraction 원문