[Agda] printing infinite structures

[Apostolis Xekoukoulotakis]

Could it be this?

https://agda.github.io/agda-stdlib/IO.html

On Wed, Feb 27, 2019 at 1:35 PM Henning Basold <henning at basold.eu> wrote:

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