[Agda] Tentative guidelines for working with coinductive types

[Anton Setzer]

Nils Anders Danielsson wrote:
> 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.
>

I think one keyword for both is a neat solution. "record" might confuse
people,
since they don't expect coalgebras. On the other hand probably people might
get used to it. 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. But I don't have
a strong
point of view here.
> 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)
>

I find the first notation very neat. "record" serves here as a nice bracket
around the different components to be defined.

In some cases one need to have arguments for record components:

record A : Set where
    f1 : Nat
    f2 : Nat -> A

a : Nat -> A
a n = record
              f1 = n
              f2 m = a m

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

The second notation makes it clear that
deeper evaluations require the use of tail,
so
tail (tail xs)  = map f (tail (tail xs))

whereas
 
tail xs = map f (tail xs)
doesn't evaluate any further if xs is a variable.

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

sounds plausible to me.
> 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 : ...
>

Seems a good idea to me.
> 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)
>
What about

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

and in the second case (I like the 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.
>
I have the feeling we are making some progress in this issue.

Anton


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