[Agda] Getting codata right

[Conor McBride]

Hi Anton

Thanks for this careful exposition. It
certainly clarifies things to distinguish
the negative coalgebras from the positive
observations they admit.

There are still a few things I wish I
understood more clearly, relating to /weak/
finality. Not very far away, there are the
inevitable issues of extensionality.

On 8 Jun 2008, at 01:15, Anton Setzer wrote:

> 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

This raises the question of what should
happen with dependent functions. Suppose
I write

   f : (n : coNat) -> T n

The translation you give would mean that

   f (~ Z) = ? {- T n -}
   f (~ (S k)) = ? {- T n -}

That is, both ?s have type T n, now out of
scope. Is that what you have in mind?
I'm guessing that's an intended feature,
because, much as with functions, we
shouldn't imagine that we can learn
what's actually "inside the box" in an
intensional theory. Dependent case analysis
on the codata itself asserts "every coNat
is Z or S", and, up to definitional equality
in the empty context, that's just not true.
(What if it were to become true, as Andreas
and I suspect might be possible?)

We should rather hope, though, that

   f : (n : coNat) -> U (n *)

will result in

   f (~ Z) = ? {- U Z -}
   f (~ (S k)) = ? {- U (S k) -}

even if it takes a bit of magic-with to
make that work. Is this also what you
intend? Could sense be made of the
notation

   f : ((~ n) : coNat) -> U n

just to reduce the burden of abstraction?

This seems safe...but frustrating in the
usual way. The idea that "all T can do
with n is * it", as with, "all you can
do with a function is apply it" is not
captured within the system, so you need
to expose and reason about those
observations as they happpen.

[..]

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

Let me repeat my usual remark at this
point, also echoing Hank's request to
be more aware of the distinction.
General (co)inductive families, can be
factored into restricted families with
equational constraints, if you have a
suitably equality around for the index
types. The question, as ever is "what
is equality?". One might give the
traditional "Ford" expansion

codata _bisim_ : coNat -> coNat -> Set where
   pZ : (n m : coNat) ->
        n * == Z -> m * == Z ->
        n bisim m
   pS : (n m n' m' : coNat) ->
        n * == S n' -> m * == S m' ->
        n' bisim m' -> n bisim m

where _==_ is whatever equality on the
observations you're prepared to put up with
(the intensional one, perhaps, or something
mutually defined with _bisim_). Crucially,
once again, the constraints apply only to
the observations: the codata themselves
remain ineffable.

[..]

I'm inclined to agree that weak finality
is all that's really been "paid for",
given the current definitional and
propositional equalities lying around.
However, I do feel inclined to speculate
that if can figure out how to put more
in, we might get more out. It's certainly
interesting to try and find out what extra
would be required to pay for strong
finality. At this stage, I just don't know,
but I think there are things worth trying
(and I'm trying them).

I fear it may be useful to worry about
coinduction and equality together.

All the best

Conor