
On Sat, Sep 5, 2015 at 3:06 AM, Edward Z. Yang
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.
I tried with `error` first, and it worked exactly the way I described. But I guess it's a type inference weirdness. If I annotate mv# with MutVar# it will work, whereas otherwise it will be inferred that mv# :: a where a :: *, instead of #. Whereas !x is a pattern which requires monomorphism of x, and so it figures out mv# :: MutVar# .... Kind of an odd corner case where breaking cycles causes things _not_ to type check, due to open kinds not being first class. I thought I remembered that at some point it was decided that `let` bindings of unboxed things should be required to have bangs on the bindings, to indicate the evaluation order. Maybe I'm thinking of something else (was it that it was originally required and we got rid of it?).
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.
I know that it's the floating that makes a difference, not the bang pattern. The point would be to make the syntax require the bang pattern to give a visual indication of when it happens, and make it illegal to look like you're doing a normal let that doesn't change the value (although having it actually be a bang pattern would be bad, because it'd restrict polymorphism of the definition). Also, the constructor isn't exactly relevant, so much as whether the unlifted error occurs inside the definition of a lifted thing. For instance, we can go from: let mv = MutVar undefined to: let mv = let mv# :: MutVar# RealWorld a ; mv# = undefined in MutVar mv# and the result is the same, because it is the definition of mv that is lazy. Constructors in complex expressions---and all subexpressions for that matter---just get compiled this way. E.G. let f :: MutVar# RealWorld a -> MutVar a f mv# = f mv# in flip const (f undefined) $ putStrLn "okay" No constructors involved, but no error.
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.
Okay. So, there isn't representational overhead, but there is overhead, where you call a function or something (which will just return its argument), whereas newtype constructors end up not having any cost whatsoever? -- Dan