RE: Unlifted data types

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@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 | 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@haskell.org | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs