코패턴
코패턴 (Copatterns)
참고: 공유도 레코드와 함께 코패턴을 사용하는 방법에 대한 정보를 찾고 있다면 공유도(coinduction) 섹션을 방문하세요.
다음 레코드를 생각해 봐요:
record Enumeration (A : Set) : Set where
constructor enumeration
field
start : A
forward : A → A
backward : A → A
이것은 타입 A의 원소를 따라 이동할 수 있게 해주는 인터페이스를 제공해요.
예를 들어 타입 A의 "세 번째" 원소를 얻을 수 있어요:
open Enumeration
3rd : {A : Set} → Enumeration A → A
3rd e = forward e (forward e (forward e (start e)))
또는 주어진 a에서 시작해 2 위치를 뒤로 갈 수 있어요:
backward-2 : {A : Set} → Enumeration A → A → A
backward-2 e a = backward (backward a)
where
open Enumeration e
이제 이 메서드들을 자연수에 사용하고 싶어요. 이를 위해 Enumeration Nat 타입의 레코드가 필요해요. 코패턴이 없다면 모든 필드를 하나의 표현식으로 지정해야 해요:
open Enumeration
enum-Nat : Enumeration Nat
enum-Nat = record
{ start = 0
; forward = suc
; backward = pred
}
where
pred : Nat → Nat
pred zero = zero
pred (suc x) = x
test₁ : 3rd enum-Nat ≡ 3
test₁ = refl
test₂ : backward-2 enum-Nat 5 ≡ 3
test₂ = refl
필드 하나를 구현하기 위해 자동 케이스 분할과 패턴 매칭을 사용하려면 별도의 정의로 해야 한다는 점을 주의하세요.
코패턴을 사용하면 함수에 대해 서로 다른 경우를 주는 것과 같은 방식으로 레코드의 필드를 별도의 선언으로 정의할 수 있어요:
open Enumeration
enum-Nat : Enumeration Nat
start enum-Nat = 0
forward enum-Nat n = suc n
backward enum-Nat zero = zero
backward enum-Nat (suc n) = n
두 경우의 결과 동작은 동일해요:
test₁ : 3rd enum-Nat ≡ 3
test₁ = refl
test₂ : backward-2 enum-Nat 5 ≡ 3
test₂ = refl
함수 정의에서의 코패턴 (Copatterns in function definitions)
실제로 0에서 시작할 필요는 없어요. 사용자가 시작 원소를 지정할 수 있게 할 수 있어요.
코패턴이 없으면 함수 선언에 추가 인자만 더하면 돼요:
open Enumeration
enum-Nat : Nat → Enumeration Nat
enum-Nat initial = record
{ start = initial
; forward = suc
; backward = pred
}
where
pred : Nat → Nat
pred zero = zero
pred (suc x) = x
test₁ : 3rd (enum-Nat 10) ≡ 13
test₁ = refl
코패턴을 사용하면 함수 인자가 레코드의 각 필드마다 한 번씩 반복되어야 해요:
open Enumeration
enum-Nat : Nat → Enumeration Nat
start (enum-Nat initial) = initial
forward (enum-Nat _) n = suc n
backward (enum-Nat _) zero = zero
backward (enum-Nat _) (suc n) = n
패턴과 코패턴의 혼합 (Mixing patterns and copatterns)
임의의 값을 허용하는 대신 사용자를 0 또는 42라는 두 선택으로 제한하고 싶어요.
코패턴이 없다면 사용자가 제공한 플래그에 따라 어떤 값으로 시작할지 선택하는 보조 정의가 필요해요:
open Enumeration
if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else _ = x
if false then _ else y = y
enum-Nat : Bool → Enumeration Nat
enum-Nat ahead = record
{ start = if ahead then 42 else 0
; forward = suc
; backward = pred
}
where
pred : Nat → Nat
pred zero = zero
pred (suc x) = x
코패턴을 사용하면 패턴 매칭으로 케이스 분석을 직접 할 수 있어요:
open Enumeration
enum-Nat : Bool → Enumeration Nat
start (enum-Nat true) = 42
start (enum-Nat false) = 0
forward (enum-Nat _) n = suc n
backward (enum-Nat _) zero = zero
backward (enum-Nat _) (suc n) = n
팁: 코패턴을 사용해 레코드 타입의 원소를 정의할 때는 레코드의 필드가 스코프 안에 있어야 해요. 위 예제에서는
open Enumeration으로 레코드의 필드를 스코프로 가져왔어요.
첫 번째 예제를 생각해 봐요:
enum-Nat : Enumeration Nat
start enum-Nat = 0
forward enum-Nat n = suc n
backward enum-Nat zero = zero
backward enum-Nat (suc n) = n
Enumeration 레코드의 필드(특히 start 필드)가 스코프에 없으면 Agda는 첫 번째 코패턴이 무엇을 의미하는지 알아낼 수 없어요:
Could not parse the left-hand side start enum-Nat
Operators used in the grammar:
None
when scope checking the left-hand side start enum-Nat in the
definition of enum-Nat
해결책은 필드를 사용하기 전에 레코드를 여는 것이에요:
open Enumeration
enum-Nat : Enumeration Nat
start enum-Nat = 0
forward enum-Nat n = suc n
backward enum-Nat zero = zero
backward enum-Nat (suc n) = n