<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><div><blockquote type="cite" class=""><div class=""></div></blockquote><blockquote type="cite" class=""><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">guillaume</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">On 29/04/2020 17:58, William Harrison wrote:</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">Hi-<br class=""><br class="">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.<br class=""><br class="">In Haskell, the built-in iterate function always produces an infinite list:<br class=""><br class="">iterate :: (a -> a) -> a -> [a]<br class="">iterate f a = a : iterate f (f a)<br class=""><br class="">This can be represented in Agda using a Stream (defined as a coinductive record):<br class=""><br class="">iterate : ∀ {a} → (a → a) → a → Stream a<br class="">hd (iterate f a) = a<br class="">tl (iterate f a) = iterate f (f a)<br class=""><br class="">Now, back in Haskell, we can define a *potentially* infinite list by introducing Maybe in the codomain of f:<br class=""><br class="">iterate1 :: (a -> Maybe a) -> a -> [a]<br class="">iterate1 f a = a : case f a of<br class=""> Just a1 -> iterate1 f a1<br class=""> Nothing -> []<br class=""><br class="">Using the musical notation for coinduction in Agda, I can get something similar:<br class=""><br class="">data Colist (A : Set) : Set where<br class=""> [] : Colist A<br class=""> _∷_ : A → (∞ (Colist A)) → Colist A <br class=""><br class="">iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a<br class="">iterate1 f a = a ∷ ♯ (case f a of<br class=""> λ { (just a₁) → (iterate1 f a₁)<br class=""> ; nothing → []<br class=""> })<br class=""><br class="">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.<br class=""><br class="">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:<br class=""><br class="">data T e a = e :<< T e a | V a — a "transcript"; like a list with an "answer"<br class=""><br class="">data T (e : Set) (a : Set) : Set where<br class=""> V : a → T e a<br class=""> _<<_ : e → ∞ (T e a) → T e a<br class=""><br class="">All these definitions are given in the attached files.<br class=""><br class="">Thanks!<br class="">Bill<br class=""><br class=""><br class=""><br class=""><br class=""><br class=""><br class=""><br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a></blockquote></div></blockquote></div><br class=""></div></body></html>