[Agda] Getting codata right

[Anton Setzer]

I think I have now a suitable understanding
of in what sense codata can be regarded as an abbreviation
for coalgebraic definitions, which includes now as well
a good notation for pattern matching on codata.
Here follows my proposal, which correspond pretty much
to the implementation in Agda at present, with a slight modification
on pattern matching.

I think codata should be a notational convenient way
of dealing with coalgebra, but everything should be reducible
to coalgebras.
Although it would be desirable to have coalgebras directly,
since they probably will soon get their own independent
life, I think one can live with the fact to have only coalgebras
and that codata definitions should only in principal reduce to
codata.

I first repeat slightly more formally the definition of codata as an
abbreviation:

codata A: Set where
   C1 :  (.... , x : C -> A, ...) -> A
   ...
   Ck : ( ....                         ) -> A

is an abbreviation for

mutual
   coalg A : Set where
       _* : A -> A'

  data  A' : Set where
       C1' : ( ... , x : C -> A ,... ) -> A'
       ...
       Ck' : ( ...                          ) -> A'

C1 : ( ... , x : C -> A , ...  ) -> A  where
(C1 ... x .... ) * = C1' ... x ....

Ck : ( ... ) -> A where
(Ck ... x ...) * = Ck' ...

And we have
s ~ t :=    s * = t *
which means we can for instance define
omega : coNat
omega ~ S omega

which means
omega * = S' omega

This means that this part can be used as it is
implemented in Agda.

Concerning pattern matching I suggest that
for instance


f : coNat -> Bool
f (~ Z) = tt
f (~ (S n)) = ff

is an abbreviation for

f : coNat -> Bool
f x with x *
... | Z' = tt
... | (S' n) = ff

If one needs deeper pattern matching one can
for instance define

g : coNat -> Bool
g (~ Z) = tt
g (~ (S (~ Z))) = tt
g (~ (S (~ (S n))) = ff

for

g : coNat -> Bool
g x with x *
... | Z' = tt
... | (S' n) with n *
... | ... | Z' = tt
... | ... | (S' n) = ff

So all one needs is when defining something
by pattern matching is to use the ~.
This guarantees that the equation express exactly what is going on
and don't lead to wrong assumptions about how the unfolding takes place:
In case for f we have
f x is in case x ~ Z equal to tt
         in case x ~ (S n) equal to ff
where checking of
x ~ Z or x ~ (S n) amounds to a one step
application of _* to x.

This avoids getting the false impression that
x must be equal to Z or (S n) to match those patterns,
which then gives the impression that elements of
codata unfold automatically. They only unfold
if one applies _* to them.

With respect to indexed codata I think only the
restricted version (or coinductive families) make to me full sense yet.

Something like
codata _bisim_ : coNat -> coNat -> Set where
    pZ : (~ Z) bisim (~ Z)
    pS : (n m : coNat) -> n bisim m ->  ~ (S n)  bisim ~ (S m)

doesn't make much sense
but something like

mutual
   _bisim_ : coNat -> coNat -> Set where
   (~ Z) bisim (~ Z) = bisimZ
   (~ (S n)) bisim (~ (S m)) = n bisimS m
   (~ _) bisim (~ _) = bisimFalse
 
   codata bisimZ : Set where
       pZ : bisimZ

   codata _bisimS_ : coNat -> coNat -> Set where
        pS : n  bisim m -> n bisimS m

   codata bisimFalse where

makes sense.

Note in the previous example the use of (~ _) which
makes much sense if you look at how it translates into a
statement using 'with'

One interesting case is the empty codata type:

codata emptyset Set where

stands for

mutual
  coalg emtyset : Set where
    _* : emptyset -> emptyset'

  data emptyset' : Set where


Now if we define

f :  emptyset -> A
f (~ ())

this stands for

f : emptyset -> A
f x with (x *)
... | ()

So in summary:
  the notation of Agda as it stands is suitable.
  only in case of pattern matching we need to add those
  ~
  The underlying typechecking terminationchecking mechanism
  needs of course to be investigated to make sure that it
  correlates exactly to the categorial model, otherwise
  we will get oddities.


Anton









-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------