LGTM -- thanks | -----Original Message----- | From: ghc-steering-committee <ghc-steering-committee-bounces@haskell.org> | 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