추상 정의

추상 정의 (Abstract Definitions)

Agda에서는 정의를 abstract로 표시할 수 있어요. 이렇게 하면 구현 세부 사항을 숨기거나 다른 부분의 타입 체킹 속도를 높일 수 있답니다. 본질적으로 추상 정의는 postulate처럼 동작해서, 축약(reduce)되거나 계산(compute)되지 않아요. 예를 들어 내용이 중요하지 않은 증명은 abstract로 표시해서 Agda가 이를 펼쳐 보이는 것을 막을 수 있어요. 이렇게 하면 타입 체킹이 느려지는 것을 방지할 수 있고요.

추상 정의에 관한 모든 규칙은 추상 정의의 구현 세부 사항이 새어 나가는 것을 막도록 설계되어 있어요. 다른 프로그래밍 언어에서 비슷한 개념으로는 다음과 같은 것들이 있어요 (대표적인 예시만 골랐어요):

• UCSD 파스칼과 자바의 인터페이스
• ML의 시그니처

(특히 추상 정의를 모듈과 함께 쓸 때 이러한 개념이 중요해져요.)

개요 (Synopsis)

선언은 블록 키워드 abstract를 사용해서 추상으로 표시할 수 있어요.

abstract 블록 밖에서는 추상 정의가 축약되지 않고 postulate처럼 취급돼요. 특히:

• 추상 함수는 절대 매칭되지 않아서 축약되지 않아요.
• 추상 데이터 타입은 자신의 생성자를 드러내지 않아요.
• 추상 레코드 타입은 자신의 필드도 생성자도 드러내지 않아요.
• 그 외의 선언은 추상이 될 수 없어요.

abstract 블록 안에서는 추상 정의가 정의의 타입 체킹 동안에는 축약되지만, 타입 시그니처를 체크하는 동안에는 축약되지 않아요.

만약 그렇지 않다면, 의존 타입 때문에 구현 세부 사항이 새어 나갈 수 있어요 (예: 명제적 동일성(propositional equality)을 사용해서 축약 동작을 드러내는 것).

결과적으로 정의의 본문을 체크하면서 얻은 정보가 타입 시그니처로 새어 나갈 수 없어요. 이는 추상 정의에 대한 타입 추론을 사실상 비활성화해요. 즉, 모든 추상 정의는 완전한 타입 시그니처를 가져야 해요.

abstract 키워드 블록의 영향 범위는 함수의 where 블록과 레코드 선언 안의 선언까지 재귀적으로 확장돼요. 하지만 abstract 블록 안에서 선언된 모듈의 내부까지는 확장되지 않아요.

예제 (Examples)

정수(integer)는 여러 가지 방식으로 구현될 수 있어요. 예를 들어 두 자연수의 차이로 구현할 수 있답니다:

module Integer where

  abstract

    ℤ : Set
    ℤ = Nat × Nat

    0ℤ : ℤ
    0ℤ = 0 , 0

    1ℤ : ℤ
    1ℤ = 1 , 0

    _+ℤ_ : (x y : ℤ) → ℤ
    (p , n) +ℤ (p' , n') = (p + p') , (n + n')

    _*ℤ_ : (x y : ℤ) → ℤ
    (a , b) *ℤ (c , d) = ((a * c) + (b * d)) , ((a * d) + (b * c))

    infixl 20 _+ℤ_
    infixl 30 _*ℤ_

    -ℤ_ : ℤ → ℤ
    -ℤ (p , n) = (n , p)

    _≡ℤ_ : (x y : ℤ) → Set
    (p , n) ≡ℤ (p' , n') = (p + n') ≡ (p' + n)

    infix 10 _≡ℤ_

    private
      postulate
        +comm : ∀ n m → (n + m) ≡ (m + n)

    invℤ : ∀ x → (x +ℤ (-ℤ x)) ≡ℤ 0ℤ
    invℤ (p , n) rewrite +comm (p + n) 0 | +comm p n = refl

abstract를 사용하면 정수의 실제 표현과 연산의 구현을 드러내지 않아요. 0ℤ, 1ℤ, _+ℤ_, -ℤ_로부터 정수를 구성할 수 있지만, 제공된 보조 정리 invℤ를 통해서만 동일성 ≡ℤ에 대해 추론할 수 있어요.

정수 0의 다음 속성 shape-of-0ℤ는 정수를 쌍으로 표현한 것을 드러내요. 그래서 Agda는 이를 거부해요: 타입 시그니처를 체크할 때, x가 추상 타입 ℤ이므로 proj₁ x는 타입 체크에 실패해요. abstract 블록 안에 있어도 ℤ의 추상 정의는 타입 시그니처에서 펼쳐지지 않는다는 것을 기억하세요! 이를 우회하려면 projection 함수에 대한 별칭을 정의해야 해요:

-- 속성 0인 정수의 표현에 관한 속성:

  abstract
    private
      posZ : ℤ → Nat
      posZ = proj₁

      negZ : ℤ → Nat
      negZ = proj₂

      shape-of-0ℤ : ∀ (x : ℤ) (is0ℤ : x ≡ℤ 0ℤ) → posZ x ≡ negZ x
      shape-of-0ℤ (p , n) refl rewrite +comm p 0 = refl

shape-of-0ℤ를 타입 체크하기 위해 private로 요구함으로써 표현 세부 사항이 새어 나가는 것을 막아요.

추상화의 범위 (Scope of abstraction)

자식 모듈에서 추상 정의를 체크할 때, 부모 모듈의 추상 정의는 투명해요:

module M1 where
  abstract
    x : Nat
    x = 0

  module M2 where
    abstract
      x-is-0 : x ≡ 0
      x-is-0 = refl

따라서 자식 모듈은 부모 모듈의 표현 선택을 볼 수 있어요. 하지만 부모 모듈은 자식 모듈을 이렇게 들여다볼 수 없고, 형제 모듈들도 서로의 추상 정의를 꿰뚫어 볼 수 없어요. 이에 대한 예외는 익명 모듈인데, 익명 모듈은 부모 모듈과 추상 범위를 공유해서 부모나 형제 모듈이 그 안의 추상 정의를 볼 수 있게 해요.

abstract 키워드의 영향 범위는 모듈 안으로 확장되지 않아요:

module Parent where
  abstract
    module Child where
      y : Nat
      y = 0
    x : Nat
    x = 0  -- "useless abstract" 오류를 피하려고

  y-is-0 : Child.y ≡ 0
  y-is-0 = refl

Child 모듈 안의 선언은 추상이 아니에요!

where 블록과 함께 쓰는 추상 정의 (Abstract definitions with where-blocks)

추상 정의의 where 블록에 있는 정의도 역시 추상이에요. 즉, 이들은 삼촌(uncle)의 추상화를 꿰뚫어 볼 수 있어요:

module Where where
  abstract
    x : Nat
    x = 0
    y : Nat
    y = x
      where
      x≡y : x ≡ 0
      x≡y = refl

더 알아보기 (Learn more)

• Agda 문서: 추상 정의 원문