[Agda] Codata oddity

[Anton Setzer]

Nils Anders Danielsson wrote:
> Hi,
>
> The current implementation of codata seems to be a bit problematic.
> The following program was suggested by Nicolas Oury:
>
>   data _≡_ {a : Set} (x : a) : a -> Set where
>     refl : x ≡ x
>
>   codata Stream : Set where
>     cons : Stream -> Stream
>
>   out : Stream -> Stream
>   out (cons xs) = cons xs
>
>   out-≡ : (xs : Stream) -> xs ≡ out xs
>   out-≡ (cons xs) = refl
>
>   ω : Stream
>   ω ~ cons ω
>
>   p : ω ≡ cons ω
>   p = out-≡ ω
>
> If we evaluate p we get refl, but if we replace the right-hand side of
> p with refl we get a type error, so we do not have preservation of
> types.
>
>   
> ------------------------------------------------------------------------
>
>   
I like very much that coalgebras have been added to Agda and I think that's
a necessary step to take. And I think that many things work out nicely
is a real success story.

However, I am worried that we might soon regret such fast success and
the above example demonstrates what happens if one is not 100% clear
about what one is doing.

In my opinion it is important to keep here a clear connection with
category theory and then define some nice abbreviations so that we can
write
code which is as close as possible to equations we want to have (such as
omega = S omega)
without breaking the connection to a clean category theoretic formulation.

In category theory, data is a construct which corresponds to initial
algebras.
E.g. the natural numbers correspond to the initial algebra
intro : 1 + N -> N
where
intro inl = 0
intro (inr n) = S n
or in general
intro : F(X) -> X for some strictly positive functor F

The dual of an initial algebra is a final coalgebra, which is given by
elim : X -> F(X)
In order to obtain decidable type checking one needs to replace final
algebra by weakly final coalgebras, which essentially corresponds
to allowing functions to be defined by guarded recursion,
but there might be several functions satisfying the same guarded
recursion equation.

Following this category theoretic definition, the co-natural numbers
should be defined then as
coalg coNat : Set where
   case : coNat -> Z +  S (n : coNat)

where Z + S(n : coNat) is the same as
data constrCoNat : Set where
  Z : constrCoNat
  S : coNat -> S constrCoNat

Note that this means in particular that
neither Z nor S n are elements of coNat

We can define the element corresponding to zero and successor
in coNat by guarded recursion, namely
Z' : coNat where
  case Z'  = Z

S' : coNat -> coNat where
  case (S' n)  = S n

This doesn't look nice compared with defining something
like codata, but there is a difference between S' n and S n
When using codata one tries to identify S' n and S n  and omit the case
construct
by a  new symbol ~, and suddenly we get a confusion,
because it is not clear when to unfold a guarded recursion
and when not.
If we keep the distinction we see that if we rewrite the above example
slighly as


omega : coNat where
   case omega = S omega

data Eq (n : coNat) : coNat -> Set where
   refl : Eq n n

p : Eq omega (S omega)
p = ?

that Eq omega (S omega) doesn't make any sense.
We can insteadn try

p : Eq omega (S' omega)
p = ?
but now omega and (S' omega) are irreducible elements
(since case is not applied to either of them).

I don't think we will get any clear concepts in Agda by hacking around
this problem.
What we can do is to define good notations and good syntactic sugar
so that we can use something which looks very close to
codata, but which actually is nothing but a good notation for
the real notions coming from category theory, namely coalgebras.


What we came up during the Nottingham dependently typed workshop
in discussions with Ulf and Nils was that a solution for getting good
syntactic
sugar is to have the following:

codata coNat : Set where
   Z : coNat
   S : coNat -> coNat

is syntactic sugar for the following:

coalg coNat : Set where
  -* : coNat -> Z' + S' (n : coNat)

Z : coNat
Z * = Z'

S : coNat -> coNat
(S n) * = S' n

and we have the abbreviation

a ~ b   stands for a * = b *

Then we can essentially hide Z', S' n
and write Z' *, (S n) * for them and then write guarded recursion
equations like

omega : coNat
omega ~ S omega

If we take into account that all of this is just syntactic
sugar (not a hack) which translates back into
coalgebras above, then we can answer questions like

Does
p: Id omega (S omega)
p = refl
make sense?

It doesn't, because (S omega) and omega are elements
which don't reduce unless we apply _* to them
(which looks with this notation as if we have to apply them to *)


However, I think even if we have this nice syntactic sugar,
I think notions like coalg need to be kept,
since when evaluating terms we will most likely end up with
raw terms which are elements of some coalg type.
And it is nice to explain what the syntactic sugar actually means.

     

What about pattern matching?
It looks nice to have something like
f : coNat -> Bool
f Z = tt
f (S n) = ff

But this suggest that if n: coNat then
n = Z or n = S n'
which is not true.
All we have is that
n ~ Z or n ~ S n'
If you do anything else, users will get confused because
then they get the impression that    omega = S omega
which is not the case.

The best notation I could find at present is to say we have

f : coNat -> Bool
f n  with~ n
.. | Z = tt
.. | S n' = ff

as an abbreviation  for
f : coNat -> Bool
f n with n *
.. | Z * = tt
.. | (S n') * = ff

which is the right thing since for every n we have
n ~ Z or n ~ S n'

This is not so nice if we want to have deeper pattern matching like

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

but I don't see yet a way to avoid this,
since for n : coNat we don't have
n ~ Z or n ~ (S Z) or n ~ S (S n') for some n'.
All we have is
n ~ Z or  n ~ (S n') where
    n' ~ Z or n' ~ (S n'') for some n''


This is an attempt to get syntactic sugar which is as close
to the codata construct.
But I think we should make sure that whatever we define
clearly corresponds to the categorical constructs, otherwise
we will sooner or later get a lot of confusion.


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/
---------------------------------------
 
                    
  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080607/e717ed6c/attachment-0001.html