[Agda] printing infinite structures

[Henning Basold]

-----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-----