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