Copatterns

Motivation

So, what are copatterns, and why do we want them?

Essentially, copatterns allow us to make projections on the left-hand side of function definitions. Left-hand side projections make sense for definitions from which we primarily want to extract data, contrary to injecting data into data constructors. Examples include record types and coinductive types.

Observation vs. Construction

Copatterns can make our lives easier. For a standard record type Person with fields 'name' and 'age', copatterns allow us to define a person like this:

john : Person
name john = "John"
age  john = 30

Instead of the arguably more hideous:

john : Person
john = MkPerson "John" 30

Copatterns thus allow us to think in terms of "What can I observe about this piece of (co)data?" (when I observe John's age, the number 30 should be extracted) instead of "How can I construct this piece of (co)data?" (when constructing John, the number 30 is injected as his age).

Syntax

It is not currently possible to write and run any of the examples in this section. They are merely suggestions for a possible syntax.

Records

Records could be defined directly in terms of the observations we can make on them:

record Person : Type where
  name : Person -> String
  age  : Person -> Nat
  constructor MkPerson name age

Codata

We envision that codata definitions could look as follows:

codata Stream : Type -> Type where
  head : Stream a -> a
  tail : Stream a -> Stream a
  constructor (::) head tail

This would serve as a uniform way of defining codata in terms of projections, while still allowing the current constructor-based approach to codata. With codata definitions based on projections, we can write functions on them in terms of copatterns:

map : (a -> b) -> Stream a -> Stream b
head (map f s) = f (head s)
tail (map f s) = map f (tail s)

nats : Stream Nat
head nats = Z
tail nats = map S nats

While this can seem more verbose than defining the same functions in terms of constructors, it does allow users to move away from thinking of codata as "constructing infinite syntax trees", instead defining codata in terms of observations.

Infix copatterns

For projections returning functions, infix copatterns could make sense. Consider a (rather contrived) transition system, where a state is labeled with a string and has a transition function, determining the next state based on some input parameter:

codata State : Type -> Type -> Type where
  label     : State a b -> a
  withInput : State a b -> (b -> State a b)

stateA : State String Nat
label stateA              = "A"
stateA `withInput` Z      = stateA
stateA `withInput` (S n') = stateB

stateB : State String Nat
label stateB            = "A"
stateB `withInput` Z      = stateB
stateB `withInput` (S n') = stateA

While the infix copatterns does add some value in this case, the general usefulness of having infix copatterns might be questionable.