LGTM -- thanks
| -----Original Message-----
| From: ghc-steering-committee
| On Behalf Of Richard Eisenberg
| Sent: 15 October 2018 17:12
| To: ghc-steering-committee@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@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
