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
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
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
LGTM -- thanks
| -----Original Message-----
| From: ghc-steering-committee
With item 4 in mind: shouldn't we require explicitly this new specification
to be an extension or revision of your current 'System FC, as implemented
in GHC' paper in docs/core-spec/core-spec.pdf with the same structure etc.
That'd give this document more formal status which is convenient for
referring to it later.
Vitaly
On Mon, Oct 15, 2018 at 9:12 AM Richard Eisenberg
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://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
participants (3)
-
Richard Eisenberg -
Simon Peyton Jones -
Vitaly Bragilevsky