함수 정의

함수 정의 (Function Definitions)

소개 (Introduction)

함수는 먼저 타입을 선언한 다음 절(clause)이라고 불리는 여러 방정식을 나열함으로써 정의돼요. 각 절은 정의 중인 함수를 여러 패턴에 적용한 것으로 구성되고, 그 뒤에 =와 오른쪽 변(right-hand side)이라 불리는 항이 따라와요. 예를 들어:

not : Bool → Bool
not true  = false
not false = true

함수는 스스로를 재귀적으로 호출하는 것이 허용돼요. 예를 들어:

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

일반 형태 (General form)

함수를 정의하는 일반적인 형태는 다음과 같아요:

f : (x₁ : A₁) → … → (xₙ : Aₙ) → B
f p₁ … pₙ = d
…
f q₁ … qₙ = e

여기서 f는 새 식별자이고, pᵢ와 qᵢ는 타입 Aᵢ의 패턴이며, d와 e는 표현식이에요.

위 선언은 식별자 f에 타입 (x₁ : A₁) → … → (xₙ : Aₙ) → B를 부여하고, f는 정의 방정식으로 정의돼요. 패턴은 위에서 아래로 매칭되는데, 즉 실제 매개변수와 매칭되는 첫 번째 패턴이 사용돼요.

기본적으로 Agda는 함수 정의의 다음 속성들을 검사해요:

  • 각 절의 왼쪽 변의 패턴은 생성자와 변수로만 구성되어야 해요.
  • 어떤 변수도 단일 절의 왼쪽 변에 두 번 이상 나타나면 안 돼요.
  • 모든 절의 패턴은 함수의 모든 가능한 입력을 함께 덮어야 해요 (커버리지 검사 참고).
  • 함수는 모든 가능한 입력에 대해 종료해야 해요 (종료 검사 참고).

특수 패턴 (Special patterns)

생성자와 변수로 구성된 것에 더해 Agda는 두 가지 특수한 종류의 패턴, 즉 점 패턴(dot pattern)과 부정 패턴(absurd pattern)을 지원해요.

점 패턴 (Dot patterns)

점 패턴(접근 불가 패턴이라고도 함)은 인자의 유일한 타입-정확 값이 다른 인자들에 대해 주어진 패턴에 의해 결정될 때 사용할 수 있어요.

점 패턴은 함수 호출의 결과를 결정하기 위해 매칭되지 않아요. 대신 다른 패턴들에 의해 결정되는 해당 위치의 유일한 가능한 값에 대한 검사된 문서 역할을 해요.

점 패턴의 문법은 .t예요.

예를 들어 다음과 같이 정의된 데이터 타입 Square를 생각해 봐요:

data Square : Nat → Set where
  sq : (m : Nat) → Square (m * m)

숫자 n과 그것이 제곱수라는 증명을 인자로 받아 그 숫자의 제곱근을 반환하는 함수 root : (n : Nat) → Square n → Nat을 정의하고 싶다고 가정해 봐요. 다음과 같이 할 수 있어요:

root : (n : Nat) → Square n → Nat
root .(m * m) (sq m) = m

생성자 sq : (m : Nat) → Square (m * m)로 타입 Square n의 인자에 매칭함으로써 n이 m * m과 같도록 강제된다는 점에 주의하세요.

일반적으로 타입 D i₁ … iₙ의 인자에 생성자 c : (x₁ : A₁) → … → (xₘ : Aₘ) → D j₁ … jₙ로 매칭할 때, Agda는 i₁ … iₙ을 j₁ … jₙ과 통일하려 시도해요. 통일 알고리즘이 변수 x를 값 t로 인스턴스화할 때, 함수의 대응하는 인자는 점 패턴 .t로 대체될 수 있어요.

점 패턴은 가독성을 돕지만 필수는 아니에요. 점 패턴은 함수 정의를 바꾸지 않고 항상 밑줄이나 새 패턴 변수로 대체될 수 있어요. 다음도 root의 합법적인 정의예요:

Agda 2.4.2.4부터:

root₁ : (n : Nat) → Square n → Nat
root₁ _ (sq m) = m

Agda 2.5.2부터:

root₂ : (n : Nat) → Square n → Nat
root₂ n (sq m) = m

root₂의 경우, n은 함수 본문에서 m * m으로 평가되므로 다음과 동등해요:

root₃ : (n : Nat) → Square n → Nat
root₃ _ (sq m) = let n = m * m in m

점 패턴은 전혀 유효한 보통 패턴일 필요 없어요 (위의 m * m의 경우처럼). 그것이 우연히 유효한 보통 패턴이라면, 정의를 바꾸지 않고 점을 제거할 수 있을 때도 있어요.

다른 때에는 점을 제거하면 유효하지만 정의적 동작이 다른 정의가 나와요. 예를 들어 다음 정의에서:

data Fin : Nat → Set where
  fzero : {n : Nat} → Fin (suc n)
  fsuc : {n : Nat} → Fin n → Fin (suc n)

foo : (n : Nat) (k : Fin n) → Nat
foo .(suc zero) (fzero {zero})     = zero
foo .(suc (suc n)) (fzero {suc n}) = zero
foo .(suc _) (fsuc k)              = zero

foo에서 점을 제거하면 케이스 트리가 첫 번째 인자에서 먼저 분할되도록 바뀌어요. 이로 인해 세 번째 방정식이 정의적으로 성립하지 않게 돼요 (그래서 정의는 -exact-split 옵션 아래에서 플래그가 지정돼요).

부정 패턴 (Absurd patterns)

부정 패턴은 특정 인자에 대해 어떤 생성자도 유효하지 않을 때 사용할 수 있어요. 부정 패턴의 문법은 ()이에요.

예를 들어 데이터 타입 Even이 다음과 같이 정의되어 있다면:

data Even : Nat → Set where
  even-zero  : Even zero
  even-plus2 : {n : Nat} → Even n → Even (suc (suc n))

부정 패턴을 사용해 함수 one-not-even : Even 1 → ⊥을 정의할 수 있어요:

one-not-even : Even 1 → ⊥
one-not-even ()

절의 왼쪽 변에 부정 패턴이 포함되면 그 오른쪽 변은 생략되어야 한다는 점에 주의하세요.

일반적으로 타입 D i₁ … iₙ의 인자에 부정 패턴으로 매칭할 때, Agda는 데이터 타입 D의 각 생성자 c : (x₁ : A₁) → … → (xₘ : Aₘ) → D j₁ … jₙ에 대해 i₁ … iₙ을 j₁ … jₙ과 통일하려 시도해요. 부정 패턴은 이 통일들이 모두 충돌로 끝날 때만 받아들여져요.

As-패턴 (As-patterns)

As-패턴(@-패턴)은 패턴에 이름을 붙이는 데 사용할 수 있어요. 이름은 보통 패턴 변수와 같은 스코프(즉 오른쪽 변, where 절, 점 패턴)를 가져요. 이름은 이름 붙은 패턴의 값으로 축약돼요. 예를 들어:

module _ {A : Set} (_<_ : A → A → Bool) where
  merge : List A → List A → List A
  merge xs [] = xs
  merge [] ys = ys
  merge xs@(x ∷ xs₁) ys@(y ∷ ys₁) =
    if x < y then x ∷ merge xs₁ ys
             else y ∷ merge xs ys₁

As-패턴은 Agda 2.5.2부터 제대로 지원돼요.

케이스 트리 (Case trees)

내부적으로 Agda는 함수 정의를 케이스 트리(case tree)로 나타내요. 예를 들어 함수 정의:

max : Nat → Nat → Nat
max zero    n       = n
max m       zero    = m
max (suc m) (suc n) = suc (max m n)

는 내부적으로 다음과 같은 케이스 트리로 나타내져요:

max m n = case m of
  zero   → n
  suc m' → case n of
    zero   → suc m'
    suc n' → suc (max m' n')

Agda가 함수 max의 이 표현을 사용하기 때문에, 절 max m zero = m은 정의적으로(즉 축약 규칙으로) 성립하지 않아요. 이 방정식이 성립함을 증명하려 하면 refl을 쓸 수 없을 거예요:

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- 동작하지 않음!
lemma : (m : Nat) → max m zero ≡ m
lemma = refl

정의적으로 성립하지 않는 절은 대개(항상은 아니지만) Agda의 케이스 분할 전술 대신 절을 손으로 쓴 결과예요. 이 절들은 Emacs에서 강조 표시돼요.

--exact-split 플래그는 패턴 매칭으로 정의한 절이 정의적으로 성립하지 않을 때마다 Agda가 경고를 올리게 해요. 특정 절은 {-# CATCHALL #-} 프래그마로 이 검사에서 제외할 수 있어요.

예를 들어 위의 max 정의는 두 번째 절이 정의적으로 성립하지 않기 때문에 --exact-split 플래그를 사용할 때 플래그가 지정돼요.

--exact-split 플래그를 사용할 때 catch-all 절은 그렇게 표시되어야 해요. 예를 들어:

eq : Nat → Nat → Bool
eq zero    zero    = true
eq (suc m) (suc n) = eq m n
{-# CATCHALL #-}
eq _       _       = false

--no-exact-split 플래그를 사용해 파일에서 전역 --exact-split을 오버라이드할 수 있는데, 프래그마 {-# OPTIONS --no-exact-split #-}를 추가하면 돼요. 이 옵션은 기본적으로 활성화되어 있어요.

버전 2.8.0부터 Agda는 불필요한 CATCHALL 프래그마에 대해 경고하며 UselessPragma를 플래그로 지정해요.

더 알아보기 (Learn more)