Unlifted data types

[Simon Peyton Jones]

|  (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 at 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
|  <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.
|  
|  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