| (denotationally, at least) is the outer-most level. That's why I liked | the original proposal (which probably disappeared too fast for most | people to read it), which was more like being able to talk about `!a` | as a thing in itself. It's the only semantic gap in being able to
That's another interesting idea. Currently ! is an annotation on a data constructor argument (only). It is not a type-former; so that !Int or !(Int ->Int) are not types. I think your point is that if we spell "Force" as "!" then it becomes a first-class type former. Let's try that: * t and !t are distinct types * You get from one to the other by using ! as a term-level data constructor, so you can use it in terms and in pattern matching. Thus - if (e::t) then (!e :: !t) - if (e::!t) then case of !x -> blah here (x::t) * As with newtype constructors, pattern-matching on !t doesn't imply evaluation; after all, it's already evaluated. * In Richard's notation, the type constructor (!) has kind (!) :: TYPE 'Boxed l -> TYPE 'Boxed Unlifted The wrinkle for data types is this. The declaration data T = MkT !Int !a produces a data constructor with type MkT :: forall a. Int -> a -> T But if (!t) is a first-class type, then you'd expect to get a data constructor with type MkT :: forall a. !Int -> !a -> T and that in turn would force many calls to look like (MkT !e1 !e2). But we could re-cast the special treatment for the top-level bang on data constructor arguments, to say that we get a worker/wrapper story so that the programmer's eye view is indeed that MkT :: forall a. Int -> a -> T, and the compiler generates the eval code to match things up. (Which is what happens now.) But if you wrote, say, data S = MkS (!Int, !a) then this magic would not happen and you really would get MkS :: (!Int, !a) -> S Interesting. Simon | -----Original Message----- | From: Dan Doel [mailto:dan.d...@gmail.com] | Sent: 09 September 2015 03:44 | To: Simon Peyton Jones | Cc: Edward Z. Yang; ghc-devs | Subject: Re: Unlifted data types | | On Tue, Sep 8, 2015 at 3:52 AM, Simon Peyton Jones | <simo...@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. | | It's missing the part that makes it convenient. | | type StrictList a = Force (StrictList' a) | data StrictList' a = Nil' | Cons' !a (StrictList a) | pattern Nil = Force Nil' | pattern Cons x xs = Force (Cons' x xs) | | mapStrict :: (a -> b) -> StrictList a -> StrictList b | mapStrict f Nil = Nil | mapStrict f (Cons x xs) = Cons (f x) (mapStrict f xs) | | But, really, my point is that we already almost have StrictList | _today_: | | data StrictList a = Nil | Cons !a !(StrictList a) | | The only difference between this and the previous definition | (denotationally, at least) is the outer-most level. That's why I liked | the original proposal (which probably disappeared too fast for most | people to read it), which was more like being able to talk about `!a` | as a thing in itself. It's the only semantic gap in being able to | define totally unlifted data types right now. So maybe it's also the | only operational gap that needs to be plugged, as well. | | But that was vetoed because `!a` in a data declaration doesn't make a | constructor with type `!a -> ...`, but `a -> ...` which evaluates. | | > 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. | | Yes, true. It only helps ensure that the implementation is correct, | rather than enabling a previously impossible construction. Kind of | like certain uses of GADTs vs. phantom types. | | But the ArrayArray people already want UMVar (and the like) anyway, | because it cuts out a layer of indirection for types that are already | unlifted. | | -- Dan _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs