<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=""><pre class="Agda"><font face="Helvetica" class="">This is just a follow-up question to my questions from last week about colists, mainly to check my understanding. Consider these typical definitions in Data.Colist that depend on Data.Thunk/sized types: </font></pre><pre class="Agda"><a id="1830" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1830" class="Operator Function" style="text-decoration: none; color: rgb(0, 0, 205);">[_]</a> <a id="1834" class="Symbol" style="color: rgb(64, 64, 64);">:</a> <a id="1836" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1187" class="Generalizable" style="text-decoration: none;">A</a> <a id="1838" class="Symbol" style="color: rgb(64, 64, 64);">→</a> <a id="1840" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1245" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205);">Colist</a> <a id="1847" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1187" class="Generalizable" style="text-decoration: none;">A</a> <a id="1849" href="http://agda.github.io/agda-stdlib/Agda.Builtin.Size.html#302" class="Postulate" style="text-decoration: none; color: rgb(0, 0, 205);">∞</a>
<a id="1851" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1830" class="Operator Function" style="text-decoration: none; color: rgb(0, 0, 205);">[</a> <a id="1853" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1853" class="Bound" style="text-decoration: none; color: black;">a</a> <a id="1855" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1830" class="Operator Function" style="text-decoration: none; color: rgb(0, 0, 205);">]</a> <a id="1857" class="Symbol" style="color: rgb(64, 64, 64);">=</a> <a id="1859" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1853" class="Bound" style="text-decoration: none; color: black;">a</a> <a id="1861" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1310" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0);">∷</a> <a id="1863" class="Symbol" style="color: rgb(64, 64, 64);">λ</a> <a id="1865" class="Keyword" style="color: rgb(205, 102, 0);">where</a> <a id="1871" class="Symbol" style="color: rgb(64, 64, 64);">.</a><a id="1872" href="http://agda.github.io/agda-stdlib/Codata.Thunk.html#544" class="Field" style="text-decoration: none; color: rgb(238, 18, 137);">force</a> <a id="1878" class="Symbol" style="color: rgb(64, 64, 64);">→</a> <a id="1880" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1291" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0);">[]</a>
<a id="length" class=""></a><a id="1884" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1884" class="Function" style="text-decoration: none; color: rgb(0, 0, 205);">length</a> <a id="1891" class="Symbol" style="color: rgb(64, 64, 64);">:</a> <a id="1893" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1245" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205);">Colist</a> <a id="1900" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1187" class="Generalizable" style="text-decoration: none;">A</a> <a id="1902" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1174" class="Generalizable" style="text-decoration: none;">i</a> <a id="1904" class="Symbol" style="color: rgb(64, 64, 64);">→</a> <a id="1906" href="http://agda.github.io/agda-stdlib/Codata.Conat.html#527" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205);">Conat</a> <a id="1912" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1174" class="Generalizable" style="text-decoration: none;">i</a>
<a id="1914" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1884" class="Function" style="text-decoration: none; color: rgb(0, 0, 205);">length</a> <a id="1921" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1291" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0);">[]</a> <a id="1930" class="Symbol" style="color: rgb(64, 64, 64);">=</a> <a id="1932" href="http://agda.github.io/agda-stdlib/Codata.Conat.html#558" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0);">zero</a>
<a id="1937" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1884" class="Function" style="text-decoration: none; color: rgb(0, 0, 205);">length</a> <a id="1944" class="Symbol" style="color: rgb(64, 64, 64);">(</a><a id="1945" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1945" class="Bound" style="text-decoration: none; color: black;">x</a> <a id="1947" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1310" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0);">∷</a> <a id="1949" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1949" class="Bound" style="text-decoration: none; color: black;">xs</a><a id="1951" class="Symbol" style="color: rgb(64, 64, 64);">)</a> <a id="1953" class="Symbol" style="color: rgb(64, 64, 64);">=</a> <a id="1955" href="http://agda.github.io/agda-stdlib/Codata.Conat.html#575" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0);">suc</a> <a id="1959" class="Symbol" style="color: rgb(64, 64, 64);">λ</a> <a id="1961" class="Keyword" style="color: rgb(205, 102, 0);">where</a> <a id="1967" class="Symbol" style="color: rgb(64, 64, 64);">.</a><a id="1968" href="http://agda.github.io/agda-stdlib/Codata.Thunk.html#544" class="Field" style="text-decoration: none; color: rgb(238, 18, 137);">force</a> <a id="1974" class="Symbol" style="color: rgb(64, 64, 64);">→</a> <a id="1976" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1884" class="Function" style="text-decoration: none; color: rgb(0, 0, 205);">length</a> <a id="1983" class="Symbol" style="color: rgb(64, 64, 64);">(</a><a id="1984" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1949" class="Bound" style="text-decoration: none; color: black;">xs</a> <a id="1987" class="Symbol" style="color: rgb(64, 64, 64);">.</a><a id="1988" href="http://agda.github.io/agda-stdlib/Codata.Thunk.html#544" class="Field" style="text-decoration: none; color: rgb(238, 18, 137);">force</a><a id="1993" class="Symbol" style="color: rgb(64, 64, 64);">)</a>
</pre><div class=""><a class="Symbol" style="color: rgb(64, 64, 64);">The phrase “</a><a id="1863" class="Symbol" style="color: rgb(64, 64, 64);">λ</a> <a id="1865" class="Keyword" style="color: rgb(205, 102, 0);">where</a> <a id="1871" class="Symbol" style="color: rgb(64, 64, 64);">.</a><a id="1872" href="http://agda.github.io/agda-stdlib/Codata.Thunk.html#544" class="Field" style="text-decoration: none; color: rgb(238, 18, 137);">force</a> <a id="1878" class="Symbol" style="color: rgb(64, 64, 64);">→ …</a><a class="Symbol" style="color: rgb(64, 64, 64);">” effectively plays the role of ‘freeze’ in conventional presentations of thunks while passing .force (e.g., “</a><a id="1984" href="http://agda.github.io/agda-stdlib/Codata.Colist.html#1949" class="Bound" style="text-decoration: none; color: black;">xs</a> <a id="1987" class="Symbol" style="color: rgb(64, 64, 64);">.</a><a id="1988" href="http://agda.github.io/agda-stdlib/Codata.Thunk.html#544" class="Field" style="text-decoration: none; color: rgb(238, 18, 137);">force</a><a class="Symbol" style="color: rgb(64, 64, 64);">”) is effectively ’thaw’. Is that right?</a></div><div class=""><a class="Symbol" style="color: rgb(64, 64, 64);"><br class=""></a></div><div class=""><a class="Symbol" style="color: rgb(64, 64, 64);">Thanks Again,</a></div><div class=""><a class="Symbol" style="color: rgb(64, 64, 64);">Bill</a></div><div><br class=""><blockquote type="cite" class=""><div class="">On Apr 29, 2020, at 2:53 PM, Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org" class="">guillaume.allais@ens-lyon.org</a>> wrote:</div><br class="Apple-interchange-newline"><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="">Hi William,</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=""><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="">In the standard library we use a notion of `Thunk` for sized codata.</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=""><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="">This gives you definitions that look essentially like the ones using</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=""><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="">musical notations but on which you can define more compositional</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=""><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="">operations thanks to sized types.</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=""><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="">You can find colist here:</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=""><a href="http://agda.github.io/agda-stdlib/Codata.Colist.html" 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;" class="">http://agda.github.io/agda-stdlib/Codata.Colist.html</a><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="">And what you call transcript corresponds to our cowriter:</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=""><a href="http://agda.github.io/agda-stdlib/Codata.Cowriter.html" 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;" class="">http://agda.github.io/agda-stdlib/Codata.Cowriter.html</a><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="">Both come with various functions, including an `unfold` one that is</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=""><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="">a generalisation of your `iterate` where we distinguish between the</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=""><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="">type of the internal state and the type of the values outputted in</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=""><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="">the codatatype.</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=""><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="">Best,</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=""><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=""></body></html>