In this question about how to do getLine in Agda the main answer suggests using the partiality monad to deal with the possible non-termination of working with the resulting Costring.
On the other hand, in version 2.5.3 the manual page on Coinduction advises against ∞, saying it can be used to prove absurdity. However ∞ is used in the definition of both IO.IO and IO.run and the partiality monad.
Questions:
- Is it possible to do partiality and non-terminating IO using the standard library without ∞? If not, what are the alternatives?
- Is the standard library/documentation outdated?
- Is the problem with ∞ due to the interaction with sized types?
Thanks!