Agda copatterns (Release notes for Agda 2 version 2.3.4)

agda-copatterns.md

Experimental feature: copatterns. (Activated with option --copatterns)

We can now define a record by explaining what happens if you project the record. For instance:

{-# OPTIONS --copatterns #-}

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

Taking a projection on the left hand side (lhs) is called a projection pattern, applying to a pattern is called an application pattern. (Alternative terms: projection/application copattern.)

In the first example, the symbol 'pair', if applied to variable patterns a and b and then projected via fst, reduces to a. 'pair' by itself does not reduce.

A typical application are coinductive records such as streams:

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

Again, 'repeat a' by itself will not reduce, but you can take a projection (head or tail) and then it will reduce to the respective rhs. This way, we get the lazy reduction behavior necessary to avoid looping corecursive programs.

Application patterns do not need to be trivial (i.e., variable patterns), if we mix with projection patterns. E.g., we can have

nats : Nat -> Stream Nat
head (nats zero) = zero
tail (nats zero) = nats zero
head (nats (suc x)) = x
tail (nats (suc x)) = nats x

Here is an example (not involving coinduction) which demostrates records with fields of function type:

-- The State monad

record State (S A : Set) : Set where
  constructor state
  field
    runState : S → A × S
open State

-- The Monad type class

record Monad (M : Set → Set) : Set1 where
  constructor monad
  field
    return : {A : Set}   → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B


-- State is an instance of Monad
-- Demonstrates the interleaving of projection and application patterns

stateMonad : {S : Set} → Monad (State S)
runState (Monad.return stateMonad a  ) s  = a , s
runState (Monad._>>=_  stateMonad m k) s₀ =
  let a , s₁ = runState m s₀
  in  runState (k a) s₁

module MonadLawsForState {S : Set} where

  open Monad (stateMonad {S})

  leftId : {A B : Set}(a : A)(k : A → State S B) →
    (return a >>= k) ≡ k a
  leftId a k = refl

  rightId : {A B : Set}(m : State S A) →
    (m >>= return) ≡ m
  rightId m = refl

  assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
    ((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
  assoc m k l = refl

Copatterns are yet experimental and the following does not work:

• Copatterns and 'with' clauses.

• Compilation of copatterns to Haskell, JS, or Epic.

• Projections generated by open R {{...}} are not handled properly on lhss yet.

• Conversion checking is slower in the presence of copatterns, since stuck definitions of record type do no longer count as neutral, since they can become unstuck by applying a projection. Thus, comparing two neutrals currently requires comparing all they projections, which repeats a lot of work.