<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Please note that the paper of Ulrich Berger and myself</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="Arial">Ulrich Berger and Anton Setzer: <a href="http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf">
Undecidability of Equality for Codata Types</a>, <a href="https://doi.org/10.1007/978-3-030-00389-0_4">
doi 10.1007/978-3-030-00389-0_4</a> <font face="Arial">In: Corina Cirstea (Ed): Coalgebraic Methods in computer Science. Springer Lectuer Notes in Computer Science 11202, 2018.</font></font></div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<a href="http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf" id="LPNoLP315935">http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf</a></div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
contains a discussion how the musical notation can be interpreted in the coalgebra approach (so is just a form of syntactic sugar)</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Anton<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<br>
<div>
<div id="appendonsend"></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of William Harrison <william.lawrence.harrison@gmail.com><br>
<b>Sent:</b> 29 April 2020 17:58<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> [Agda] Question about colists, musical notation vs coinductive records, and all that</font>
<div> </div>
</div>
<div>
<div class="" style="word-wrap:break-word; line-break:after-white-space">
<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 class="" style="margin:0 0 0 40px; border:none; padding:0px">
<div class=""><font class="" face="Courier New">iterate :: (a -> a) -> a -> [a]</font></div>
<div class=""><font class="" face="Courier New">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 class="" style="margin:0 0 0 40px; border:none; padding:0px">
<div class="">
<div class=""><font class="" face="Courier New">iterate : ∀ {a} → (a → a) → a → Stream a</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New">hd (iterate f a) = a</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New">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 class="" style="margin:0 0 0 40px; border:none; padding:0px">
<div class=""><font class="" face="Courier New">iterate1 :: (a -> Maybe a) -> a -> [a]</font></div>
<div class=""><font class="" face="Courier New">iterate1 f a = a : case f a of</font></div>
<div class=""><font class="" face="Courier New"> Just a1 -> iterate1 f a1</font></div>
<div class=""><font class="" face="Courier New"> 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 class="" style="margin:0 0 0 40px; border:none; padding:0px">
<div class="">
<div class=""><font class="" face="Courier New">data Colist (A : Set) : Set where</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> [] : Colist A</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> _∷_ : A → (∞ (Colist A)) → Colist A </font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"><br class="">
</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New">iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New">iterate1 f a = a ∷ ♯ (case f a of</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> λ { (just a₁) → (iterate1 f a₁)</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> ; nothing → []</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> })</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 class="" style="margin:0 0 0 40px; border:none; padding:0px">
<div class="">
<div class="">
<div class=""><font class="" face="Courier New">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 class="" face="Courier New"><br class="">
</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New">data T (e : Set) (a : Set) : Set where</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> V : a → T e a</font></div>
</div>
<div class="">
<div class=""><font class="" face="Courier New"> _<<_ : 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>
</div>
<div style="word-wrap:break-word; line-break:after-white-space">
<meta content="text/html; charset=us-ascii">
<div></div>
</div>
<div class="" style="word-wrap:break-word; line-break:after-white-space">
<div class=""></div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
</div>
</div>
</div>
</body>
</html>