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

[Simon Peyton Jones]

I agree.

I think that items 1-4 could be more clearly stated under the principle "pay as you go".  That is:

  If a module does not use -XLinearTypes, it should not pay for it:
  - If a program typechecks now, it should continue to typecheck
  - Error messages should not become more confusing
  - :type should not become confusing
  - Compilation time should not increase significantly
  - Runtime should not increase (at all)

But for all of these points there is wiggle room if -XLinearTypes is switched on.
  - We'd prefer that all existing type-correct programs remain so,
    but some corner cases might change
  - Error messages may well have to report linear stuff
  - Ditto :type
  - Compilation time should not increase markedly, but again
    there is more wiggle room
  - Runtime really should not increase.  I don't want linearity
    to impede optimisation.

For the migration-of-base question, I'm not sure it's reasonable to
ask for a migration plan in advance.  It's a tricky topic, as we saw
with the Foldable and Monad/Applicative saga.  Maybe we can say
if/when pressure emerges to really make the linear functions part
of base, we'd like to see a propose migration plan before execution?
The CLC might play a role here too.

Simon

|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org>
|  On Behalf Of Richard Eisenberg
|  Sent: 11 October 2018 22:46
|  To: ghc-steering-committee at haskell.org
|  Subject: [ghc-steering-committee] Linear types (#111): conditional
|  acceptance
|  
|  Hi all,
|  
|  Several members of the steering committee met at ICFP to discuss the
|  Linear Types proposal, #111. While some concerns were raised about the
|  utility of the proposed approach (as also explained on the GitHub trail),
|  the committee agreed that the best way forward would be to accept the
|  proposal.
|  
|  I thus propose *conditional acceptance*, subject to these conditions,
|  which were discussed at ICFP:
|  
|  1. 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.
|  
|  2. Type inference must remain backward-compatible. All programs accepted
|  today must be accepted when -XLinearTypes is not in effect. Ideally,
|  these programs would also be accepted when -XLinearTypes is in effect,
|  but there can be some wiggle room here.
|  
|  3. 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.
|  
|  4. 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.
|  
|  5. There must 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?
|  
|  6. 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.
|  
|  7. There must be a specification (in some typeset document) of the new
|  core language, written out for public inspection.
|  
|  If the final version of this should violate these prescriptions, it does
|  not immediately mean we are at an impasse -- it just means that we need
|  to have more discussion.
|  
|  Before officially posting this on #111 on behalf of the committee, I'd
|  like some feedback on this recommendation. As usual, I'll take silence
|  for agreement.
|  
|  Discussion period: 1 week (shortened due to the fact that many have
|  already participated in formulating this list)
|  
|  Thanks!
|  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%7C303607a28a294ae7cd
|  f008d62fc2ea8d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6367489115454
|  76671&sdata=4ExqdXNPwu7CLr%2BV3FgfU8VDVbZsbW1DuMYdd5lNBh4%3D&rese
|  rved=0