Unlifted data types

[Dan Doel]

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.

----

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


On Fri, Sep 4, 2015 at 2:12 PM, Edward Z. Yang <ezyang at mit.edu> wrote:
> Excerpts from Dan Doel's message of 2015-09-04 09:57:42 -0700:
>> All your examples are non-recursive types. So, if I have:
>>
>>     data Nat = Zero | Suc Nat
>>
>> what is !Nat? Does it just have the outer-most part unlifted?
>
> Just the outermost part.
>
>> Is the intention to make the !a in data type declarations first-class,
>> so that when we say:
>>
>>     data Nat = Zero | Suc !Nat
>>
>> the !Nat part is now an entity in itself, and it is, for this
>> declaration, the set of naturals, whereas Nat is the flat domain?
>
> No, in fact, there is a semantic difference between this and strict
> fields (which Paul pointed out to me.) There's now an updated proposal
> on the Trac which partially solves this problem.
>
> Edward