커버리지 검사

커버리지 검사 (Coverage Checking)

패턴 매칭에 의한 정의의 완전성을 보장하기 위해, Agda는 각 패턴 매칭 정의에 대해 커버리지 검사(coverage check)를 수행해요. 이 페이지는 단순한 예제에서 시작해 일반적인 경우로 확장하면서 이 커버리지 검사가 어떻게 작동하는지 설명할게요.

인덱스되지 않은 데이터 타입에 대한 단일 매칭 (Single match on a non-indexed datatype)

함수 정의가 단순한(즉 인덱스되지 않은) 데이터 타입의 단일 인자에 패턴 매칭할 때, 각 생성자에 대한 절(clause)이 있어야 해요. 예를 들어:

data TrafficLight : Set where
  red yellow green : TrafficLight

go : TrafficLight → Bool
go red    = false
go yellow = false
go green  = true

대안으로, 하나 이상의 경우를 변수 패턴이나 와일드카드 패턴 _을 사용하는 catchall 절로 대체할 수 있어요. 이 경우 catchall 절이 마지막이어야 해요.

go' : TrafficLight → Bool
go' green = true
go' _     = false

참고: -exact-split 플래그가 활성화되면 catchall 절은 catchall 프래그마({-# CATCHALL #-})로 명시적으로 표시되어야 해요.

개별 정의에 대해 타입 시그니처 바로 앞에 {-# NON_COVERING #-} 프래그마를 두면 커버리지 검사를 끌 수 있어요.

{-# NON_COVERING #-}
go'' : TrafficLight → Bool
go'' red   = false
go'' green = true

생성자가 없는 데이터 타입(즉 빈 타입)의 특별한 경우에는 부정 패턴 ()과 오른쪽 변이 없는 단일 부정 절(absurd clause)이 있어야 해요.

data ⊥ : Set where
  -- no constructors

magic : {A : Set} → ⊥ → A
magic ()

여러 인자에 대한 매칭 (Matching on multiple arguments)

함수가 여러 인자에 매칭하면 생성자 조합의 각 가능한 경우가 있어야 해요.

sameColor : TrafficLight → TrafficLight → Bool
sameColor red    red    = true
sameColor red    yellow = false
sameColor red    green  = false
sameColor yellow red    = false
sameColor yellow yellow = true
sameColor yellow green  = false
sameColor green  red    = false
sameColor green  yellow = false
sameColor green  green  = true

다시, 하나 이상의 경우를 catchall 절로 대체할 수 있어요.

sameColor' : TrafficLight → TrafficLight → Bool
sameColor' red    red    = true
sameColor' yellow yellow = true
sameColor' green  green  = true
sameColor' _      _      = false

코패턴 매칭 (Copattern matching)

레코드 타입의 원소를 반환하는 함수는 개별 필드를 주기 위해 코패턴을 사용할 수 있어요. 커버리지 검사는 레코드 타입의 각 필드에 대해 하나의 경우가 있는지 보장해요. 예를 들어:

record Person : Set where
  field
    name : String
    age  : Nat
open Person

bob : Person
name bob = "Bob"
age  bob = 25

부정 코패턴이나 와일드카드 코패턴은 지원되지 않아요.

인덱스된 데이터 타입에 대한 매칭 (Matching on indexed datatypes)

함수 정의가 인덱스된 데이터 타입의 인자에 매칭할 때 다음 조건이 만족되어야 해요:

• 생성자 패턴 c u₁ … uₙ에 매칭하는 각 절에 대해, 패턴 타입의 인덱스는 매칭되는 데이터 타입의 인덱스와 통일 가능해야 해요.
• 절에 나타나지 않는 각 생성자 c에 대해, 생성자 타입의 인덱스와 데이터 타입의 인덱스의 통일은 충돌로 끝나야 해요.

예를 들어 벡터의 head 함수 정의를 생각해 봐요:

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

head : ∀ {A m} → Vec A (suc m) → A
head (x ∷ xs) = x

패턴 x ∷ xs의 타입은 Vec A (suc n)으로, 타입 Vec A (suc m)과 통일 가능해요. 한편 생성자 []의 타입 Vec A 0과 타입 Vec A (suc n)의 통일은 0과 suc n 사이의 충돌로 끝나므로 []에 대한 경우는 없어요.

함수가 여러 인자에 매칭하고 그 중 하나 이상이 인덱스된 데이터 타입일 때, 인덱스가 충돌로 이어지지 않는 인자 조합만 고려해야 해요. 예를 들어 벡터의 zipWith 함수를 생각해 봐요:

zipWith : ∀ {A B C m} → (A → B → C) → Vec A m → Vec B m → Vec C m
zipWith f []       []       = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

두 입력 벡터의 길이가 같으므로(둘 다 m), 한 벡터의 길이가 0이고 다른 벡터의 길이가 suc n인 조합에 대한 경우는 없어요.

모든 생성자에 대해 통일이 충돌로 끝나는 특별한 경우에는 (빈 타입처럼) 단일 부정 절이 있어야 해요. 예를 들어:

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

no-fin-zero : Fin 0 → ⊥
no-fin-zero ()

많은 일반적인 경우에는 남은 절들이 케이스 분할할 인자를 나타낼 충분한 정보를 드러내기만 하면 부정 절을 생략할 수 있어요. 예를 들어 벡터의 lookup 함수 정의를 생각해 봐요:

lookup : ∀ {A} {n} → Vec A n → Fin n → A
lookup []       ()
lookup (x ∷ xs) zero    = x
lookup (x ∷ xs) (suc i) = lookup xs i

이 정의는 부정 절과 두 일반 절 모두에서 (명시적) 인자 두 개 모두에 패턴 매칭해요. 따라서 정의에서 부정 절을 빼는 것이 허용돼요:

lookup' : ∀ {A} {n} → Vec A n → Fin n → A
lookup' (x ∷ xs) zero    = x
lookup' (x ∷ xs) (suc i) = lookup' xs i

부정 절을 언제 생략할 수 있는지에 대한 정확한 설명은 다음 섹션을 참고하세요.

일반적인 경우 (General case)

일반적인 경우에 커버리지 검사기는 사용자가 준 정의에서 케이스 트리(case tree)를 구성해요. 그런 다음 다음 속성들이 만족되는지 보장해요:

• 정의의 비-부정 절은 케이스 트리의 잎으로 나타나야 해요.
• 정의의 부정 절은 자식이 없는 케이스 트리의 내부 노드로 나타나야 해요.
• 대응하는 내부 노드를 케이스 트리에서 제거해도 다른 내부 노드가 무자식이 되지 않으면 부정 절을 생략할 수 있어요.
• 비-부정 절은 다음 조건에서 catchall 절로 대체될 수 있어요: (1) 그 catchall 절의 패턴이 생략된 절보다 더 일반적이고, (2) 추가된 catchall 절이 뒤따르는 어떤 절보다 더 일반적이지 않으며, (3) 생략된 절에 대응하는 잎을 제거해도 어떤 내부 노드가 무자식이 되지 않는다.

예를 들어 위에서 정의한 lookup 함수의 케이스 트리를 생각해 봐요:

lookup xs i = case xs of
  []       → case i of {}
  (x ∷ xs) → case i of
    zero    → x
    (suc i) → lookup xs i

부정 절은 xs = []인 가지에서 i에 대한 케이스 분할에서 발생하며, 이는 zero 케이스로 이어져요. 두 일반 절은 케이스 트리의 두 잎에서 발생해요. 케이스 [] → case i of {}를 케이스 트리에서 제거하면 남은 모든 내부 노드가 여전히 적어도 하나의 자식을 가지므로 부정 절을 정의에서 뺄 수 있어요.

Agda가 케이스 트리를 구성하고 패턴 매칭 정의의 커버리지를 검사하는 데 사용하는 알고리즘의 완전한 형식적 설명은 'Elaborating dependent (co)pattern matching: No pattern left behind' 논문을 참고하세요.

더 알아보기 (Learn more)

• Agda 문서: 커버리지 검사 원문