[Agda] printing infinite structures

[Henning Basold]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190227/9582e1c0/attachment.html>