4

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:

  1. Is it possible to do partiality and non-terminating IO using the standard library without ∞? If not, what are the alternatives?
  2. Is the standard library/documentation outdated?
  3. Is the problem with ∞ due to the interaction with sized types?

Thanks!

André Gustavo Rigon
  • 73
  • 4
  • You can have a look at my work in progress [agda-sizedIO](https://github.com/gallais/agda-sizedIO) for a more modern copattern-based approach to IO in Agda. The main types are [here](https://gallais.github.io/agda-sizedIO/Sized.IO.html#IO′) and there's a [run function](https://gallais.github.io/agda-sizedIO/Sized.IO.html#run) which produces a `Prim.IO` just like in the old style. You can see how to use the [sized Colist](https://gallais.github.io/agda-sizedIO/Sized.Colist.html) in e.g. the [cat example](https://gallais.github.io/agda-sizedIO/cat.html). – gallais Oct 26 '17 at 13:50
  • I haven't defined `Sized.Partiality` but it shouldn't be too hard: it's basically a `Sized.Colist` which doesn't store values on the conses but does have one at the nil. – gallais Oct 26 '17 at 13:57
  • @gallais Your library looks very interesting! If you'd like to transform your comments into an answer I'll accept it. Thank you! – André Gustavo Rigon Oct 27 '17 at 11:25

0 Answers0