[Agda] Coinductive families

[Anton Setzer]

On 05/10/10 02:00, Dan Doel wrote:
> On Monday 04 October 2010 8:45:42 pm Anton Setzer wrote:
>   
>> Although a record is close to a coalgebra, I think there are two problems:
>>
>> - in Agda record types have the eta rule, which leads to
>> non-normalisation in coalgebras.
>>    Restricting it for recursive types and allowing it for non-recursive
>> types seems to me confusing for the
>>    user.
>> If we define
>>
>> a : Stream
>> a  = record{head = 0; tail = a }
>>
>> misleads the user into thinking that this will expand to
>>
>> a = record{head = 0; tail = record{head = 0; tail = record{  ... }}}
>>
>> Even if s/he doesn't expect this, she might expect some partial expansion.
>>     
> Yes, I didn't mean to suggest (if I did) that eta would work with recursive 
> records. Unfortunately, I know of no way to get equality of coinductive types 
> via bisimulation without adopting some level of extensionality. 

If you want bisimulation equality you have to accept extensionality.
Take the streams

g 0 :: g 1 :: g 2 :: g 3 ::
and
h 0 :: h 1 :: h 2 :: h 3 ::

They are bisimilar if
g and h are extensionally equal.

However one can define bisimulation equality on coalgebras, e.g.
for streams

coalg _bisim_ {A : Set} : Stream A -> Stream A -> Set where
   headeq : (l l' : Stream A) ->  l bisim l' -> head l == head l'
   taileq     : (l l' : Stream A) -> l bisim l'  -> (tail l) bisim (tail l')

and then prove that certain streams are equal by guarded recursion.

If you want any reasonable equality on colagebras you become extensional.
We have to live with the fact that definitional equality on coalgebras
is similar to
definitional equality on functions:
two functions are the same if the algorithm producing them is equal
two streams are the same if the programs generating them are the same.

The mistakes with coalgebras in Agda in the past was that
people said: I want these two streams to be the same. And when you
make a bit too much the same, then you get the problem of either
substitution of equal terms doesn't give equal results, or you end
up with non-normalisation.

There is a little article by myself and Peter Hancock (unfortunately
only a report)
which gives rules for coalgebras in dependent type theory with a suitable
definitional equality (based on what I said before).

http://www.cs.swan.ac.uk/~csetzer/articles/dagstuhl2004.pdf

http://www.cs.swan.ac.uk/~csetzer/articles/dagstuhl2004.bib

Anton


> And yes, it 
> would be strange for eta to work sometimes and not others.
>
> I just thought it was worth noting that eta can correspond to coinduction as 
> well as induction, and that, being:
>
>   unfold observe x = x
>
> if we think of 'record { proj1 = e1 ; proj2 = e2 ... }' as specifying what the 
> projections of the value being defined will be, it looks more like coinduction 
> than induction. But perhaps I'm biased.
>
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>   


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