[Agda] why coinductive?

[Henning Basold]

On 02/03/2020 11:17, Thorsten Altenkirch wrote:
>     > 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.
>     

I see. Thanks for the reference!

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

I guess, like any naming scheme. However, even in quantum physics one
talks about states and observations, even though making an observation
has a detrimental effect on a state. Moreover, observations there do not
give you the full information to recover the state either. In the end,
we will probably just stick to our personal preferences :)

Henning

> Thorsten
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 2472 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200302/2f3c2786/attachment.bin>