<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="">Hi-</div><div class=""><br class=""></div><div 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.</div><div class=""><br class=""></div><div class="">In Haskell, the built-in iterate function always produces an infinite list:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><font face="Courier New" class="">iterate :: (a -> a) -> a -> [a]</font></div><div class=""><font face="Courier New" class="">iterate f a = a : iterate f (f a)</font></div></blockquote><div class=""><br class=""></div><div class="">This can be represented in Agda using a Stream (defined as a coinductive record):</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Courier New" class="">iterate : ∀ {a} → (a → a) → a → Stream a</font></div></div><div class=""><div class=""><font face="Courier New" class="">hd (iterate f a) = a</font></div></div><div class=""><div class=""><font face="Courier New" class="">tl (iterate f a) = iterate f (f a)</font></div></div></blockquote><div class=""><br class=""></div><div class="">Now, back in Haskell, we can define a *potentially* infinite list by introducing Maybe in the codomain of f:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><font face="Courier New" class="">iterate1 :: (a -> Maybe a) -> a -> [a]</font></div><div class=""><font face="Courier New" class="">iterate1 f a = a : case f a of</font></div><div class=""><font face="Courier New" class=""> Just a1 -> iterate1 f a1</font></div><div class=""><font face="Courier New" class=""> Nothing -> []</font></div></blockquote><div class=""><br class=""></div><div class="">Using the musical notation for coinduction in Agda, I can get something similar:</div><div class=""><br class=""></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><font face="Courier New" class="">data Colist (A : Set) : Set where</font></div></div><div class=""><div class=""><font face="Courier New" class=""> [] : Colist A</font></div></div><div class=""><div class=""><font face="Courier New" class=""> _∷_ : A → (∞ (Colist A)) → Colist A </font></div></div><div class=""><div class=""><font face="Courier New" class=""><br class=""></font></div></div><div class=""><div class=""><font face="Courier New" class="">iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a</font></div></div><div class=""><div class=""><font face="Courier New" class="">iterate1 f a = a ∷ ♯ (case f a of</font></div></div><div class=""><div class=""><font face="Courier New" class=""> λ { (just a₁) → (iterate1 f a₁)</font></div></div><div class=""><div class=""><font face="Courier New" class=""> ; nothing → []</font></div></div><div class=""><div class=""><font face="Courier New" class=""> })</font></div></div></blockquote><div class=""><br class=""></div><div 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.</div><div class=""><br class=""></div><div 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:</div><div class=""><div class=""><br class=""></div></div><blockquote style="margin: 0 0 0 40px; border: none; padding: 0px;" class=""><div class=""><div class=""><div class=""><font face="Courier New" class="">data T e a = e :<< T e a | V a — a "transcript"; like a list with an "answer"</font></div></div></div><div class=""><div class=""><font face="Courier New" class=""><br class=""></font></div></div><div class=""><div class=""><font face="Courier New" class="">data T (e : Set) (a : Set) : Set where</font></div></div><div class=""><div class=""><font face="Courier New" class=""> V : a → T e a</font></div></div><div class=""><div class=""><font face="Courier New" class=""> _<<_ : e → ∞ (T e a) → T e a</font></div></div></blockquote><div class=""><br class=""></div><div class="">All these definitions are given in the attached files.</div><div class=""><br class=""></div><div class="">Thanks!</div><div class="">Bill</div><div class=""></div></body></html>