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