Unlifted data types

[Simon Peyton Jones]

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

I've re-numbered them 1,2,3,4, since 1.1 is (to me) a pretty major deal, stands in its own right, and certainly isn't a sub-proposal of (1).

Under (new) 2, I'm very dubious about "Boxed levity polymorphism in types (and functions with extra code generation)".  It's certainly true that we could generate two copied of the code for every function; but by generating three, or perhaps four copies we could also deal with Int# and Float#. Maybe one more for Double#.  .NET does this on the fly, incidentally.  Where do you stop?

Also remember it's not just an issue of GC pointers.  The semantics of the function changes, because things that are thunks for the lifted version become strict in the unlifted version.

Your 'umap' is a bit more convincing.  But for now (2) would be low on my priority list, until we encounter user pressure which (note) we have not encountered so far despite the range of boxed but unlifted types. Why is now the right time?

(1) and (3) seem solid.

I'll leave (4) for another message.

Simon

| -----Original Message-----
| From: Edward Z. Yang [mailto:ezyang at mit.edu]
| Sent: 07 September 2015 22:36
| To: Simon Peyton Jones
| Cc: ghc-devs
| Subject: RE: Unlifted data types
| 
| 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:Polym
| orphismoveranewUnliftedkind
| 
| (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