[ghc-steering-committee] Linear types (#111): conditional acceptance

[Simon Peyton Jones]

LGTM -- thanks

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org>
|  On Behalf Of Richard Eisenberg
|  Sent: 15 October 2018 17:12
|  To: ghc-steering-committee at haskell.org
|  Subject: Re: [ghc-steering-committee] Linear types (#111): conditional
|  acceptance
|  
|  Revised proposal, in light of Simon's comments:
|  
|  I propose that #111 be *conditionally accepted*, with the following
|  conditions.
|  
|  1. The extension is pay-as-you-go; users who do not enable -XLinearTypes
|  and who do not import modules that do should never need to know about the
|  feature:
|    a. Error messages must remain free of mention of linear types, unless -
|  XLinearTypes is in effect (or some flag like -fprint-linear-types is on).
|  The same must be true of using the `:type` facility in GHCi.
|    b. Type inference must remain backward-compatible. All programs
|  accepted today must be accepted when -XLinearTypes is not in effect.
|    c. Compile times for programs without -XLinearTypes must not unduly
|  increase. Anything approaching or over a 2% across-the-board increase in
|  compile times would be a cause for concern.
|    d. There must be no degradation in runtime performance of GHC-compiled
|  programs. Linear types in Core might, for example, make some
|  optimizations harder to apply; however, we must find a way to get runtime
|  performance on par with what we have today.
|  
|  2. We must work out an acceptable syntax for this all. In particular, :
|  in types is taken by the list-cons operator, so we'll need something new.
|  
|  3. The theory of the linear types must be sound. This seems to be the
|  case today, but as things evolve, we want to state explicitly that this
|  must remain true. In particular, we must be able to rely on the safety of
|  using linear mutable arrays.
|  
|  4. There must be a specification (in some typeset document) of the new
|  core language, written out for public inspection.
|  
|  In addition to the stronger conditions above, we ask for these weaker
|  conditions:
|  
|  5. The worries in (1), above, should not become unduly worse when -
|  XLinearTypes is enabled. For example, it is ideal if all programs that
|  are accepted without -XLinearTypes are still accepted with -XLinearTypes,
|  but there is considerably more wiggle room here. Similarly with compile
|  times: a compile-time regression with -XLinearTypes are more acceptable
|  than a regression without -XLinearTypes, but would still be a cause for
|  concern.
|  
|  6. There should be a story for a migration of `base`. The committee is
|  concerned that, once linear types hits, there will be a great demand to
|  incorporate linear types into `base`. (Note that `fmap` may want a linear
|  type, and due to Functor's status as a superclass of Monad, `fmap` is
|  really baked in.) How will this work? In particular, how will Haddock
|  render newly-linearized types?
|  
|  If the final version of -XLinearTypes should violate these prescriptions,
|  it does not immediately mean we are at an impasse -- it just means that
|  we need to have more discussion.
|  
|  More comments / suggestions are very welcome!
|  Richard
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.has
|  kell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-
|  committee&data=02%7C01%7Csimonpj%40microsoft.com%7C50550b93f6a448a406
|  7608d632b8f7d0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6367521673523
|  59760&sdata=eVCZLRwjfzjHYjd5bdF%2BRw5kj%2B92jskU9eJOjwzExig%3D&re
|  served=0