[Agda] coinductively defined families

[Thorsten Altenkirch]

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.

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

Post by Thorsten Altenkirch
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
[] : 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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Jesper Cockx
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

Post by Thorsten Altenkirch
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
[] : 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
https://lists.chalmers.se/mailman/listinfo/agda

[Thorsten Altenkirch]

One problem with it is that your proposed syntax would break all existing code with records in it.

Yes, I just thought about that. One would need to write "destructor" instead of "field". if one wants to include the domain.

Thorsten

From: Jesper Cockx <***@sikanda.be<mailto:***@sikanda.be>>
Date: Wednesday, 7 March 2018 at 14:20
To: Thorsten Altenkirch <***@exmail.nottingham.ac.uk<mailto:***@exmail.nottingham.ac.uk>>
Cc: Agda mailing list <***@lists.chalmers.se<mailto:***@lists.chalmers.se>>
Subject: Re: [Agda] coinductively defined families

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 <***@nottingham.ac.uk<mailto:***@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
***@lists.chalmers.se<mailto:***@lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda





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.

[Andreas Abel]

Post by Thorsten Altenkirch
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

Post by Thorsten Altenkirch
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
    [] : 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
https://lists.chalmers.se/mailman/listinfo/agda

[Henning Basold]

Post by Andreas Abel

Post by Thorsten Altenkirch
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.

I had at some point talked about this at the AIM. Indeed, it would be
nice to have indexed coinductive types, but as Andreas mentions in an
intensional type theory this does not work well. Instead, one needs a
type theory, in which bisimilarity would be included in the
propositional equality (observational type theory any one?). With this
in mind, one would implement covectors, or partial streams as I call
them, just like one would implement indexed inductive types by using
equality. See the code below.

open import Data.Unit
open import Data.Sum

record ℕ∞ : Set where
coinductive
field pred : ⊤ ⊎ ℕ∞
open ℕ∞ public

data Lift {A B : Set} (R : A → B → Set) : ⊤ ⊎ A → ⊤ ⊎ B → Set where
inl : Lift R (inj₁ tt) (inj₁ tt)
inr : ∀ a b → R a b → Lift R (inj₂ a) (inj₂ b)

record _~_ (m n : ℕ∞) : Set where
coinductive
field pred~ : Lift _~_ (pred m) (pred n)

_≈_ : ⊤ ⊎ ℕ∞ → ⊤ ⊎ ℕ∞ → Set
_≈_ = Lift _~_

record PStream (A : Set) (n : ℕ∞) : Set where
coinductive
field
hd : ∀ m → pred n ≈ inj₂ m → A
tl : ∀ m → pred n ≈ inj₂ m → PStream A m


Cheers,
Henning

Post by Andreas Abel
Cheers, Andreas

Post by Thorsten Altenkirch
Using coinductive types as records I can write
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
[] : 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
https://lists.chalmers.se/mailman/listinfo/agda

[Thorsten Altenkirch]

I would assume this as the default by now. Intensional equality for infinite objects is just wrong.

Ok, the implementation is a bit behind but we don’t take every bug as a principle, do we?

Thorsten

On 08/03/2018, 11:09, "Agda on behalf of Henning Basold" <agda-***@lists.chalmers.se on behalf of ***@basold.eu> wrote:

Instead, one needs a
type theory, in which bisimilarity would be included in the
propositional equality (observational type theory any one?).




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.