[ghc-steering-committee] Unlifted Newtypes (#98)

[Simon Peyton Jones]

Yes, I like this proposal.

Some thoughts about the text of the proposal, here
https://github.com/andrewthad/ghc-proposals/blob/unboxed_newtypes/proposals/0000-unlifted-newtypes.rst

* Data families.  "Under this proposal, this restriction (that data families
  must have a lifted return kind) would be lifted".  That's fine, but I'd like
  some additional text pointing out that the reason for this is that we can
  define newtype instances of that family.  Indeed, if the return kind is
  only unlifted (e.g. TYPE 'IntRep) then we can /only/ define newtype instances
  (because data instances would be lifted).  If the return kind is polymorphic
  (which I assume is allowed -- better to say) then we can define both kinds
  of instances.

* "More generally, if an unlifted newtype is well-kinded, then its kind should
  always be inferrable."  I'm not sure exactly what this means, or if it is correct.
  What we /do/ want is that if the programmer writes a CUSK for each type constructor
  then all the kinds work out.  The question of whether you can /infer/ such kinds
  is another matter, and probably orthogonal to this proposal.

  I think that might be all we need.  E.g. for Recurse, you can't write a CUSK
  because it would be inifinite.

  The text should give the CUSKs for GoodA and GoodB, and explain why you can't
  give one for BadA and BadB.



|  -----Original Message-----
|  From: ghc-steering-committee [mailto:ghc-steering-committee-
|  bounces at haskell.org] On Behalf Of Richard Eisenberg
|  Sent: 22 February 2018 04:19
|  To: Manuel M T Chakravarty <chak at justtesting.org>
|  Cc: ghc-steering-committee at haskell.org
|  Subject: Re: [ghc-steering-committee] Unlifted Newtypes (#98)
|  
|  Conversation here has ebbed down. I am understanding this to mean
|  acceptance, in accordance with my recommendation. In roughly a week,
|  I'll conclude that indeed we have accepted this proposal.
|  
|  Thanks,
|  Richard
|  
|  > On Feb 12, 2018, at 9:43 PM, Manuel M T Chakravarty
|  <chak at justtesting.org> wrote:
|  >
|  > Given that you think the levity polymorphism-related implications
|  are fine, the proposal seems fine to me.
|  >
|  > Manuel
|  >
|  >> 12.02.2018 11:28 Richard Eisenberg <rae at cs.brynmawr.edu>:
|  >>
|  >> I have been assigned as the shepherd for proposal #98: Unlifted
|  Newtypes, https://github.com/ghc-proposals/ghc-proposals/pull/98
|  >>
|  >> Summary:
|  >>
|  >> This proposal suggests lifting the current restriction that newtype
|  kinds are always Type -- that is, TYPE LiftedRep. At its core, that's
|  the entire proposal; the rest is just motivation (which is quite well-
|  written, if you're feeling unmotivated) and consequences. Here are a
|  few of the twists and turns:
|  >>
|  >> - The non-Type kinds should be inferred, based on the kind of the
|  wrapped type. In the event of a trivial recursive newtype (e.g.,
|  newtype Void = Void Void), the kind would default to lifted, though
|  the user could override this behavior with a kind signature using GADT
|  syntax. The proposal author conjectures that all inhabited unlifted
|  newtypes will have inferrable kinds; I've not tried hard to prove or
|  refute this claim.
|  >>
|  >> - The proposal suggests that the Coercible mechanism be extended to
|  deal with unlifted types. This could be handled by generalizing the
|  type of `coerce` to be levity-polymorphic. Note that doing so does not
|  violate levity polymorphism restrictions, because coerce always
|  inlines to a cast, and casts are erased before code generation. If
|  `coerce` is generalized, GeneralizedNewtypeDeriving will work over the
|  new unlifted newtypes.
|  >>
|  >> - The proposal suggests that newtypes can indeed be levity-
|  polymorphic: newtype Id# (r :: RuntimeRep) (a :: TYPE r) = MkId# a.
|  This does not appear to violate levity polymorphism restrictions,
|  either, because the MkId# constructor doesn't appear in Core. Any use
|  of this newtype will have to be specialized to a certain RuntimeRep,
|  but that specialization would already be guaranteed by the existing
|  levity polymorphism restrictions.
|  >>
|  >> The main drawback in the proposal is that this is the first way
|  users can create their own unlifted types. Accordingly, a user might
|  unwittingly use an unlifted type where they expect laziness; the
|  strictness that, say, an unlifted-variable pattern binding would
|  induce would be a surprise and hard to find.
|  >>
|  >> Opinion & recommendation:
|  >>
|  >> I am in support of this proposal and propose acceptance. The
|  motivation section in the proposal is compelling, and this seems a
|  natural generalization of existing structures. There are no concrete
|  syntax ramifications. Given the existing levity polymorphism set-up,
|  this proposal seems like an easy win.
|  >>
|  >> If we are concerned about unexpected strictness, we could require
|  that all unlifted newtypes be suffixed with one or more hashes, but I
|  do not recommend doing so, instead encouraging library-writers to be
|  sensitive to this problem, giving those authors the latitude to choose
|  the best name for their types.
|  >>
|  >> Thanks,
|  >> Richard
|  >>
|  >> _______________________________________________
|  >> ghc-steering-committee mailing list
|  >> ghc-steering-committee at haskell.org
|  >> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-
|  committee
|  >
|  
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-
|  committee