[Agda] printing infinite structures

[Guillaume Allais]

Yes, this is what I meant: IO in the stdlib is defined as a coinductive type.
Unfortunately it is currently not possible to run IO actions from inside of
Agda: you need to compile your program (so you need a main) and then run it.
Being able to execute them from inside Agda is currently still future work.

Cheers,
--
gallais

On 27/02/2019 13:33, Apostolis Xekoukoulotakis wrote:
> 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:
>>>
> 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
>>>>>
>>>>>     

>>> ------------------------------
>>>     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
>>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190227/94dca899/attachment.sig>