[Agda] Getting codata right

[Anton Setzer]

Conor McBride wrote:
> 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?
If we translate the above into real syntax, we would get

f : (n : coNat) -> T n
f n with n *
... | Z -> ?   {- T n -}
... | (S k) -> ? {- T n -}

so the goal is really T n.
The trouble is that the with construct, as I understand it,
wouldn't allow us to know in those cases that
n * = Z or n * = S k,
so we wouldn't get, if T n = U (n *)
that
in the first case the goal is U Z
and in the second case the goal is U (S k)
(unless we use the tricks to work around in this situation)

I feel one could clarify this more by modifying the notation
in case the goal depends on n and have a notation like

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

Of course the proper workaround, in case T n = U (n *) would be to define

f : (n : coNat) -> T n
f n = g (n *)

g : (n : coNat') -> U n
g Z' = ?
g (S' n') = ?


This example by the way seems to indicate that it is
not completely unavoidable to have notations for
coNat',  Z', S'   (it's probably not good to use ' in this case),
although I would prefer if one could avoid it.



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

I think the magic here has to do with the problem of
the with construct.
> 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?
>
I have the feeling the mutual definition of f and g
mentioned above would be the right way of dealing with this problem.
Having an f of this time seems to me to have a similar character as having

g : (S n : Nat) -> U n

> 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.
>
I think I have to weaken my statement here:
We can have general indexed coinductive types, since they reduce essentially
to general indexed inductive types:


codata C : Nat -> Set where
    C0 : C Z
    C1 : (n : Nat, C (S n)) -> C n

stands for

coalg C : Nat -> Set where
  -* : { n : Nat} -> C n -> C' n

data C' : Nat -> Set where
   C0 : C' Z
   C1 : (n : Nat, C (S n)) -> C' n

The problem is that ~ can only occur on in pattern matching,
and not on the right hand side in a general inductive or coinductive type.

data isZero: coNat -> Set where
    iszero : isZero (~ Z)
doesn't make much sense to me because
what is the type of iszero?

If one replaces it by
data isZero : coNat -> Z where
   iszero : isZero Z

then we would have
iszero : isZero Z

but if we define

a : coNat
a ~ Z
then we wouldn't get

iszero : isZero a

The way around is to shift the pattern matching to the right by for
instance defining

IsZero : coNat -> Set
IsZero (~ Z) = True
IsZero (~ (S n)) = False

where in more complicated examples one would define
some of the cases simultaneously inductively or coinductively.




> 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.
>
Finality of coalgebras gives you extensional equality on
Nat -> Nat
since
there every f : Nat -> Nat can be converted into a stream
stream f
such that
f and g are extensionally equal if and only if stream f and stream g
are bisimilar
I assume you can take your observational type theory approach
and extend it to coalgebras and then get some kind of notion
of final coalgebras.

> All the best
>
> Conor
>


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