# 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
```