Unlifted data types

[Simon Peyton Jones]

| After many discussions and beers at ICFP, I've written up my current
| best understanding of the unlifted data types proposal:
| 
|     https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes

Too many beers!  I like some, but not all, of this.

There are several distinct things being mixed up.

(1) First, a proposal to allow a data type to be declared to be unlifted.  On its own, this is a pretty simple proposal:

 * Data types are always boxed, and so would unlifted data types

 * But an unlifted data type does not include bottom, and operationally
   is always represented by a pointer to the value.  Just like Array#.
 
 * ALL the evaluation rules are IDENTICAL to those for other unlifted 
   types such as Int# and Array#.  Lets are strict, and cannot be 
   recursive, function arguments are evaluated before the call. Literally
   nothing new here.

 * The code generator can generate more efficient case expressions,
   because the pointer always points to a value, never to a thunk or
   (I believe) an indirection.   I think there are some special cases
   in GC and the RTS to ensure that this invariant holds.

And that's it.  Syntax: I'd suggest something more prominent than an Unlifted return kind, such as
  data unlifted T a = L a | R a
but I would not die for this.

I would really like to see this articulated as a stand-alone proposal.  It makes sense by itself, and is really pretty simple.

(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.

(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 got lost in all the traffic about it.

(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.  


My suggestion: let's nail down (1), including a boxed version of Force an suspend as plain library code, if you want, and perhaps (4); and only THEN tackle the trickiness of unboxing Force. 

Simon
	
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Edward
| Z. Yang
| Sent: 04 September 2015 09:04
| To: ghc-devs
| Subject: Unlifted data types
| 
| Hello friends,
| 
| After many discussions and beers at ICFP, I've written up my current
| best understanding of the unlifted data types proposal:
| 
|     https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
| 
| Many thanks to Richard, Iavor, Ryan, Simon, Duncan, George, Paul,
| Edward Kmett, and any others who I may have forgotten for crystallizing
| this proposal.
| 
| Cheers,
| Edward
| _______________________________________________
| ghc-devs mailing list
| ghc-devs at haskell.org
| http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs