[Agda] Question about colists, musical notation vs coinductive records, and all that
Eric Finster
ericfinster at gmail.com
Wed Apr 29 20:49:37 CEST 2020
Hi Bill,
I would have written this:
record Colist (A : Set) : Set where
constructor hd
coinductive
field
Hd : Maybe (A × Colist A)
open Colist
iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
Hd (iterate1 {A} f a) = Just (a , loop (f a))
where loop : Maybe A → Colist A
loop Nothing = hd Nothing
loop (Just a') = iterate1 f a'
Is that what you had in mind?
Best,
Eric
On Wed, Apr 29, 2020 at 6:58 PM William Harrison
<william.lawrence.harrison at gmail.com> wrote:
>
> Hi-
>
> I have a question about the best way to handle colists — aka, potentially infinite lists as opposed to streams — in Agda. I give some examples below in Haskell and Agda, and I’ve also attached *.hs and *.agda files with complete, stand-alone definitions.
>
> In Haskell, the built-in iterate function always produces an infinite list:
>
> iterate :: (a -> a) -> a -> [a]
> iterate f a = a : iterate f (f a)
>
>
> This can be represented in Agda using a Stream (defined as a coinductive record):
>
> iterate : ∀ {a} → (a → a) → a → Stream a
> hd (iterate f a) = a
> tl (iterate f a) = iterate f (f a)
>
>
> Now, back in Haskell, we can define a *potentially* infinite list by introducing Maybe in the codomain of f:
>
> iterate1 :: (a -> Maybe a) -> a -> [a]
> iterate1 f a = a : case f a of
> Just a1 -> iterate1 f a1
> Nothing -> []
>
>
> Using the musical notation for coinduction in Agda, I can get something similar:
>
> data Colist (A : Set) : Set where
> [] : Colist A
> _∷_ : A → (∞ (Colist A)) → Colist A
>
> iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
> iterate1 f a = a ∷ ♯ (case f a of
> λ { (just a₁) → (iterate1 f a₁)
> ; nothing → []
> })
>
>
> My question is, how do I use coinductive records to define Colist rather than musical notation. Is there a standard approach? That isn’t clear. I'm supposing that musical notation should be avoided.
>
> What I’m really trying to define is analogous functions to iterate for what I’ll call the transcript data type, defined below in Haskell and Agda:
>
> data T e a = e :<< T e a | V a — a "transcript"; like a list with an "answer"
>
> data T (e : Set) (a : Set) : Set where
> V : a → T e a
> _<<_ : e → ∞ (T e a) → T e a
>
>
> All these definitions are given in the attached files.
>
> Thanks!
> Bill
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list