Unlifted data types

[Dan Doel]

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