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