Unlifted data types

[Simon Peyton Jones]

I like your suggestion!

I think it'd be better to have 

TYPE :: TypeShape -> *

data TypeShape = Unboxed | Boxed Levity
data Levity = Lifted | Unlifted

Now the awkward "unboxed/lifted" combination doesn't arise.

Now, 'error' is "TypeShape-polymorphic":
  error :: forall (ts :: TypeShape) (a :: TYPE ts). String -> a

What functions (if any) are "Levity-polymorphic". That is, they have identical code regardless of whether their (boxed) type args are lifted or unlifted?  Answer: data constructors. As Richard says
  Cons :: forall (v1::Levity) (v2::Levity) (a::TYPE (Boxed v1)).
          a -> List v1 v2 a -> List v1 v2 a

Why can it be levity-polymorphic? Because data constructors guarantee to construct no intermediate values (which they would be unsure whether or not to evaluate).

Typically, though, functions over lists would not be levity-polymorphic, for reasons previously discussed.


The awkward spot is the runtime system.  Currently it goes to some lengths to ensure that it never introduces an indirection for a boxed-but-unlifted type.  Simon Marlow would know exactly where.  So I suspect that we WOULD need two versions of each (levity-polymorphic) data constructor, alas.  And we'd need to know which version to use at every call site, which means the code would need to be levity-monomorphic.  So we really would get very little levity polymorphism ineed.  I think.

All this fits nicely with Dan Doel's point about making ! a first class type constructor.

Simon


|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  Richard Eisenberg
|  Sent: 08 September 2015 14:46
|  To: ghc-devs
|  Subject: Re: Unlifted data types
|  
|  I have put up an alternate set of proposals on
|  
|    https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
|  
|  These sidestep around `Force` and `suspend` but probably have other
|  problems. They make heavy use of levity polymorphism.
|  
|  Back story: this all was developed in a late-evening Haskell Symposium
|  session that took place in the hotel bar. It seems Edward and I walked
|  away with quite different understandings of what had taken place. I've
|  written up my understanding. Most likely, the Right Idea is a
|  combination of this all!
|  
|  See what you think.
|  
|  Thanks!
|  Richard
|  
|  On Sep 8, 2015, at 3:52 AM, Simon Peyton Jones <simonpj at microsoft.com>
|  wrote:
|  
|  > |  And to
|  > |  be honest, I'm not sure we need arbitrary data types in Unlifted;
|  > | Force (which would be primitive) might be enough.
|  >
|  > That's an interesting thought.  But presumably you'd have to use
|  'suspend' (a terrible name) a lot:
|  >
|  > type StrictList a = Force (StrictList' a) data StrictList' a = Nil |
|  > Cons !a (StrictList a)
|  >
|  > mapStrict :: (a -> b) -> StrictList a -> StrictList b mapStrict f xs
|  =
|  > mapStrict' f (suspend xs)
|  >
|  > mapStrict' :: (a -> b) -> StrictList' a -> StrictList' b mapStrict'
|  f
|  > Nil = Nil mapStrict' f (Cons x xs) = Cons (f x) (mapStrict f xs)
|  >
|  >
|  > That doesn't look terribly convenient.
|  >
|  > | ensure that threads don't simply
|  > |  pass thunks between each other. But, if you have unlifted types,
|  > | then  you can have:
|  > |
|  > |      data UMVar (a :: Unlifted)
|  > |
|  > |  and then the type rules out the possibility of passing thunks
|  > | through  a reference (at least at the top level).
|  >
|  > Really? Presumably UMVar is a new primitive? With a family of
|  operations like MVar?  If so can't we just define
|  > 	newtype UMVar a = UMV (MVar a)
|  > 	putUMVar :: UMVar a -> a -> IO ()
|  > 	putUMVar (UMVar v) x = x `seq` putMVar v x
|  >
|  > I don't see Force helping here.
|  >
|  > Simon
|  > _______________________________________________
|  > ghc-devs mailing list
|  > ghc-devs at haskell.org
|  > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs