Unlifted data types

[Dan Doel]

On Sat, Sep 5, 2015 at 3:06 AM, Edward Z. Yang <ezyang at mit.edu> wrote:
>> 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