Linear Types: ready for review

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Linear Types: ready for review

Spiwack, Arnaud
Dear GHC devs,

The linear types patch is ready for review!
https://gitlab.haskell.org/ghc/ghc/merge_requests/852

It is a fairly large patch (~3500loc of change to the compiler itself,
with a ~2000loc diff on the testsuite). And it's gone through a lot of
redesigns. The issue with a patch like this is that it is rather easy
to get reviewer fatigue and just let things through.

This is why I want to encourage as many people as possible to give a
thorough review of part of the patch. Even 15 minutes of your time
would be tremendously helpful!

Here is what I suggest: pick a part of the compiler you know well, and
look at how the patch affects it. If there is something that you don't
understand let us know! Either in the MR discussion, or send an email
to Krzysztof and me. We will answer and update the documentation.

---

If you are still unsure where to start, here are what we consider to
be the main entry points to the patch:

- The file Multiplicity, which defines type Mult = Type, the Scaled
  type and functions unrestricted, linear, pattern synonyms One and
  Omega, quick submultiplicity test submult
- The change to FunTy and new mkFunTy in TyCoRep, where the
  multiplicity argument is added
- The change to funTyCon in TysPrim
- The new unrestrictedFunTyCon and multiplicityTy in TysWiredIn
- Var has now a new field varMult; functions such as
  updateVarTypeAndMult can be used to update multiplicity (e.g. when
  zonking). In Core, the multiplicity of a lambda is indicated by its
  varMult; multiplicity of a case expression is indicated by varMult
  of the case binder.
- The functions mkDataConRepXin basicTypes/MkId and and
  dataConUserType function in basicTypes/DataCon, which are adding
  multiplicity variables to constructors. The change to wrapper_reqd
  means that all data constructors have a wrapper now.
- The file UsageEnv defines a map from a variable to its multiplicity,
  used when typechecking
- Calls to submult and tcSubMult, which guide multiplicity checking in
  the type checker
- ensureSubMult and its calls, which guide multiplicity checking in
  Lint
 
---

A more in-depth documentation and overview of the patch is on the
wiki: https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation

It has a table of contents which you can use as yet another way to
find a starting point.

---

If any of these resources are lacking, let us know too! We'll make
sure to update them.

---

Finally, I'll be holding a project session on Linear Types in ZüriHac
next month. Where we can have further, more in-depth discussion about
the patch, finalise its documentation, and address outstanding
requests from reviews.



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Linear Types: ready for review

Wolfgang Jeltsch-3
Am Freitag, den 03.05.2019, 11:52 +0200 schrieb Spiwack, Arnaud:
>   * The file `Multiplicity`, which defines `type Mult = Type`, the
>     `Scaled` type and functions unrestricted, linear, pattern
>      synonyms `One` and `Omega`, quick submultiplicity test submult

Could `Omega` **please** be changed to `Many`? I argued long time
ago [1] already why `Omega` seems to be a bad choice and `Many` to be a
much better alternative. Unfortunately, my arguments, while having been
positively received, didn’t really have a considerable impact on the
proposal and implementation; still today the proposal reflects only part
of them, as it did 1½ months ago [2].

Notation is important, since good notation aids and bad notation
confuses. Notation is something that is very likely to stay once it has
been in use. Given that changing this one identifier shouldn’t be a big
deal, I’m asking you keenly to make this change.

Following are my arguments again:

  1. It’s already questionable that the paper uses the symbol ω. The
     choice of this symbol stems from its use for the smallest
     transfinite ordinal number, the number that denotes the length of
     an infinite list, if you so wish. This doesn’t match the use of ω
     in this proposal, where it stands for the possibility to use a
     value *any number* of times and thus rather corresponds to
     something like ℕ ∪ {ω}.

  2. Even if ω is considered okay for being used in the theory, we
     shouldn’t use the identifier `Omega` in Haskell. `Omega` doesn’t
     name the multiplicity; instead it names the symbol that is used to
     denote the multiplicity.

  3. To people not into something like ordinal numbers or ω-words,
     `Omega` doesn’t mean anything. Therefore its use would rather
     confuse than enlighten those people.

I propose to pick multiplicity identifiers that capture the actual
meanings of the multiplicities and are consistent with existing
identifiers at the same time. `Control.Applicative` already uses the
identifiers `some`, `many`, and `optional`. Thus we should use `Many`
for what is now called `Omega` and `Optional` for the affinity
multiplicity in case it’s added at some time. I think `One` is a good
name and thus should be kept. The 0-multiplicity would probably be best
named `None`.

All the best,
Wolfgang

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Linear Types: ready for review

Wolfgang Jeltsch-3
Hi, again!

Here are the missing links to my previous e-mail:

[1] https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-437271986
[2] https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-476125233

All the best,
Wolfgang

Am Sonntag, den 05.05.2019, 14:02 +0300 schrieb Wolfgang Jeltsch:

> Am Freitag, den 03.05.2019, 11:52 +0200 schrieb Spiwack, Arnaud:
> >   * The file `Multiplicity`, which defines `type Mult = Type`, the
> >     `Scaled` type and functions unrestricted, linear, pattern
> >      synonyms `One` and `Omega`, quick submultiplicity test submult
>
> Could `Omega` **please** be changed to `Many`? I argued long time
> ago [1] already why `Omega` seems to be a bad choice and `Many` to be
> a much better alternative. Unfortunately, my arguments, while having
> been positively received, didn’t really have a considerable impact on
> the proposal and implementation; still today the proposal reflects
> only part of them, as it did 1½ months ago [2].
>
> Notation is important, since good notation aids and bad notation
> confuses. Notation is something that is very likely to stay once it
> has been in use. Given that changing this one identifier shouldn’t be
> a big deal, I’m asking you keenly to make this change.
>
> Following are my arguments again:
>
>   1. It’s already questionable that the paper uses the symbol ω. The
>      choice of this symbol stems from its use for the smallest
>      transfinite ordinal number, the number that denotes the length of
>      an infinite list, if you so wish. This doesn’t match the use of ω
>      in this proposal, where it stands for the possibility to use a
>      value *any number* of times and thus rather corresponds to
>      something like ℕ ∪ {ω}.
>
>   2. Even if ω is considered okay for being used in the theory, we
>      shouldn’t use the identifier `Omega` in Haskell. `Omega` doesn’t
>      name the multiplicity; instead it names the symbol that is used
>      to denote the multiplicity.
>
>   3. To people not into something like ordinal numbers or ω-words,
>      `Omega` doesn’t mean anything. Therefore its use would rather
>      confuse than enlighten those people.
>
> I propose to pick multiplicity identifiers that capture the actual
> meanings of the multiplicities and are consistent with existing
> identifiers at the same time. `Control.Applicative` already uses the
> identifiers `some`, `many`, and `optional`. Thus we should use `Many`
> for what is now called `Omega` and `Optional` for the affinity
> multiplicity in case it’s added at some time. I think `One` is a good
> name and thus should be kept. The 0-multiplicity would probably be
> best named `None`.
>
> All the best,
> Wolfgang

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Linear Types: ready for review

Eric Seidel-3
In reply to this post by Wolfgang Jeltsch-3
Hi Wolfgang,

Just FYI, the GHC Steering Committee is currently reviewing a few more design decisions for the Linear Types proposal, one of which is the name of the unrestricted multiplicity. The current recommendation is to use Many rather than Omega (https://mail.haskell.org/pipermail/ghc-steering-committee/2019-May/001082.html).

Thanks!
Eric

On Sun, May 5, 2019, at 07:02, Wolfgang Jeltsch wrote:

> Am Freitag, den 03.05.2019, 11:52 +0200 schrieb Spiwack, Arnaud:
> >   * The file `Multiplicity`, which defines `type Mult = Type`, the
> >     `Scaled` type and functions unrestricted, linear, pattern
> >      synonyms `One` and `Omega`, quick submultiplicity test submult
>
> Could `Omega` **please** be changed to `Many`? I argued long time
> ago [1] already why `Omega` seems to be a bad choice and `Many` to be a
> much better alternative. Unfortunately, my arguments, while having been
> positively received, didn’t really have a considerable impact on the
> proposal and implementation; still today the proposal reflects only part
> of them, as it did 1½ months ago [2].
>
> Notation is important, since good notation aids and bad notation
> confuses. Notation is something that is very likely to stay once it has
> been in use. Given that changing this one identifier shouldn’t be a big
> deal, I’m asking you keenly to make this change.
>
> Following are my arguments again:
>
>   1. It’s already questionable that the paper uses the symbol ω. The
>      choice of this symbol stems from its use for the smallest
>      transfinite ordinal number, the number that denotes the length of
>      an infinite list, if you so wish. This doesn’t match the use of ω
>      in this proposal, where it stands for the possibility to use a
>      value *any number* of times and thus rather corresponds to
>      something like ℕ ∪ {ω}.
>
>   2. Even if ω is considered okay for being used in the theory, we
>      shouldn’t use the identifier `Omega` in Haskell. `Omega` doesn’t
>      name the multiplicity; instead it names the symbol that is used to
>      denote the multiplicity.
>
>   3. To people not into something like ordinal numbers or ω-words,
>      `Omega` doesn’t mean anything. Therefore its use would rather
>      confuse than enlighten those people.
>
> I propose to pick multiplicity identifiers that capture the actual
> meanings of the multiplicities and are consistent with existing
> identifiers at the same time. `Control.Applicative` already uses the
> identifiers `some`, `many`, and `optional`. Thus we should use `Many`
> for what is now called `Omega` and `Optional` for the affinity
> multiplicity in case it’s added at some time. I think `One` is a good
> name and thus should be kept. The 0-multiplicity would probably be best
> named `None`.
>
> All the best,
> Wolfgang
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Linear Types: ready for review

Spiwack, Arnaud
Indeed,

I'd like to insist, to dispell any ambiguity, that none of the syntax in the above-mentioned patch is definitive. We had to make up some syntax because we needed it for testing, but the decision on what the actual syntax will be has not been made yet. It's too early to worry :)

I'll, of course, update the proposal with the committee's decision when it is made.

Best,
Arnaud

On Sun, May 5, 2019 at 4:27 PM Eric Seidel <[hidden email]> wrote:
Hi Wolfgang,

Just FYI, the GHC Steering Committee is currently reviewing a few more design decisions for the Linear Types proposal, one of which is the name of the unrestricted multiplicity. The current recommendation is to use Many rather than Omega (https://mail.haskell.org/pipermail/ghc-steering-committee/2019-May/001082.html).

Thanks!
Eric

On Sun, May 5, 2019, at 07:02, Wolfgang Jeltsch wrote:
> Am Freitag, den 03.05.2019, 11:52 +0200 schrieb Spiwack, Arnaud:
> >   * The file `Multiplicity`, which defines `type Mult = Type`, the
> >     `Scaled` type and functions unrestricted, linear, pattern
> >      synonyms `One` and `Omega`, quick submultiplicity test submult
>
> Could `Omega` **please** be changed to `Many`? I argued long time
> ago [1] already why `Omega` seems to be a bad choice and `Many` to be a
> much better alternative. Unfortunately, my arguments, while having been
> positively received, didn’t really have a considerable impact on the
> proposal and implementation; still today the proposal reflects only part
> of them, as it did 1½ months ago [2].
>
> Notation is important, since good notation aids and bad notation
> confuses. Notation is something that is very likely to stay once it has
> been in use. Given that changing this one identifier shouldn’t be a big
> deal, I’m asking you keenly to make this change.
>
> Following are my arguments again:
>
>   1. It’s already questionable that the paper uses the symbol ω. The
>      choice of this symbol stems from its use for the smallest
>      transfinite ordinal number, the number that denotes the length of
>      an infinite list, if you so wish. This doesn’t match the use of ω
>      in this proposal, where it stands for the possibility to use a
>      value *any number* of times and thus rather corresponds to
>      something like ℕ ∪ {ω}.
>
>   2. Even if ω is considered okay for being used in the theory, we
>      shouldn’t use the identifier `Omega` in Haskell. `Omega` doesn’t
>      name the multiplicity; instead it names the symbol that is used to
>      denote the multiplicity.
>
>   3. To people not into something like ordinal numbers or ω-words,
>      `Omega` doesn’t mean anything. Therefore its use would rather
>      confuse than enlighten those people.
>
> I propose to pick multiplicity identifiers that capture the actual
> meanings of the multiplicities and are consistent with existing
> identifiers at the same time. `Control.Applicative` already uses the
> identifiers `some`, `many`, and `optional`. Thus we should use `Many`
> for what is now called `Omega` and `Optional` for the affinity
> multiplicity in case it’s added at some time. I think `One` is a good
> name and thus should be kept. The 0-multiplicity would probably be best
> named `None`.
>
> All the best,
> Wolfgang
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Linear Types: ready for review

GHC - devs mailing list
In reply to this post by Spiwack, Arnaud

Dear GHC developers and friends

 

I would like to urge you to review, and help to improve, this patch.

 

Adding linear types to Haskell is a big change that touches a lot of code.   That makes the patch a bit daunting.  But GHC is supposed to be a laboratory for advanced stuff, and this is a great example.   The authors (esp Arnaud, Krzysztof, and Jean-Philippe) have invested a lot of effort in the paper, the proposal, and now the patch.  And lots of people are interested in the result.  In short, we owe it to them to give their work serious attention.

 

But please don’t think “oh, I’m not qualified and anyway Simon will look at it”.  I will, of course, but like you I’m too busy.  And a far-reaching change like this needs many eyes.   Moreover, assuming it’s committed, this code will be us for a long time;       most future developers will be no better qualified than you, but they’ll still have to deal with it!  So if you get bamboozled, make constructive suggestions about what sorts of Notes or explanation would un-bamboozle you.  Don’t just assume you are too stupid; that way likes an un-maintainable code base.

 

So please jump in there.  This is  your compiler.

 

Thanks

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Spiwack, Arnaud
Sent: 03 May 2019 10:52
To: GHC developers <[hidden email]>
Cc: Krzysztof Gogolewski <[hidden email]>
Subject: Linear Types: ready for review

 

Dear GHC devs,

The linear types patch is ready for review!
https://gitlab.haskell.org/ghc/ghc/merge_requests/852

It is a fairly large patch (~3500loc of change to the compiler itself,
with a ~2000loc diff on the testsuite). And it's gone through a lot of
redesigns. The issue with a patch like this is that it is rather easy
to get reviewer fatigue and just let things through.

This is why I want to encourage as many people as possible to give a
thorough review of part of the patch. Even 15 minutes of your time
would be tremendously helpful!

Here is what I suggest: pick a part of the compiler you know well, and
look at how the patch affects it. If there is something that you don't
understand let us know! Either in the MR discussion, or send an email
to Krzysztof and me. We will answer and update the documentation.

---

If you are still unsure where to start, here are what we consider to
be the main entry points to the patch:

- The file Multiplicity, which defines type Mult = Type, the Scaled
  type and functions unrestricted, linear, pattern synonyms One and
  Omega, quick submultiplicity test submult
- The change to FunTy and new mkFunTy in TyCoRep, where the
  multiplicity argument is added
- The change to funTyCon in TysPrim
- The new unrestrictedFunTyCon and multiplicityTy in TysWiredIn
- Var has now a new field varMult; functions such as
  updateVarTypeAndMult can be used to update multiplicity (e.g. when
  zonking). In Core, the multiplicity of a lambda is indicated by its
  varMult; multiplicity of a case expression is indicated by varMult
  of the case binder.
- The functions mkDataConRepXin basicTypes/MkId and and
  dataConUserType function in basicTypes/DataCon, which are adding
  multiplicity variables to constructors. The change to wrapper_reqd
  means that all data constructors have a wrapper now.
- The file UsageEnv defines a map from a variable to its multiplicity,
  used when typechecking
- Calls to submult and tcSubMult, which guide multiplicity checking in
  the type checker
- ensureSubMult and its calls, which guide multiplicity checking in
  Lint
 
---

A more in-depth documentation and overview of the patch is on the
wiki: https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation

It has a table of contents which you can use as yet another way to
find a starting point.

---

If any of these resources are lacking, let us know too! We'll make
sure to update them.

---

Finally, I'll be holding a project session on Linear Types in ZüriHac
next month. Where we can have further, more in-depth discussion about
the patch, finalise its documentation, and address outstanding
requests from reviews.


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs