[Agda] Question about colists, musical notation vs coinductive records, and all that

[Guillaume Allais]

Hi William,

In the standard library we use a notion of `Thunk` for sized codata.
This gives you definitions that look essentially like the ones using
musical notations but on which you can define more compositional
operations thanks to sized types.

You can find colist here:
http://agda.github.io/agda-stdlib/Codata.Colist.html

And what you call transcript corresponds to our cowriter:
http://agda.github.io/agda-stdlib/Codata.Cowriter.html

Both come with various functions, including an `unfold` one that is
a generalisation of your `iterate` where we distinguish between the
type of the internal state and the type of the values outputted in
the codatatype.

Best,
guillaume


On 29/04/2020 17:58, William Harrison 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/ef948c10/attachment.sig>