프래그마

프래그마 (Pragmas)

프래그마는 일반 선언이 어떻게 해석되어야 하는지에 대한 추가 정보를 Agda에 전달하는 특별한 선언이에요. 블록 주석과 비슷하게 작성되어, 사용자가 Agda 문서를 처음 읽을 때 쉽게 건너뛸 수 있게 해줘요.

일반적인 형식은:

{-# <PRAGMA_NAME> <arguments> #-}

프래그마 색인 (Index of pragmas)

  • BUILTIN
  • CATCHALL
  • COMPILE
  • DISPLAY
  • ETA_EQUALITY
  • FOREIGN
  • INJECTIVE
  • INJECTIVE_FOR_INFERENCE
  • INLINE
  • NO_POSITIVITY_CHECK
  • NO_TERMINATION_CHECK
  • NO_UNIVERSE_CHECK
  • NOINLINE
  • NON_COVERING
  • NON_TERMINATING
  • OPTIONS
  • POLARITY
  • REWRITE
  • STATIC
  • TERMINATING
  • WARNING_ON_USAGE
  • WARNING_ON_IMPORT

명령줄 및 프래그마 옵션(Command-line and pragma options)도 참고하세요.

DISPLAY 프래그마 (The DISPLAY pragma)

사용자는 DISPLAY 프래그마로 표시 형식(display form)을 선언할 수 있어요:

{-# DISPLAY f e1 .. en = e #-}

이것은 f e1 .. en이 e와 같은 방식으로 출력되게 하는데, 여기서 ei는 e에서 사용되는 변수를 바인딩할 수 있어요. 표현식 ei와 e는 스코프 검사되지만 타입 검사되지는 않아요.

예를 들어 오버로드된 (인스턴스) 함수를 오버로드된 이름으로 출력하는 데 사용할 수 있어요:

instance
  NumNat : Num Nat
  NumNat = record { ..; _+_ = natPlus }

{-# DISPLAY natPlus a b = a + b #-}

제한 사항:

  • 표시 형식의 왼쪽 변은 변수, 생성자, 정의된 함수 또는 타입, 리터럴로 제한돼요. 특히 람다는 왼쪽 변에 허용되지 않아요.
  • 표시 형식은 타입 검사되지 않으므로, f의 타입이 패턴 매칭 후 암시 함수 공간으로 계산되면 암시 인자 삽입이 제대로 동작하지 않을 수 있어요.
  • 잘못 타입된 표시 형식은 Agda가 그것을 사용하려고 할 때 내부 오류로 Agda가 충돌하게 할 수 있어요 (이슈 #6476).

INJECTIVE 프래그마 (The INJECTIVE pragma)

injective 프래그마는 패턴 매칭 통일자(unifier)에 대해 정의를 단사(injective)로 표시하는 데 사용할 수 있어요. 이것은 특정 데이터 타입에만 적용되는 --injective-type-constructors의 버전으로 사용할 수 있어요.

예제:

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

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

{-# INJECTIVE Fin #-}

Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
Fin-injective refl = refl

데이터 타입 외에도 이 프래그마는 다른 정의(postulate 같은)를 단사로 표시하는 데 사용할 수 있어요. 현재 그것은 명제적 단사성(propositional injectivity)만 줄 뿐이라, 위 예제에서 Fin x ≡ Fin y의 증명에 패턴 매칭할 수 있지만, 제약 해결사가 Fin x = Fin _ 제약을 해결하는 방법을 알지 못하므로 정의적 단사성(definitional injectivity)은 주지 않아요.

관련 이슈: https://github.com/agda/agda/issues/4106#issuecomment-534904561

INJECTIVE_FOR_INFERENCE 프래그마 (The INJECTIVE_FOR_INFERENCE pragma)

타입 추론을 위해 함수를 단사로 취급해요. 이것은 --lossy-unification의 로컬 버전처럼 동작하고 똑같은 잠재적 문제가 있어요. Agda가 함수가 단사인지 항상 추론할 수는 없으므로, 그 함수들에 대해 더 강한 통일을 얻는 데 사용할 수 있어요.

--no-require-unique-meta-solutions 옵션은 함수가 사용되는 파일에서 활성화되어야 하지만, 정의된 파일에서는 반드시 그럴 필요는 없어요. --require-unique-meta-solutions가 적용 중인 파일에서 함수를 포함하는 제약을 해결할 때는 프래그마가 무시돼요.

예제:

open import Agda.Builtin.Equality
open import Agda.Builtin.List

module _ {A : Set} where
  _++_ : List A → List A → List A
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  reverse : List A → List A
  reverse []      = []
  reverse (x ∷ l) = reverse l ++ (x ∷ [])

  {-# INJECTIVE_FOR_INFERENCE reverse #-}

  reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
  reverse-≡ h = h

  []≡[] : {l l' : List A} → [] ≡ []
  []≡[] = reverse-≡ (refl {x = reverse []})

INLINE과 NOINLINE 프래그마 (The INLINE and NOINLINE pragmas)

INLINE 프래그마로 표시된 함수 정의는 컴파일 중에 인라인돼요. 패턴 매칭을 하지 않는 단순한 함수 정의라면 타입 체킹 시점에도 함수 본문에서 인라인돼요.

--auto-inline 명령줄 옵션이 활성화되면 함수 정의가 다음 기준을 충족하면 자동으로 INLINE으로 표시돼요:

  • 패턴 매칭이 없음.
  • 각 인자를 최대 한 번씩 사용함.
  • 모든 인자를 사용하지 않음.

자동 인라인은 NOINLINE 프래그마로 막을 수 있어요.

예제:

-- 타입 인자를 사용하지 않으므로 자동 인라인됨.
_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

{-# NOINLINE _∘_ #-} -- 자동 인라인 방지

-- 모든 인자를 사용하므로 자동 인라인되지 않음.
_o_ : (Set → Set) → (Set → Set) → Set → Set
(F o G) X = F (G X)

{-# INLINE _o_ #-} -- 인라인 강제

생성자 오른쪽 변 인라인 (Inlining constructor right-hand sides)

버전 2.6.4에 추가됨.

생성자도 INLINE으로 표시할 수 있어요 (코패턴 매칭을 지원하는 타입용):

record Stream (A : Set) : Set where
  coinductive; constructor _∷_
  field head : A
        tail : Stream A
open Stream
{-# INLINE _∷_ #-}

이 생성자들을 사용하는 함수 정의는 그 대신 코패턴 매칭을 사용하도록 번역돼요. 예:

nats : Nat → Stream Nat
nats n = n ∷ nats (1 + n)

는 다음과 같이 번역돼요:

nats' : Nat → Stream Nat
nats' n .head = n
nats' n .tail = nats (n + 1)

이것은 종료 검사를 통과해요. 이 번역은 함수 정의의 오른쪽 변의 루트에 있는 완전히 적용된 생성자에 대해서만 동작해요.

--exact-split이 켜져 있으면 인라인은 nats에 대해 InlineNoExactSplit 경고를 촉발해요.

NON_COVERING 프래그마 (The NON_COVERING pragma)

버전 2.6.1에 추가됨.

NON_COVERING 프래그마는 사용자가 부분 함수(partial)임을 아는 함수(또는 상호 정의된 함수 블록) 앞에 둘 수 있어요. 특정 함수에만 적용되는 --allow-incomplete-matches의 버전으로 사용할 수 있어요.

NOT_PROJECTION_LIKE 프래그마 (The NOT_PROJECTION_LIKE pragma)

버전 2.6.3에 추가됨.

NOT_PROJECTION_LIKE 프래그마는 특정 함수에 대한 투영 유사성(projection-likeness) 분석을 비활성화해요. 이 함수는 프래그마의 영향을 받기 전에 정의되어야 해요. 특정 함수에만 적용되는 --no-projection-like의 버전으로 사용할 수 있어요.

예를 들어 인스턴스 인자에서 필드를 투영하고 인스턴스 선택이 가시 인자에 의존하는 함수가 있다고 가정해 봐요. 이 함수의 적용이 메타프로그래밍으로 생성되고 elaborate-and-give(Emacs에서 C-c C-m)가 소스 코드에 삽입하면, 가시 인자는 지워졌기 때문에 오히려 _로 출력돼요!

예제:

open import Agda.Builtin.Bool

record P (n : Nat) : Set where
  field the-bool : Bool
open P

-- Agda는 보통 이것을 투영 유사로 표시해서, 출력할 때(예: elaborate-and-give)
-- (n : Nat) 인자를 지우게 됨
get-bool-from-p : (n : Nat) ⦃ has-p : P n ⦄ → Bool
get-bool-from-p _ ⦃ p ⦄ = p .the-bool
{-# NOT_PROJECTION_LIKE get-bool-from-p #-}

-- 프래그마를 사용하면 일반 함수로 취급됨.

OPTIONS 프래그마 (The OPTIONS pragma)

일부 옵션은 .agda 파일의 맨 위에 다음 형태로 주어질 수 있어요:

{-# OPTIONS --{opt₁} --{opt₂} ... #-}

가능한 옵션은 명령줄 및 프래그마 옵션(Command-line and pragma options)에 나열돼 있어요.

WARNING_ON_ 프래그마 (The WARNING_ON_ pragmas)

라이브러리 작성자는 WARNING_ON_USAGE 프래그마를 사용해 정의된 이름에, 그 이름이 사용될 때마다 발생할 경고를 붙일 수 있어요 (Agda 2.5.4부터). 마찬가지로 WARNING_ON_IMPORT 프래그마를 사용해 모듈에, 그 모듈이 임포트될 때마다 발생할 경고를 붙일 수 있어요 (Agda 2.6.1부터). 이것은 보통 이름이나 모듈을 'DEPRECATED'(폐기됨)로 선언하고, 기능이 제거되기 전에 코드를 이식하도록 최종 사용자에게 조언하는 데 사용돼요.

사용자는 --warn=noUserWarning 옵션으로 이 경고들을 끌 수 있어요. 경고 장치에 대한 더 많은 정보는 경고(Warnings)를 참고하세요.

예제:

-- 항등의 새 이름
id : {A : Set} → A → A
id x = x

-- 폐기된 이름
λx→x = id

-- 경고
{-# WARNING_ON_USAGE λx→x "DEPRECATED: Use `id` instead of `λx→x`" #-}
{-# WARNING_ON_IMPORT "DEPRECATED: Use module `Function.Identity` rather than `Identity`" #-}

더 알아보기 (Learn more)