add examples of copattern/coinductive data to the std-lib?

[cartazio]

i've written 1-2 tiny examples, and something akin to them should perhaps be in the STD-lib now that copatterns are gonna be on by default?

https://gist.github.com/cartazio/3873e805ad288e52ece7
https://gist.github.com/cartazio/a7f8c7adf2c6c68adcfb

are the tiny ones i've done,
but the point being, some concrete examples in the std-lib / read the docs manual is probably a good idea?

[MatthewDaggitt]

Examples are always good, but as these are demonstrating how language features work, rather than providing useful, reusable code, they should be in the docs rather than the standard library. I would open an issue in the main Agda repository where the documentation can be found.

[andreasabel]

We could have .Example or .Examples modules in the std-lib [or a whole Examples. hierarchy]. Sometimes an API is hard to comprehend without examples.

[MatthewDaggitt]

I quite like the idea of .Examples modules but in this particular case these examples are demonstrating features of the Agda language, not features of the standard library (the first one doesn't even have a dependency on the library!). Surely they should live elsewhere?

[gallais]

Isn't the README directory the right place to keep adding examples and use cases?

[andreasabel]

Right, general examples could go into README, specific ones into a .Examples module.

Examples for the Agda language should not go into the standard library, but in the Agda documentation. However, maybe @cartazio meant that the standard library does not make use of copatterns and maybe should.

[cartazio]

A bit of both :)

…

On Thu, Jun 29, 2017 at 5:17 AM Andreas Abel ***@***.***> wrote: Right, general examples could go into README, specific ones into a .Examples module. Examples for the Agda language should not go into the standard library, but in the Agda documentation. However, maybe @cartazio <https://github.com/cartazio> meant that the standard library does not make use of copatterns and maybe should. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#84 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAAQwlXNrsiehS32ijokKKk83mzd_Edkks5sI2u6gaJpZM4HvaT_> .

[gallais]

I have experimented a bit with Conat and I guess this leads to asking some questions about the kind of conventions we want to adopt:

https://github.com/gallais/agda-stdlib/blob/codata/src/Codata/Conat.agda
https://github.com/gallais/agda-stdlib/blob/codata/src/Codata/Conat2.agda
https://github.com/gallais/agda-stdlib/blob/codata/src/Codata/Conat3.agda

Should we:

• have the Size index implicit or explicit?
• use Size<_ style or ↑_ style?
• have a mutually defined sum Coℕ and the ∞Coℕ coinductive record or just one codatatype? (I couldn't even define _⊔_ with these mutually defined types... maybe someone else will have more success than me)

[andreasabel]

https://github.com/gallais/agda-stdlib/blob/codata/src/Codata/Conat.agda
https://github.com/gallais/agda-stdlib/blob/codata/src/Codata/Conat2.agda

These two implement just sized natural numbers, nothing coinductive here.

The third one actually implements co-natural numbers.

We should:

• have the Size index explicit in the type and implicit in the term
• use Size< for coinductive types
• do the mutually defined thing for codata types with more than one "constructors" (does not work otherwise)

Here is a definition of the maximum function based on your code:

open import Size
open import Data.Nat.Base as ℕ using (ℕ)
open import Function

data    Coℕ (i : Size) : Set
record ∞Coℕ (i : Size) : Set

data Coℕ i where
  zero : Coℕ i
  suc  : ∞Coℕ i → Coℕ i

record ∞Coℕ i where
  coinductive
  field force : {j : Size< i} → Coℕ j
open ∞Coℕ public

fromℕ  : ℕ → Coℕ ∞
∞fromℕ : ℕ → ∞Coℕ ∞

fromℕ ℕ.zero    = zero
fromℕ (ℕ.suc m) = suc (∞fromℕ m)

force (∞fromℕ m) = fromℕ m

infixl 5 _⊔_ -- _⊓_
-- infixl 6 _+_ _∸_
-- infixl 7 _*_

_⊔_  : {i : Size} → Coℕ i → Coℕ i → Coℕ i
_∞⊔_ : {i : Size} → ∞Coℕ i → ∞Coℕ i → ∞Coℕ i

zero  ⊔ n     = n
m     ⊔ zero  = m
suc m ⊔ suc n = suc (m ∞⊔ n)

force (m ∞⊔ n) = force m ⊔ force n

[gallais]

These two implement just sized natural numbers, nothing coinductive here.

Indeed. I don't know what I was thinking.

Here is a definition of the maximum function based on your code:

Oh, so you need the two conats to be 'as much defined'. Makes sense, I guess. I need to build a better intuition for these things.

[MatthewDaggitt]

Hmm so we do actually have Conat, Cofin, Colist and Covec modules already, although they don't use sized types and they're a little bare bones.

[andreasabel]

The intuition here is that n : CoNat i is a process which guarantees a request depth i. If i > 0, you can send it a force request and it comes back with one of the two answers zero or suc m. The new process m : CoNat j has a request depth j <= i+1 which you can actually choose when sending the force request. Case i=omega guarantees infinite request depth.

When you add two CoNats (or compute minimum or maximum), the two CoNats have to have at least the request depth of the produced CoNat. Look at the cases for zero to understand why!

[MatthewDaggitt]

I'm going to close this given that we do have some examples of coinductive data in the library. If anyone has done or will do further work on them, please feel free to submit pull requests.