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

[Setzer A.G.]

Please note that the paper of Ulrich Berger and myself
Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types<http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf>, doi 10.1007/978-3-030-00389-0_4<https://doi.org/10.1007/978-3-030-00389-0_4>  In: Corina Cirstea (Ed): Coalgebraic Methods in computer Science. Springer Lectuer Notes in Computer Science 11202, 2018.
http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf

contains a discussion how the musical notation can be interpreted in the coalgebra approach (so is just a form of syntactic sugar)

Anton



________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of William Harrison <william.lawrence.harrison at gmail.com>
Sent: 29 April 2020 17:58
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: [Agda] Question about colists, musical notation vs coinductive records, and all that

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/20200430/b3763ead/attachment.html>