[Agda] coinductively defined families

[Jesper Cockx]

Probably you know you can already write this:

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Vec (A : Set) (n : Nat) : Set where
  inductive
  field
    hd : ∀ {m} → n ≡ suc m → A
    tl : ∀ {m} → n ≡ suc m → Vec A m
open Vec

[] : ∀ {A} → Vec A 0
[] .hd ()
[] .tl ()

_∷_ : ∀ {A n} → A → Vec A n → Vec A (suc n)
(x ∷ xs) .hd refl = x
(x ∷ xs) .tl refl = xs

but I agree that having syntax for indexed records would be a nice thing to
have. One problem with it is that your proposed syntax would break all
existing code with records in it.

I was actually thinking recently of going in the opposite direction and
making indexed datatypes behave more like records, so you could have
projections and eta-laws when there's only a single possible constructor
for the given indices (as would be the case for vectors).

-- Jesper


On Wed, Mar 7, 2018 at 2:58 PM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Using coinductive types as records I can write
>
>     record Stream (A : Set) : Set where
>         coinductive
>         field
>           hd : A
>           tl : Stream A
>
> and then use copatterns to define cons (after open Stream)
>
>     _∷_ : {A : Set} → A → Stream A → Stream A
>     hd (x ∷ xs) = x
>     tl (x ∷ xs) = xs
>
> Actually I wouldn't mind writing
>
>     record Stream (A : Set) : Set where
>       coinductive
>       field
>         hd : Stream A → A
>         tl : Stream A → Stream A
>
> as in inductive definitions we also write the codomain even though we know
> what it has to be. However, this is more interesting for families because
> we should be able to write
>
>     record Vec (A : Set) : ℕ → Set where
>       coinductive
>       field
>         hd : ∀{n} → Vec A (suc n) → A
>         tl : ∀{n} → Vec A (suc n) → Vec A n
>
> and we can derive [] and cons by copatterns:
>
>     [] : Vec A zero
>     [] ()
>
>     _∷_ : {A : Set} → A → Vec A n → Vec A (suc n)
>     hd (x ∷ xs) = x
>     tl (x ∷ xs) = xs
>
> here [] is defined as a trivial copattern (no destructor applies).
> Actually in this case the inductive and the coinductive vectors are
> isomorphic. A more interesting use case would be to define coinductive
> vectors indexed by conatural numbers. And I have others. :-)
>
> Maybe this has been discussed already? I haven't been able to go to AIMs
> for a while.
> 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.
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180307/e1bd01ee/attachment.html>