Unlifted data types

[Edward Z. Yang]

Hello Simon,

> There are several distinct things being mixed up.

I've split the document into three (four?) distinct subproposals.
Proposals 1 and 2 stand alone.

> (1) First, a proposal to allow a data type to be declared to be unlifted.  On its own, this is a pretty simple proposal: [snip]
> 
> I would really like to see this articulated as a stand-alone proposal.  It makes sense by itself, and is really pretty simple.

This is now "Proposal 1".

> (2) Second, we cannot expect levity polymorphism.  Consider
>    map f (x:xs) = f x : map f xs
> Is the (f x) a thunk or is it evaluated strictly?  Unless you are going to clone the code for map (which levity polymorphism is there to avoid), we can't answer "it depends on the type of (f x)".   So, no, I think levity polymorphism is out.
> 
> So I vote against splitting # into two: plain will do just fine.

Levity polymorphism will not work without generating two copies of
'map', but plain polymorphism over 'Unlifted' is useful (as Dan has
also pointed out.)  In any case, I've extracted this out into a
separate subproposal "Proposal 1.1".
https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes#Proposal1.1:PolymorphismoveranewUnliftedkind

(reordering here.)

> (4) Fourth, you don't mention a related suggestion, namely to allow
>     newtype T = MkT Int#
> with T getting kind #.  I see no difficulty here.  We do have (T ~R Int#). It's just a useful way of wrapping a newtype around an unlifted type.  

This is now "Proposal 2".

> (3) Third, the stuff about Force and suspend.  Provided you do no more than write library code that uses the above new features I'm fine.   But there seems to be lots of stuff that dances around the hope that (Force a) is represented the same way as 'a'.  I don't' know how to make this fly.  Is there a coercion in FC?  If so then (a ~R Force a).  And that seems very doubtful since we must do some evaluation.

I agree that we can't introduce a coercion between 'Force a' and
'a', for the reason you mentioned. (there's also a second reason which
is that 'a ~R Force a' is not well-typed; 'a' and 'Force a' have
different kinds.)

I've imagined that we might be able to just continue representing
Force explicitly in Core, and somehow "compile it away" at STG time,
but I am definitely fuzzy about how this is supposed to work.  Perhaps
Force should not actually be a data type, and we should have
'force# :: a -> Force a' and 'unforce# :: Force a -> a' (the latter
of which compiles to a no-op.)

Cheers,
Edward