[Agda] coinductively defined families

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512



On 07/03/18 15:31, Andreas Abel wrote:
>> 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

> 
> 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
>> 
> 
> 
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlqhGdoACgkQatBsEc2x
Mm6+iBAAlaDis0XXJFEPPFrrKECZC44XaWAVDj6xQtK4VkOed/e2m5BJdlhdhlCr
/w7QzGUYSj1R6/hz3poWgaPEX/Z8y7Q6PDg9sdwJIkDvW126pXzRdX6jk2m2n8Iu
y3eLWHMXhwridyaueNStcOip8EKjDmmEudSeWN6f2QOZeYW/G8q/ffkfl+81wTht
nuhoyLuczA1aHko0DCp5hYPVPZaHDSaWJsZzio2Tyhe+uvXF+G5oPj8yrh0pjTit
rsHZk7H2+E5ZR5WA3jW6CpC11CLYnzTpVNCDcfh0km4b//KKW9WeL0ZS1kTmZzaB
+j3k5jAZHoLyX7f2+xOyXLPRPSMoZYJqWBk04WmvJTFAyFVOJPTrDeqWVv6Pq+q/
opU8La2F1N+6CEpugz4YXUc/CND6KaiZW7Am3lEoHwDYc3kRwvDKcTsYVG25Hy7+
u2nB91jc20AyXS+BShQK4QhVEWkXzFjgbLNJgiZJIrbnaJlRc/b5mQ4EchyT6VSH
gqurqweFZk6d1jfX84b6aWc4Sc/QBCbExj3RjKETdsq7z3y8uX3OOjwa+nrXwVdj
8Z5gnetoXHP7y05HQg7ddZQU0wUfW/VUo6FlI4tp5rHmCg7sxXOJ8rGh2ZYCE3AE
YSMB8819siBnUNPyKWWRIE0jZdcWN64/DNJE71Q8FprS76709cg=
=O/lm
-----END PGP SIGNATURE-----