<div dir="ltr"><div>Could it be this?</div><div><br></div><div dir="ltr"><a href="https://agda.github.io/agda-stdlib/IO.html">https://agda.github.io/agda-stdlib/IO.html</a><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Feb 27, 2019 at 1:35 PM Henning Basold <<a href="mailto:henning@basold.eu">henning@basold.eu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>I'm only aware of the monadic apprach here: <a href="https://github.com/agda/agda-system-io/" target="_blank">https://github.com/agda/agda-system-io/</a><br><br>Perhaps, Anton has something in his work on GUIs?<br><br><div class="gmail_quote">On February 27, 2019 12:27:46 PM CET, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<pre class="gmail-m_4110708341874097444k9mail">I know this paper. Is there a coinductive implementation of IO which I can use from interactive agda? If yes where is it described?<br><br>Thorsten<br><br>On 27/02/2019, 11:03, "Agda on behalf of Henning Basold" <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a> on behalf of <a href="mailto:henning@basold.eu" target="_blank">henning@basold.eu</a>> wrote:<br><br> -----BEGIN PGP SIGNED MESSAGE-----<br> Hash: SHA512<br> <br> What Guillaume refers to is the paper "Interactive Programs and Weakly<br> Final Coalgebras in Dependent Type Theory", I suppose. However, this<br> will not give you any printing methods, you still need to implement<br> them yourself as commands that you evaluate later in the compilation<br> stage. Also, since IO is implemented as cofree comonad, evaluation of<br> elements in it will typically not terminate. Thus, in the end you will<br> have to resort to some mechanism that cuts of evaluation again.<br> <br> That being said, maybe it's worthwhile to implement IO in the standard<br> library and have a general abortion mechanism in the evaluation of<br> compiled programs.<br> <br> Henning<br> <br> On 27/02/2019 11:25, Thorsten Altenkirch wrote:<br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid rgb(114,159,207);padding-left:1ex">Can I use IO from interactive agda? How? What do you mean it is<br>defined coinductively? Where is this described?<br><br>On 26/02/2019, 16:35, "Guillaume Allais"<br><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>> wrote:<br><br>IO is coinductive so you could write `Stream String -> IO ()` in<br>Agda itself.<br><br>On 26/02/2019 17:08, Thorsten Altenkirch wrote:<br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid rgb(173,127,168);padding-left:1ex">I told them that I have no idea how to run the compiler. Which is<br>true. T.<br><br>From: "Setzer A.G." <<a href="mailto:a.g.setzer@swansea.ac.uk" target="_blank">a.g.setzer@swansea.ac.uk</a>> Date: Tuesday, 26<br>February 2019 at 15:59 To: Thorsten Altenkirch<br><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>>, agda list<br><<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>> Subject: Re: printing infinite<br>structures<br><br>The only disadvantage is that you need to compile your code, but<br>I when interacting with students the first thing they want to<br>know is how to compile the code.<br><br><br><br><br><br>This message and any attachment are intended solely for the<br>addressee and may contain confidential information. If you have<br>received this message in error, please contact the sender and<br>delete the email and attachment.<br><br>Any views or opinions expressed by the author of this email do<br>not necessarily reflect the views of the University of<br>Nottingham. Email communications with the University of<br>Nottingham may be monitored where permitted by law.<br><br><br><br><br><br>_______________________________________________ Agda mailing<br>list <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br></blockquote><br><br><br><br><br><br>This message and any attachment are intended solely for the<br>addressee and may contain confidential information. If you have<br>received this message in error, please contact the sender and<br>delete the email and attachment.<br><br>Any views or opinions expressed by the author of this email do not <br>necessarily reflect the views of the University of Nottingham.<br>Email communications with the University of Nottingham may be<br>monitored where permitted by law.<br><br><br><br><br>_______________________________________________ Agda mailing list <br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br></blockquote> -----BEGIN PGP SIGNATURE-----<br> <br> iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlx2bk4ACgkQatBsEc2x<br> Mm5w4A//ZLs6G8uCkw/KZBzwM9+7hFzy5anN7phKQ1hLwvM3oxYq/ckUB6X288/K<br> WPaj8fleX0/beAk5ucqhZ4iFMKVtHJCTeBDINeGdoXwA3qVE6cjnsjQUA4HZ6q5G<br> PL1tdMQyaoi/TBddOBeiyt+8AHiJ+Ddp5vL2BslcnuEV+VxRWTUfSYEv9RdQadjK<br> b/x3k1jhm73/6pL2zkkZ7ujn5egxgSb+fq/ppI/4XEdd9vc8BHm4PZ1UYDMd1nP3<br> mVnsD3ZP5EFKqrbC0x+PxyaYZAU1cd/Dphm6AQjmO4SfH4pa6L/+j+vDDBwMxavS<br> H1nk/AnZv3r4WXQreZQhtXHnUYee5AYPLbkFK1Rf2z1xL+mP5QtSWooMhitnQRfN<br> u2FBS/5qaJvJA/q9M3zv8eG2nCxPz7oKEnSYXlWQ8vNHvxml8VPkWxSWm2iknJPA<br> jpK3E2/UnMJF4KocQbVQet5aGF29+kHnXmUKD+rXlaFqDU7NiP0c0n4tm5D27hdR<br> kKiRuU6W4t1mgW95RL/+BvVpLVS+fMNY+k0+t2yeOHyEmTyVTsu2IANs4T6yAkAv<br> ZIwsTRc0CH7obuuTJMZEpnjLTXp6o6wN/Yh63828ysSH/xvojPUpGSURWjUxeM9H<br> oajGfrCbaa/M+h9y3BJ7wkdefzaG41PcuhSmP5NjSKXmBJeEa6k=<br> =FSTn<br> -----END PGP SIGNATURE-----<hr> Agda mailing list<br> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br> <br><br><br><br><br>This message and any attachment are intended solely for the addressee<br>and may contain confidential information. If you have received this<br>message in error, please contact the sender and delete the email and<br>attachment. <br><br>Any views or opinions expressed by the author of this email do not<br>necessarily reflect the views of the University of Nottingham. Email<br>communications with the University of Nottingham may be monitored <br>where permitted by law.<br><br><br><br><br></pre></blockquote></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>