[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-16 17:34, Anton Setzer wrote:

> One solution for the problem with using record in two different
> meanings (for type declaration and record formation) might be to use
> coalg for the type former, record for the term former.

I think "coalg" sounds a bit ugly; coalgebra would be better. However,
since we do not have direct access to the coalgebra but only its domain,
I think the word is a bit misleading. A natural name for the dual to
data would be codata, but that name carries some baggage.

> However there is as well a big problem with the first notation:
> One feels tempted to think the evaluation should be
> 
> map f xs = record
>     head = f (head xs)
>     tail = map f (tail xs)
>           = record
>                     head = f (head (tail xs))
>                     tail     = map f (tail (tail xs))
>                               = ...

One would have to teach people that the record keyword blocks evaluation
until a destructor is applied. It seems like a bad idea to block
evaluation for non-recursive records, though. Maybe we should have
separate keywords after all, or go for the approach which only has one
coinductive type per universe level.

Andreas Abel suggested that ♭ and ♯_ should be inserted automatically,
using some subtyping mechanism. I am not sure if this is a good idea,
because it might be confusing, but it would reduce clutter. It would
also mean that we can keep records as they are today (or with some
improvements), but still have general coinductive records with no
syntactic overhead.

> What about
> 
> map (record { proj₁ = n }) = 2 + n

Sorry, what I meant with

   map (λ record { proj₁ = n } → 2 + n)

was an application of the map function to a lambda abstraction. (It
ought to be possible to pattern match on records in lambdas.)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.