뷰와 "with" 규칙

뷰와 "with" 규칙 (Views and the "with" rule)

의존 패턴 매칭 (Dependent pattern matching)

타입이 값에 의존할 수 있으므로, 어떤 인자의 형태는 다른 인자의 값에 의해 결정될 수 있어요. 예를 들어 (++)에 암시적 길이 인자를 명시해 적어 본다면, 길이 인자의 형태가 벡터가 비어 있는지 아닌지에 의해 결정된다는 것을 알 수 있어요:

(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) {n=Z}   []        ys = ys
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

[] 경우에 n이 후임자(successor)이거나, :: 경우에 0이면, 그 정의는 잘 타입되지 않을 거예요.

with 규칙 — 중간 값 매칭 (The with rule — matching intermediate values)

매우 자주 중간 계산의 결과에 매치할 필요가 있어요. Idris는 이를 위한 구성물인 with 규칙을 제공해요. 이는 Epigram의 뷰(views) [1]에서 영감을 받았으며, 의존 타입 언어에서 값에 매치하는 것이 다른 값의 형태에 대해 아는 것에 영향을 줄 수 있다는 사실을 반영해요. 가장 단순한 형태에서, with 규칙은 정의되는 함수에 또 다른 인자를 추가해요.

우리는 벡터 필터 함수를 이미 봤어요. 이번에는 with를 사용해 다음과 같이 정의할게요:

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p [] = ( _ ** [] )
filter p (x :: xs) with (filter p xs)
  filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

여기서 with 절은 filter p xs의 결과를 분해(deconstruct)할 수 있게 해줘요. 뷰로 정제된 인자 패턴(view refined argument pattern) filter p (x :: xs)가 with 절 아래에 오고, 그 다음에 세로 막대 |가 오고, 그 다음에 분해된 중간 결과 ( _ ** xs' )가 와요. 뷰로 정제된 인자 패턴이 원래 함수 인자 패턴과 같다면, |의 왼쪽은 불필요하므로 생략할 수 있어요:

filter p (x :: xs) with (filter p xs)
  | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

with 절은 중첩될 수도 있어요:

foo : Int -> Int -> Bool
foo n m with (succ n)
  foo _ m | 2 with (succ m)
    foo _ _ | 2 | 3 = True
    foo _ _ | 2 | _ = False
  foo _ _ | _ = False

중간 계산 자체가 의존 타입을 갖는다면, 그 결과는 다른 인자들의 형태에 영향을 줄 수 있어요 — 하나의 값을 테스트해 다른 값의 형태를 알 수 있어요. 이런 경우 뷰로 정제된 인자 패턴은 명시적이어야 해요. 예를 들어 Nat는 짝수(even)이거나 홀수(odd)예요. 짝수라면 두 개의 같은 Nat의 합이에요. 그렇지 않다면 두 개의 같은 Nat의 합에 1을 더한 것이에요:

data Parity : Nat -> Type where
   Even : Parity (n + n)
   Odd  : Parity (S (n + n))

우리는 Parity가 Nat의 뷰(view)라고 말해요. 그것은 짝수인지 홀수인지를 테스트하고 그에 따라 술어(predicate)를 구성하는 덮개 함수(covering function)를 가져요.

parity : (n:Nat) -> Parity n

parity의 정의로는 잠시 후에 돌아올게요. 그것을 사용해 자연수를 (최하위 자리가 먼저인) 이진 숫자 리스트로 변환하는 함수를 with 규칙을 사용해 다음과 같이 작성할 수 있어요:

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
   natToBin (j + j)     | Even = False :: natToBin j
   natToBin (S (j + j)) | Odd  = True  :: natToBin j

parity k의 값은 k의 형태에 영향을 줘요. 왜냐하면 parity k의 결과가 k에 의존하기 때문이에요. 그래서 |의 오른쪽에 중간 계산 결과에 대한 패턴(Even과 Odd)을 쓰는 것뿐 아니라, 그 결과들이 | 왼쪽의 다른 패턴에 어떻게 영향을 주는지도 써요. 즉:

parity k가 Even으로 평가되면, Even 생성자 정의의 Parity (n + n)에 따라 원래 인자 k를 정제된 패턴 (j + j)으로 정제할 수 있어요. 따라서 (j + j)가 |의 왼쪽에서 k를 대체하고, Even 생성자가 오른쪽에 나타나요. 정제된 패턴의 자연수 j는 = 기호의 오른쪽에서 사용될 수 있어요.
그렇지 않으면, parity k가 Odd로 평가될 때, Odd 생성자 정의의 Parity (S (n + n))에 따라 원래 인자 k가 S (j + j)로 정제되고, Odd가 |의 오른쪽에 나타나며, 다시 = 기호의 오른쪽에서 자연수 j가 사용돼요.

패턴에 함수(+)와 j의 반복 출현이 있다는 점을 유의하세요 — 이것은 다른 인자가 이 패턴들의 형태를 결정했기 때문에 허용돼요.

다음 절 Theorems in Practice에서 parity의 정의를 완성하기 위해 이 함수로 돌아올게요.

with와 증명 (With and proofs)

정리 증명을 위해 의존 패턴 매치를 사용하려면, 때로는 패턴 매치에서 나오는 증명을 명시적으로 구성할 필요가 있어요.

이를 위해 with 절에 proof p를 접미사로 붙일 수 있으며, 패턴 매치가 생성한 증명이 범위 안에 p라는 이름으로 있게 돼요. 예를 들어:

data Foo = FInt Int | FBool Bool

optional : Foo -> Maybe Int
optional (FInt x) = Just x
optional (FBool b) = Nothing

isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))
isFInt foo with (optional foo) proof p
  isFInt foo | Nothing = Nothing           -- here, p : Nothing = optional foo
  isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo

[1]

Conor McBride and James McKinna. 2004. The view from the left. J. Funct. Program. 14, 1 (January 2004), 69-111. https://doi.org/10.1017/S0956796803004829

출처: 문서