[Agda] printing infinite structures

[Thorsten Altenkirch]

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.