Interesting. So is it the case that existentials are only meant to hide internals? Is there another useful application for them?




On Sun, Jan 13, 2013 at 5:50 PM, Brandon Allbery <allbery.b@gmail.com> wrote:
On Sun, Jan 13, 2013 at 8:34 PM, Darren Grant <therealkludgy@gmail.com> wrote:
On Wed, Jan 9, 2013 at 1:45 PM, Aleksandar Dimitrov <aleks.dimitrov@gmail.com> wrote:
> Sometimes I read an argument that existentials are required due to unknown
> constraints at compile time, but do not have an intuition for this
> situation yet.  For instance, I read that IO requires existentials. Still
> working on that one. :)

Where did you read that? The *definition* of the IO type does not use
existentials [2]. But I'm not very familiar with the internals.

You're right!  I'm not sure what I saw, but I would guess that I conflated some application of IO with the definition.

The only thing I'm aware of offhand is that an existential is used to hide the internals, not because this is in some sense necessary for IO to work, but to allow the compiler to ensure that nothing is violating IO's "contract":  you can't do anything with something you don't know the type of, so it's impossible for normal code to do anything out of bounds with an IO type.  You could just as well write an implementation of IO without any existentials or magic internals, but it'd be trivial to "cheat".  (GHC's, with the magic stripped away, is just state:  sequential execution is guaranteed by passing a state "baton" between IO actions, and the magic just makes sure you can't stash a copy of the baton or manufacture one yourself.  There's some slight additional magic that functions as an optimization.)

--
brandon s allbery kf8nh                               sine nomine associates
allbery.b@gmail.com                                  ballbery@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net