패턴 동의어
패턴 동의어 (Pattern Synonyms)
패턴 동의어는 왼쪽 변(lhs, 패턴 매칭할 때)과 오른쪽 변(rhs, 표현식에서) 양쪽에서 사용할 수 있는 선언이에요. 예를 들어:
data Nat : Set where
zero : Nat
suc : Nat → Nat
pattern z = zero
pattern ss x = suc (suc x)
f : Nat → Nat
f z = z
f (suc z) = ss z
f (ss n) = n
패턴 동의어는 추상 구문에 대한 치환으로 구현되므로, 정의는 스코프 검사만 되고 타입 검사는 되지 않아요. 이들은 특히 유니버스 구성에 유용해요.
오버로딩 (Overloading)
패턴 동의어는 모든 후보가 같은 형태(shape)를 가질 때에만 오버로드될 수 있어요. 두 패턴 동의어 정의는 변수와 생성자 이름을 무시하고 같을 때 같은 형태를 가진다고 해요. 형태는 해석(resolution) 시점과 중첩 패턴 동의어의 확장 이후에 검사돼요.
예를 들어:
data List (A : Set) : Set where
lnil : List A
lcons : A → List A → List A
data Vec (A : Set) : Nat → Set where
vnil : Vec A zero
vcons : ∀ {n} → A → Vec A n → Vec A (suc n)
pattern [] = lnil
pattern [] = vnil
pattern _∷_ x xs = lcons x xs
pattern _∷_ y ys = vcons y ys
lmap : ∀ {A B} → (A → B) → List A → List B
lmap f [] = []
lmap f (x ∷ xs) = f x ∷ lmap f xs
vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
vmap f [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs
vcons의 동의어에서 인자를 뒤집어 pattern _∷_ ys y = vcons y ys로 바꾸면, 그 동의어를 사용하려 할 때 다음 오류가 발생해요:
Cannot resolve overloaded pattern synonym _∷_, since candidates
have different shapes:
pattern _∷_ x xs = lcons x xs
at pattern-synonyms.lagda.rst:51,13-16
pattern _∷_ ys y = vcons y ys
at pattern-synonyms.lagda.rst:52,13-16
(hint: overloaded pattern synonyms must be equal up to variable and
constructor names)
when checking that the clause lmap f (x ∷ xs) = f x ∷ lmap f xs has
type {A B : Set} → (A → B) → List A → List B
재접기 (Refolding)
각 패턴 pattern lhs = rhs에 대해, Agda는 rhs를 lhs로 재접기(refold)하는 DISPLAY 프래그마를 선언해요 (더 자세한 내용은 DISPLAY 프래그마를 참고하세요).