손실적 통일
손실적 통일 (Lossy Unification)
--lossy-unification 옵션은 통일(unification) 검사기의 실험적 휴리스틱을 활성화해요. 이는 f es₀ = f es₁ 형태의 통일 문제, 즉 여기서 f인 같은 정의된 함수의 두 적용을 (아마도 다른) 인자와 projection 목록 es₀과 es₁에 대해 통일하는 문제의 성능을 향상시키기 위한 것이에요.
이 휴리스틱은 건전(sound)하지만 완전(complete)하지는 않아요. 특히 Agda가 이 플래그로 코드를 받아들이면 (충분한 자원과, 어쩌면 추가 타입 주석이 필요할 수 있지만) 플래그 없이도 그 코드를 받아들여야 해요.
이 옵션은 전역적으로 또는 OPTIONS 프래그마에서 사용할 수 있고, 후자의 경우 현재 모듈에만 적용돼요.
f에 대해서만 손실적 통일을 활성화하는 {-# INJECTIVE_FOR_INFERENCE f #-} 프래그마도 있어요.
휴리스틱 (Heuristic)
통일 문제 f es₀ = f es₁을 풀려고 할 때 이 휴리스틱은 es₀ = es₁을 풀려고 시도함으로써 진행돼요. 그게 성공하면 원래 문제도 풀리고, 그렇지 않으면 통일은 플래그 없이처럼 진행되는데, 아마도 f es₀과 f es₁ 둘 다를 축약할 거예요.
예제 (Example)
f가 아래처럼 입력에 100을 더한다고 가정해 봐요:
f : ℕ → ℕ
f n = 100 + n
그러면 f 2와 f (1 + 1)을 통일하기 위해 휴리스틱은 2를 (1 + 1)과 통일하는 것으로 진행하는데, 이것은 빠르게 성공해요. 플래그가 없으면 대신 f 2와 f (1 + 1) 둘 다 102로 축약한 다음 그 결과들을 비교할 수도 있어요.
f의 적용을 축약하면 큰 항이 생길 때 성능이 가장 극적으로 개선돼요. 어쩌면 여러 필드를 가진 레코드 타입의 원소거나, 큰 임베딩된 증명 항의 원소일 수 있죠.
단점 (Drawbacks)
한 가지 단점은 어떤 경우에는 이 휴리스틱으로 통일 성능이 더 나빠진다는 거예요. 구체적으로 휴리스틱이 인자 목록 es₀ = es₁의 통일을 반복적으로 시도하면서 실패하는 경우예요.
주요 단점은 휴리스틱이 완전하지 않아서, Agda가 통일 변수의 일부 가능한 해를 무시하게 된다는 것이에요.
예를 들어 f가 상수 함수라면, 제약 f ?0 = f 1은 ?0을 유일하게 결정하지 않지만, 휴리스틱은 결국 ?0에 1을 할당하게 돼요.
하지만 f가 주입적이면 이 휴리스틱은 완전해요.
이런 할당은 Agda가 휴리스틱 없이는 보고되지 않았을 타입 오류를 보고하게 만들 수 있어요. 그 이유는 ?0 = 1에 전념하면 다른 제약들이 만족 불가능해질 수 있기 때문이에요.
이런 할당은 독자를 혼란스럽게 할 수도 있어요. 비-손실 통일에서는 (버그가 없다는 가정 하에) 코드가 타입 체크되고 모든 메타 변수를 인스턴스화하는 일관된 방법 하나를 찾을 수 있다면, 그것이 시스템이 코드를 해석하는 방식이라는 보장이 있어요. 손실적 통일에서는 당신이 생각하는 해가 시스템이 사용하는 해가 아닐 수 있어요.
López Juan의 박사 논문(리스팅 6.16 참고)의 예제를 기반으로 한 다음 코드를 생각해 봐요:
{-# OPTIONS --lossy-unification #-}
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
private variable
m n : Nat
infixr 5 _∷_ _++_
data Bit-vector : Nat → Set where
[] : Bit-vector 0
_∷_ : Bool → Bit-vector n → Bit-vector (suc n)
_++_ : Bit-vector m → Bit-vector n → Bit-vector (m + n)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
replicate : ∀ n → Bool → Bit-vector n
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x
vector : Bit-vector (m + n)
vector {m = m} {n = n} = replicate m true ++ replicate n false
다음 네 개의 비트 벡터의 값을 모두 자신 있게 예측할 수 있나요? 코드의 독자들이 이것을 할 수 있다고 확신하나요?
ex₁ : Bit-vector (0 + 1)
ex₁ = vector
ex₂ : Bit-vector (1 + 0)
ex₂ = vector
ex₃ : Bit-vector ((0 + 1) + (1 + 0))
ex₃ = xs ++ xs
where
xs = vector
ex₄ : Bit-vector ((0 + 1) + (1 + 0))
ex₄ = xs ++ xs
where
xs = vector {m = _}
참고 문헌 (References)
단일 한 줄 정의의 느린 타입 체킹, 이슈 (#1625).