[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-15 19:22, Anton Setzer wrote:
>
> In some sense I feel that coalg generalises record types:
>  record is just the degenerated case of a coalg with no recursive
>  occurrence of the type defined.

Yes. If we decide to include general coinductive records, why don't we
simply use the keyword "record" instead of "coalg"? No other keyword is
an abbreviation (as far as I recall), and fewer keywords is often
better.

What notation do you have in mind for defining values of record types?
One could simply use the current record notation, but I would prefer
"record" to be a layout keyword, so that we could drop the braces and
semicolons:

   _,_ : ∀ {A B} (x : A) → B x → Σ A B
   (x , y) = record
     proj₁ = x
     proj₂ = y

   map : ∀ {A B} → (A → B) → Stream A → Stream B
   map f xs = record
     head = f (head xs)
     tail = map f (tail xs)

(There was some problem with this, though. Ulf knows more.) One could
also use something like the following:

   _,_ : ∀ {A B} (x : A) → B x → Σ A B
   proj₁ (x , y) = x
   proj₂ (x , y) = y

   map : ∀ {A B} → (A → B) → Stream A → Stream B
   head (map f xs) = f (head xs)
   tail (map f xs) = map f (tail xs)

This notation has some disadvantages:

* It is a declaration form, rather than an expression.

* One has to repeat the same left-hand side over and over (once per
   projection).

* I think it would be confusing if where clauses scoped over all the
   "branches", and inconvenient/inefficient if they did not.

I think I prefer the record notation. I want to improve it, though. I
think that it should be possible to omit record fields which can be
inferred automatically:

   x : Σ ℕ (λ n → n ≡ 0)
   x = record
     proj₂ = refl  -- proj₁ can be inferred.

It should perhaps also be possible to mark record fields as implicit, so
that they are not printed out unnecessarily:

   record Setoid : Set1 where
     field
       {A : Set}
       _≈_ : A → A → Set
       isEquivalence : ...

Pattern matching for records would also be very nice. (This would be
translated into use of destructors, so I don't think it would break
anything.) However, using the "record" syntax is rather clunky:

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

It would be better if one could (optionally) define a short name for a
record value:

   record Σ (A : Set) (B : A → Set) : Set where
     field
       proj₁ : A
       proj₂ : B proj₁

     name _,_

   map (λ (n , _) → 2 + n)

This name could also be used by Agda when printing record values.

> But these are just my first thoughts about it. I think a broad discussion
> and lots of experiments are needed in order to clarify this issue.

Absolutely. The current implementation of codata was never intended as a
final solution (not by me, anyway), it was implemented so that we could
experiment and get some intuition for the problems at hand.

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