The Coq mailing list

[alexandre p <ataaroap AT gmail.com>]

Hello,

On Fri, Feb 18, 2011 at 6:21 PM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
>
> I also tried to implement some IO monad which manages only standard
> channels (stdin, stdout, stderr); but it is quite naive and of course
> getchar doesn't really expect the user to input some character, and
> putchar doesn't print anything on a terminal.

This looks quite interesting, but shouldn't it be possible to recycle some of
the machinery you used for the state monad in your IO monad? The proofs
seem to be roughly similar.

I'm not terribly strong with Coq, but I am a seasoned Haskell user, and
(while the report doesn't mandate this representation) most Haskell
implementations do implement IO as a sort of state monad, typically
passing around an opaque state object that represents, formally,
the so-called "real world". This opaque object has no deeper structure,
because actual I/O happens outside of the type system. The obvious downside
(acceptable in Haskell but not in Coq, on philosophical grounds) is that you
can't really prove anything about a program's I/O behavior, because the type
system only annotates "does I/O" but doesn't say anything about what
kind of I/O is done.

I like how your naïve IO allows one to prove things about the input and output
streams by exposing some of the plumbing, but the obvious downside is
that such a scheme would quickly become too unwieldy to extend.

Has anyone thought about how to deal with I/O in a dependently typed
environment?

Best regards,

Alexandre