<div dir="auto">I used my own Maybe type because I didn't have the standard library handy. I guess I named the constructors differently?</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Apr 29, 2020, 21:08 William Harrison <<a href="mailto:william.lawrence.harrison@gmail.com">william.lawrence.harrison@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">Thank you Eric and Guillaume! I think you have both answered my questions, and the pointer to Cowriter are spot on.<div><br></div><div>Eric,</div><div><br></div><div>What you wrote is what I was trying to write, although I get an odd syntax error when I try it (I’ve attached the file that generates the error). It is possible that this is just a stupid mistake on my part made after staring at an emacs buffer all day.</div><div><br></div><div>This definition:</div><div><div><font face="Courier New">iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a</font></div><div><font face="Courier New">Hd (iterate1 {A} f a) = Just (a , loop (f a))</font></div><div><font face="Courier New"> where</font></div><div><font face="Courier New"> loop : Maybe A → Colist A</font></div><div><font face="Courier New"> loop Nothing = hd Nothing</font></div><div><font face="Courier New"> loop (Just a') = iterate1 f a’</font></div><div><br></div><div>Generates this error:</div><div><br></div><div><font face="Courier New">…/ColistQuestion.agda:19,6-20</font></div><div><font face="Courier New">Could not parse the left-hand side loop (Just a')</font></div><div><font face="Courier New">Operators used in the grammar:</font></div><div><font face="Courier New"> None</font></div><div><font face="Courier New">when scope checking the left-hand side loop (Just a') in the</font></div><div><font face="Courier New">definition of loop</font></div><div><br></div><div>Am I missing something obvious?</div><div><br></div><div>Thanks Again,</div><div>Bill</div><div><br><blockquote type="cite"><div>On Apr 29, 2020, at 2:53 PM, Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank" rel="noreferrer">guillaume.allais@ens-lyon.org</a>> wrote:</div><br><div><span style="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;text-decoration:none;float:none;display:inline!important">Hi William,</span><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">In the standard library we use a notion of `Thunk` for sized codata.</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">This gives you definitions that look essentially like the ones using</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">musical notations but on which you can define more compositional</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">operations thanks to sized types.</span><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">You can find colist here:</span><br style="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;text-decoration:none"><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;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank" rel="noreferrer">http://agda.github.io/agda-stdlib/Codata.Colist.html</a><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">And what you call transcript corresponds to our cowriter:</span><br style="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;text-decoration:none"><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;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px" target="_blank" rel="noreferrer">http://agda.github.io/agda-stdlib/Codata.Cowriter.html</a><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">Both come with various functions, including an `unfold` one that is</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">a generalisation of your `iterate` where we distinguish between the</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">type of the internal state and the type of the values outputted in</span><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">the codatatype.</span><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">Best,</span></div></blockquote></div></div></div><div style="word-wrap:break-word;line-break:after-white-space"><div><div><blockquote type="cite"><div></div></blockquote><blockquote type="cite"><div><span style="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;text-decoration:none;float:none;display:inline!important">guillaume</span><br style="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;text-decoration:none"><br style="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;text-decoration:none"><br style="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;text-decoration:none"><span style="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;text-decoration:none;float:none;display:inline!important">On 29/04/2020 17:58, William Harrison wrote:</span><br style="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;text-decoration:none"><blockquote type="cite" style="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;text-decoration:none">Hi-<br><br>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><br>In Haskell, the built-in iterate function always produces an infinite list:<br><br>iterate :: (a -> a) -> a -> [a]<br>iterate f a = a : iterate f (f a)<br><br>This can be represented in Agda using a Stream (defined as a coinductive record):<br><br>iterate : ∀ {a} → (a → a) → a → Stream a<br>hd (iterate f a) = a<br>tl (iterate f a) = iterate f (f a)<br><br>Now, back in Haskell, we can define a *potentially* infinite list by introducing Maybe in the codomain of f:<br><br>iterate1 :: (a -> Maybe a) -> a -> [a]<br>iterate1 f a = a : case f a of<br> Just a1 -> iterate1 f a1<br> Nothing -> []<br><br>Using the musical notation for coinduction in Agda, I can get something similar:<br><br>data Colist (A : Set) : Set where<br> [] : Colist A<br> _∷_ : A → (∞ (Colist A)) → Colist A <br><br>iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a<br>iterate1 f a = a ∷ ♯ (case f a of<br> λ { (just a₁) → (iterate1 f a₁)<br> ; nothing → []<br> })<br><br>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><br>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><br>data T e a = e :<< T e a | V a — a "transcript"; like a list with an "answer"<br><br>data T (e : Set) (a : Set) : Set where<br> V : a → T e a<br> _<<_ : e → ∞ (T e a) → T e a<br><br>All these definitions are given in the attached files.<br><br>Thanks!<br>Bill<br><br><br><br><br><br><br><br><br>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" rel="noreferrer">https://lists.chalmers.se/mailman/listinfo/agda</a></blockquote></div></blockquote></div><br></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>