런타임 비관련성

런타임 비관련성 (Run-time Irrelevance)

버전 2.6.1부터 Agda는 런타임 비관련성(또는 소거, erasure) 주석을 지원해요. 소거로 표시된 값은 런타임에 존재하지 않으므로, 결과적으로 타입 체커는 어떤 계산도 소거된 값에 의존하지 않도록 강제해요.

문법 (Syntax)

함수 또는 생성자 인자는 @0 또는 @erased 주석으로 소거로 선언돼요. (이 주석들은 --erasure 옵션이 활성화된 경우에만 사용할 수 있어요.)

예를 들어 다음 벡터 정의는 _∷_에 대한 길이 인자가 런타임에 존재하지 않음을 보장해요:

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

GHC 백엔드는 이것을 cons 생성자가 두 인자만 취하는 데이터 타입으로 컴파일해요.

참고: 이 특별한 경우에 컴파일러는 주석 없이도 Brady 등의 강제 분석(forcing analysis) [1]을 사용해 길이 인자를 소거할 수 있다는 것을 식별해요. 그러나 그것을 명시적으로 소거로 표시하면 분석에 의존하지 않고 소거됨을 보장해요.

참고: --erasure를 사용하면 생성자와 레코드 필드의 타입 시그니처에서 매개변수는 데이터 또는 레코드 타입의 텔레스코프에서 소거로 표시되지 않아도 소거로 표시돼요. 단 한 가지 예외가 있어서, 인덱스된 데이터 타입의 경우 --with-K 플래그가 활성화된 경우에만 이렇게 돼요.

소거 주석은 함수 인자(1차원과 고차원 모두)에도 나타날 수 있어요. 예를 들어 벡터의 foldl 구현은 다음과 같아요:

foldl : (B : @0 Nat → Set b)
      → (f : ∀ {@0 n} → B n → A → B (suc n))
      → (z : B 0)
      → ∀ {@0 n} → Vec A n → B n
foldl B f z []       = z
foldl B f z (x ∷ xs) = foldl (λ n → B (suc n)) (λ {n} → f {suc n}) (f z x) xs

여기서 foldl과 f에 대한 길이 인자들이 소거로 표시됐어요. 결과적으로 다음 하스켈 코드로 컴파일돼요 (이름 변경 제외):

foldl f z xs
  = case xs of
      []     -> z
      x ∷ xs -> foldl f (f _ z x) xs

생성자 인자와 대조적으로, 고차 함수에 대한 소거 인자는 완전히 제거되지 않고 대신 자리 표시자 값 _로 대체돼요. 소거 주석이 가능하게 하는 핵심 최적화는 λ {n} → f {suc n}을 단순히 f로 컴파일하여 프로그램에서 심각한 공간 누수(space leak)를 제거하는 것이에요. 소거 없이 컴파일한 결과와 비교해 봐요:

foldl f z xs
  = case xs of
      []     -> z
      x ∷ xs -> foldl (\ n -> f (1 + n)) (f 0 z x) xs

소거된 정의와 필드 (Erased definitions and fields)

최상위 함수 정의를 소거로 표시하는 것도 가능해요. 이것은 소거된 인자에서만 사용됨을 보장하고, 컴파일 타임 평가 전용으로 의도된 코드가 런타임에 실행되지 않도록 하는 데 유용할 수 있어요. (소거된 정의의 본문에서도 소거된 것을 사용할 수 있어요.) 예를 들어:

@0 spec : Nat → Nat   -- 느리지만, 검증하기 쉬움
impl    : Nat → Nat   -- 빠르지만, 이해하기 어려움
proof   : ∀ n → spec n ≡ impl n

소거된 레코드 필드는 레코드 생성자에 대한 소거된 인자가 되고, 투영 함수는 소거된 정의로 취급돼요.

소거된 생성자 (Erased constructors)

생성자도 소거로 표시할 수 있어요:

data D : Set where
  always : D
  @0 compile-time-only : D

caseD : A → @0 A → D → A
caseD a c always            = a
caseD a c compile-time-only = c

위 코드에서 생성자 compile-time-only는 컴파일 타임에만 사용 가능하고, always는 런타임에도 사용 가능해요. 비-소거 위치에서 소거된 생성자에 매칭하는 절은 (적어도 일부) 컴파일러 백엔드에 의해 생략되므로, 그러한 절의 본문에서 소거된 이름을 사용할 수 있어요. (원래 소거로 선언되지 않았지만 현재 소거된 것으로 취급되는 생성자에 대한 예외가 있어요.)

소거된 생성자에 대한 더 의미 있는 예는 고차 귀납 타입과 관련된 것이며, 소거된 생성자를 참고하세요.

소거된 데이터 타입 (Erased data types)

데이터 및 레코드 타입을 소거로 표시할 수도 있어요. 그러한 타입은 소거된 위치에서만 사용될 수 있고, 그들의 생성자와 투영은 소거되며, 소거된 레코드 타입의 레코드 모듈 안의 정의는 소거돼요. 데이터 또는 레코드 타입은 선언의 data 또는 record 키워드 바로 뒤에 @0 또는 @erased를 써서 소거로 표시돼요:

data @0 D₁ : Set where
  c : D₁

data @0 D₂ : Set

data D₂ where
  c : D₁ → D₂

interleaved mutual

  data @0 D₃ : Set where

  data D₃ where
    c : D₃

record @0 R₁ : Set where
  field
    x : D₁

record @0 R₂ : Set

record R₂ where
  field
    x : R₁

소거된 모듈 (Erased modules)

마지막으로 모듈을 소거로 표시할 수 있어요. 모듈 식별자 자체는 소거되지 않지만, 모듈 안의 모든 정의는 소거돼요. 모듈은 module 키워드 바로 뒤에 @0 또는 @erased를 써서 소거로 표시돼요:

module @0 _ where

  F : @0 Set → Set
  F A = A

module M (@0 A : Set) where

  record R : Set where
    field
      @0 x : A

module @0 N (@0 A : Set) = M A

G : (@0 A : Set) → let module @0 M₂ = M A in Set
G A = M.R C
  module @0 _ where
    C : Set
    C = A

람다 추상화 (Lambda abstraction)

람다로 바인딩된 변수는 소거 상태 @0과 @ω로 주석을 달 수 있어요. 람다 표현식의 타입이 알려져 있으면 그러한 주석은 불필요하며, 이 경우 타입에서 상속돼요:

checkedLambda : _ → _
checkedLambda = λ x → x + x

const : {A B : Set} → A → @0 B → A
const = λ x y → x

타입이 알려져 있지 않고 Agda가 추론해야 한다면 주석은 필수예요. 예를 들어 다음 정의는 Agda가 받아들이지 않아요:

inferredLambda = λ x → x + x

x가 소거되지 않음을 알려주면 받아들여져요:

inferredLambda = λ (@ω x) → x + x

모든 람다 바인딩 변수에 소거 상태를 주석으로 달아야 해요:

Const = λ (@ω A : Set) (@0 B : Set) → A

그러나 --cubical에서는 람다가 일반적으로 추론되지 않는다는 점에 주의하세요.

패턴 람다 (Pattern lambdas)

일반 패턴 람다는 비-소거 함수 정의로 취급돼요. 람다 앞에 @0 또는 @erased를 써서 패턴 람다를 소거로 만들 수 있어요:

@0 _ : @0 Set → Set
_ = λ @0 { A → A }

@0 _ : @0 Set → Set
_ = λ @erased where
  A → A

규칙 (Rules)

타이핑 규칙은 Conor McBride의 "I Got Plenty o'Nuttin'" [2]과 Bob Atkey의 "The Syntax and Semantics of Quantitative Type Theory" [3]에 기반해요. 본질적으로 타입 체커는 런타임에 필요한 것을 검사하는 런타임 모드에서 실행 중인지, 아니면 소거될 것을 검사하는 컴파일 타임 모드에서 실행 중인지 추적해요. 컴파일 타임 모드에서는 소거와 관련된 모든 것을 안전하게 무시할 수 있지만, 런타임 모드에서는 다음 제한이 적용돼요:

소거된 변수나 정의를 사용할 수 없음.
소거된 인자에 패턴 매칭할 수 없음. 단, 가장 유효한 경우가 하나뿐인 경우(소거된 매칭)는 예외. 소거된 매칭은 --erased-matches의 설정에 따라 허용되거나 허용되지 않을 수 있어요.
소거된 매칭이 허용되면 바인딩된 변수는 모두 소거된 것으로 취급돼요.

η-동등성이 있는 레코드 타입에 대한 매칭은 실제로 매칭이 아니라는 점에 주의하세요. 이는 오른쪽 변에서 투영 함수를 사용하는 것에 해당하기 때문이에요. 그러한 매칭은 항상 허용되지만, 바인딩된 변수는 소거된 것으로 취급돼요.

소거된 벡터 인자를 취하는 함수 foo를 생각해 봐요:

foo : (n : Nat) (@0 xs : Vec Nat n) → Nat
foo zero    []       = 0
foo (suc n) (x ∷ xs) = foo n xs

이것은 (다른 설정에서는) 허용되는데, 길이에 매칭한 후에는 벡터에 대한 매칭이 어떤 계산적 정보도 제공하지 않고, 패턴의 모든 변수(x와 xs)가 차례로 소거로 표시되기 때문이에요. 반면에 먼저 길이에 매칭하지 않으면 타입 체커가 불평해요:

foo : (n : Nat) (@0 xs : Vec Nat n) → Nat
foo n []       = 0
foo n (x ∷ xs) = foo _ xs
-- 오류: Cannot branch on erased argument of datatype Vec Nat n

타입 체커는 다음 경우에 컴파일 타임 모드로 진입해요:

생성자, 함수 또는 모듈 적용에 대한 소거된 인자를 검사할 때,
소거된 정의(소거된 모듈 적용 포함)의 본문을 검사할 때,
원래 소거로 정의된 생성자에 (비-소거 위치에서) 매칭하는 절의 본문을 검사할 때 (생성자가 현재 소거된 것으로 취급되는 것만으로는 충분하지 않음),
소거된 Π 타입의 정의역을 검사할 때, 또는
타입을 검사할 때, 즉 :의 오른쪽으로 이동할 때. 몇 가지 예외가 있어요:
- 비-소거 Π 타입의 정의역에 대해서는 컴파일 타임 모드로 진입하지 않음.
- K 규칙이 꺼져 있으면 (fibrant 타입의) 비-소거 생성자나 레코드 필드에 대해서는 컴파일 타임 모드로 진입하지 않음.

타입 체커는 항이 검사되는 타입에 기반해 컴파일 타임 모드로 진입하지 않는다는 점에 주의하세요 (fibrant와 비-fibrant 타입 사이의 구분이 때때로 이루어지는 경우는 제외). 특히 Set에 대해 항을 검사하는 것은 컴파일 타임 모드를 촉발하지 않아요.

하드 컴파일 타임 모드(hard compile-time mode)라는 것도 있어요. 이 모드에서는 모든 정의가 소거된 것으로 취급돼요. 하드 컴파일 타임 모드는 소거된 정의가 검사될 때 진입돼요.

소거된 문맥의 이름 없는 및 이름 있는 where 모듈은 항상 하드 컴파일 타임 모드에서 검사돼요.

타입 체커는 하드 컴파일 타임 모드에 있지 않으면 다음 표현식/선언에 대해 컴파일 타임 모드에서 런타임 모드로 전환해요:

부정 람다 (Absurd lambdas).
비-소거 패턴 람다.
비-소거 모듈 정의 (module M … = …) 또는 적용 (M …).
♯의 적용 (옛 공유도(Old Coinduction) 참고).

반영 API는 수동으로 타입 체커를 런타임 모드에서 컴파일 타임 모드로 전환하는 프리미티브 함수 workOnTypes : TC A → TC A를 제공해요.

참고 문헌 (References)

[1] Brady, Edwin, Conor McBride, and James McKinna. "Inductive Families Need Not Store Their Indices." International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 2003.

[2] McBride, Conor. "I Got Plenty o'Nuttin'." A List of Successes That Can Change the World. Springer, Cham, 2016.

[3] Atkey, Robert. "The Syntax and Semantics of Quantitative Type Theory". In LICS '18: Oxford, United Kingdom. 2018.

더 알아보기 (Learn more)

Agda 문서: 런타임 비관련성 원문