[Agda] coinductively defined families

[Jesper Cockx]

Oh, and here's the CoVec example:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record CoNat : Set where
  coinductive
  field
    iszero : Bool
    pred   : iszero ≡ false → CoNat
open CoNat

zero : CoNat
zero .iszero    = true
zero .pred   ()

suc : CoNat → CoNat
suc x .iszero      = false
suc x .pred   refl = x

inf : CoNat
inf .iszero      = false
inf .pred   refl = inf

record CoVec (A : Set) (n : CoNat) : Set where
  coinductive
  field
    hd :       n .iszero ≡ false  → A
    tl : (pf : n .iszero ≡ false) → CoVec A (n .pred pf)
open CoVec

[] : {A : Set} → CoVec A zero
[] .hd ()
[] .tl ()

_∷_ : {A : Set} {n : CoNat} → A → CoVec A n → CoVec A (suc n)
(x ∷ xs) .hd refl = x
(x ∷ xs) .tl refl = xs

repeat : {A : Set} → A → CoVec A inf
repeat x .hd refl = x
repeat x .tl refl = repeat x


-- Jesper

On Wed, Mar 7, 2018 at 3:20 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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@
> 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/3a72e2fa/attachment.html>