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@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