Copatterns
Note
If you are looking for information on how to use copatterns with coinductive records, please visit the section on coinduction.
Consider the following record:
record Enumeration (A : Set) : Set where
constructor enumeration
field
start : A
forward : A → A
backward : A → A
This gives an interface that allows us to move along the elements of a
data type A
.
For example, we can get the “third” element of a type A
:
open Enumeration
3rd : {A : Set} → Enumeration A → A
3rd e = forward e (forward e (forward e (start e)))
Or we can go back 2 positions starting from a given a
:
backward-2 : {A : Set} → Enumeration A → A → A
backward-2 e a = backward (backward a)
where
open Enumeration e
Now, we want to use these methods on natural numbers. For this, we need
a record of type Enumeration Nat
. Without copatterns, we would
specify all the fields in a single expression:
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
Note that if we want to use automated case-splitting and pattern matching to implement one of the fields, we need to do so in a separate definition.
With copatterns, we can define the fields of a record as separate declarations, in the same way that we would give different cases for a function:
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
The resulting behaviour is the same in both cases:
test₁ : 3rd enum-Nat ≡ 3
test₁ = refl
test₂ : backward-2 enum-Nat 5 ≡ 3
test₂ = refl
Copatterns in function definitions
In fact, we do not need to start at 0
. We can allow the user to
specify the starting element.
Without copatterns, we just add the extra argument to the function declaration:
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
With copatterns, the function argument must be repeated once for each field in the record:
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 co-patterns
Instead of allowing an arbitrary value, we want to limit the user to
two choices: 0
or 42
.
Without copatterns, we would need an auxiliary definition to choose which value to start with based on the user-provided flag:
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
With copatterns, we can do the case analysis directly by pattern matching:
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
Tip
When using copatterns to define an element of a record type,
the fields of the record must be in scope. In the examples above,
we use open Enumeration
to bring the fields of the record into
scope.
Consider the first example:
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
If the fields of the Enumeration
record are not in scope (in
particular, the start
field), then Agda will not be able to
figure out what the first copattern means:
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
The solution is to open the record before using its fields:
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