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

[Vitaly Bragilevsky]

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 <rae at cs.brynmawr.edu>
wrote:

> 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://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20181018/b0697611/attachment.html>