Unlifted data types

[Dan Doel]

Here are some additional thoughts.

If we examine an analogue of some of your examples:

    data MutVar a = MV (MutVar# RealWorld a)

    main = do
      let mv# = undefined
      let mv = MV mv#
      putStrLn "Okay."

The above is illegal. Instead we _must_ write:

      let !mv# = undefined

which signals that evaluation is occurring. So it is impossible to
accidentally go from:

    main = do
      let mv = MV undefined
      putStrLn "Okay."

which prints "Okay.", to something that throws an exception, without
having a pretty good indication that you're doing so. I would guess
this is desirable, so perhaps it should be mandated for Unlifted as
well.

----

However, the above point confuses me with respect to another example.
The proposal says that:

    data Id :: * -> Unlifted where
      Id :: a -> Id a

could/should be compiled with no overhead over `a`, like a newtype.
However, if Unlifted things have operational semantics like #, what
does the following do:

    let x :: Id a
        !x = Id undefined

The ! should evaluate to the Id constructor, but we're not
representing it, so it actually doesn't evaluate anything? But:

    let x :: Id a
        !x = undefined

throws an exception? Whereas for newtypes, both throw exceptions with
a !x definition, or don't with an x definition? Is it actually
possible to make Id behave this way without any representational
overhead?

I'm a little skeptical. I think that only Force (and Box) might be
able to have no representational overhead.

-- Dan


On Fri, Sep 4, 2015 at 5:23 PM, Edward Z. Yang <ezyang at mit.edu> wrote:
> 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