Unlifted data types
Simon Peyton Jones
simonpj at microsoft.com
Wed Sep 9 12:28:01 UTC 2015
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.
| -----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
| 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.
| On Sep 8, 2015, at 3:52 AM, Simon Peyton Jones <simonpj at microsoft.com>
| > | 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'
| > 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
More information about the ghc-devs