[Haskell-cafe] Identity of indiscernibles

[Tom Ellis]

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 <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> 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