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

[William Harrison]

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






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/4c8f872c/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ColistQuestion.hs
Type: application/octet-stream
Size: 775 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/4c8f872c/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/4c8f872c/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ColistQuestion.agda
Type: application/octet-stream
Size: 1239 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/4c8f872c/attachment-0001.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/4c8f872c/attachment-0002.html>