Unlifted data types

[Edward Z. Yang]

Excerpts from Dan Doel's message of 2015-09-04 13:09:26 -0700:
> Okay. That answers another question I had, which was whether MutVar#
> and such would go in the new kind.
> 
> So now we have partial, extended natural numbers:
> 
>     data PNat :: * where
>       PZero :: PNat
>       PSuc :: PNat -> PNat
> 
> A flat domain of natural numbers:
> 
>     data FNat :: * where
>       FZero :: FNat
>       FSuc :: !FNat -> FNat
> 
> And two sets of natural numbers:
> 
>     Force FNat :: Unlifted
> 
>     data UNat :: Unlifted where
>       UZero :: UNat
>       USuc :: UNat -> UNat
> 
> And really perhaps two flat domains (and three sets), if you use Force
> instead of !, which would differ on who ensures the evaluation. That's
> kind of a lot of incompatible definitions of essentially the same
> thing (PNat being the significantly different thing).
> 
> I was kind of more enthused about first class !a. For instance, if you
> think about the opening quote by Bob Harper, he's basically wrong. The
> flat domain FNat is the natural numbers (existing in an overall lazy
> language), and has the reasoning properties he wants to teach students
> about with very little complication. It'd be satisfying to recognize
> that unlifting the outer-most part gets you exactly there, with
> whatever performance characteristics that implies. Or to get rid of !
> and use Unlifted definitions instead.
> 
> Maybe backwards compatibility mandates the duplication, but it'd be
> nice if some synthesis could be reached.

I would certainly agree that in terms of the data that is representable,
there is not much difference; but there is a lot of difference for the
client between Force and a strict field. If I write:

    let x = undefined
        y = Strict x
    in True

No error occurs with:

    data Strict = Strict !a

But an error occurs with:

    data Strict = Strict (Force a)

One possibility for how to reconcile the difference for BC is to posit
that there are just two different constructors:

    Strict  ::       a -> Strict a
    Strict! :: Force a -> Strict a

But this kind of special handling is a bit bothersome. Consider:

    data SPair a b = SPair (!a, !b)

The constructor has what type?  Probably

    SPair :: (Force a, Force b) -> SPair a

and not:

    SPair :: (a, b) -> SPair a

> It'd also be good to think about/specify how this is going to interact
> with unpacked/unboxed sums.

I don't think it interacts any differently than with unpacked/unboxed
products today.

Edward