[Agda] why coinductive?

[Thorsten Altenkirch]

    > You are right, I forgot. Btw, one could have eta-expansion for sums but
    > it seems that eta-expansion for records is more popular.
    > 

    What do you mean by that? That every map f : A + B → C is of the form
    λ{in₁ x → f (in₁ x), in₂ x → f (in₂ x)} ?
  
You need a bit more - see our LICS 2001 paper
http://www.cs.nott.ac.uk/~psztxa/publ/lics01.pdf

A problem is that eta equality for coproducts is computationally more expensive and it only works for non-empty coproducts.
    
    > 
    >     Having η for recursive coinductive types would make definitional
    > 
    >     equality undecidable: https://cronfa.swan.ac.uk/Record/cronfa38822
    > 
    >    
    > 
    >     About the destructors, or rather what I would call observations,
    > 
    >  
    > 
    > I prefer destructors because it is nicely dual to constructors.
    > 
    
    I prefer observation because "destructor" sounds, well, destructive ;)
    That is probably also my C++-trained mind, which expects a destructor to
    end an object's life!

Ok, I guess we can discuss this forever but tail : Stream A -> Stream A isn't really an observation.

Thorsten
 




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.