Unlifted data types

[Edward Z. Yang]

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