Re: [Haskell-cafe] Identity of indiscernibles

On Fri, Aug 09, 2013 at 12:38:45AM +0700, Kim-Ee Yeoh wrote:

On Thu, Aug 8, 2013 at 11:05 PM, Tom Ellis wrote:

...

On Thu, Aug 08, 2013 at 03:38:41PM +0200, Jerzy Karczmarczuk wrote:

...

...

One could simply implement IO as a free monad Interesting. I wonder how.

See [1] for an explanation of free monads in general. For IO in particular, define a functor

data IOF a = GetChar (Char -> a) | PutChar Char a | ...

with constructors for all elementary IO operations.

If I understand correctly, you're proposing equality of (IO a) based on the AST of imperatives, similar to what comes out of GCC's front-end for C [1].

I'm not proposing it. I'm just pointing out it could be done, as a challenge to Jerzy's assertion that "In fact, you can do almost nothing with [values of type IO ()]". However, I may have misunderstood Jerzy's point anyway. Tom