[Agda] coinductively defined families

[Andreas Abel]

 > A more interesting use case would be to define coinductive
 > vectors indexed by conatural numbers. And I have others. :-)

A reason against indexed coinductive records was that indexing was 
resolved by propositional equality and that was too weak for interesting 
indices such as conatural numbers.

However, with extensional equality such as in cubical, indexed records 
become more interesting again.

Maybe for now, Jesper's workaround is sufficient.  Then you can also 
work with bisimilarity of CoNats instead of propositional equality and 
that works in vanilla Agda as well.

Cheers,
Andreas

On 07.03.2018 14:58, Thorsten Altenkirch 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
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/