Excerpts from Dan Doel's message of 2015-09-04 18:21:29 -0700:
Here are some additional thoughts.
If we examine an analogue of some of your examples:
data MutVar a = MV (MutVar# RealWorld a)
main = do let mv# = undefined let mv = MV mv# putStrLn "Okay."
The above is illegal. Instead we _must_ write:
This doesn't typecheck, but for a different reason: undefined :: a where a :: *, so you can't match up the kinds. error is actually extremely special in this case: it lives in OpenKind and matches both * and #. But let's suppose that we s/undefined/error "foo"/...
let !mv# = undefined
which signals that evaluation is occurring.
Also not true. Because error "foo" is inferred to have kind #, the bang pattern happens implicitly.
So it is impossible to accidentally go from:
main = do let mv = MV undefined putStrLn "Okay."
which prints "Okay.", to something that throws an exception, without having a pretty good indication that you're doing so. I would guess this is desirable, so perhaps it should be mandated for Unlifted as well.
Nope, if you just float the error call out of MV, you will go from "Okay." to an exception. Notice that *data constructors* are what are used to induce suspension. This is why we don't have a 'suspend' special form; instead, 'Box' is used directly.
However, the above point confuses me with respect to another example. The proposal says that:
data Id :: * -> Unlifted where Id :: a -> Id a
could/should be compiled with no overhead over `a`, like a newtype. However, if Unlifted things have operational semantics like #, what does the following do:
let x :: Id a !x = Id undefined
The ! should evaluate to the Id constructor, but we're not representing it, so it actually doesn't evaluate anything? But:
That's correct. Id is a box containing a lifted value. The box is unlifted, but the inner value can be lifted.
let x :: Id a !x = undefined
throws an exception?
Yes, exactly.
Whereas for newtypes, both throw exceptions with a !x definition, or don't with an x definition?
Also correct. They key thing is to distinguish error in kind * and error in kind #. You can make a table: | Id (error "foo") | error "foo" | ---------------------+-----------------------+-------------------+ newtype Id :: * -> * | error "foo" :: * | error "foo" :: * | data Id :: * -> # | Id (error "foo" :: *) | error "foo" :: # |
Is it actually possible to make Id behave this way without any representational overhead?
Yes. The reason is that an error "foo" :: # *immediately fails* (rather than attempt to allocate an Id). So the outer level of error doesn't ever need to be represented on the heap, so we can just represent the inner liftedness. Here's another way of looking at it: error in kind # is not a bottom at all. It's just a way of bailing immediately. HOWEVER...
I'm a little skeptical. I think that only Force (and Box) might be able to have no representational overhead.
It seems like it might be easier to explain if just Force and Box get optimized, and we don't bother with others; I only really care about those two operators being optimized. Edward