Please review #273: Local Types, Shepherd: Eric

older
Updated partial type signatures...

Joachim Breitner

4 Nov 2019 4 Nov '19

3:21 a.m.

Dear Committee, this is your secretary speaking: Local Types has been updated by David Feuer https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc... I propose Eric as the shepherd. Please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you. Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Attachments:

signature.asc (application/pgp-signature — 833 bytes)

Show replies by date

Eric Seidel

23 Nov 23 Nov

11:32 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

Hi all, I am the shepherd for proposal #273: Local Types (https://github.com/ghc-proposals/ghc-proposals/pull/273). This proposal would add support for local type and instance (class and type-family) definitions as a means of addressing the Configurations Problem, which as I understand it is essentially "How can we *implicitly* pass around dynamically determined values in a safe manner?" The `reflection` package provides an answer to this question with its `Reifies` class, but the implementation relies on `unsafeCoerce` and the implementation details of how GHC represents single-method class dictionaries. The proposal argues that we could safely implement the `reflection` package with local types and instances, if only Haskell had such things! As a motivation I find this pretty compelling. The proposal introduces a few restrictions on local types and instances, and functions that contain them, primarily as a means of providing a no-escape property: local types must not be able to escape their defining scope. There are a couple ways this could happen. (1) The defining function could return a value of some local type. This is prohibited unless the value is wrapped in an existential, as otherwise the function simply could not be typed. (2) More interestingly, a type class with a functional dependency or a type family could leak the local type to the outer scope. Consider the following: ``` type family F x foo x = x where data T type instance F Int = T bar :: F Int bar = ??? ``` What type should `bar` have? The proposal says that all instances are still global, which would mean `bar :: T`, which is absurd. To avoid cases like this, the proposal introduces a restriction on local instances that says local types may not be determined by types from an outer scope (either via fundeps or type families). I believe these two restrictions are sufficient to guarantee the no-escape property. I think the key question that is left unanswered by the proposal is how exactly we might implement local types in GHC. The proposal (as a guideline, not necessarily an implementation strategy) to think of local types as global types that are implicitly indexed by the type and value parameters of its defining function. But GHC does not yet have dependent types, so this is not a workable implementation strategy. Another possible strategy would be to add type/instance definitions to Core, but as Simon PJ points out this would be a tremendous amount of work, so also not a practical direction for the short-term. Lastly, Arnaud suggests that we treat local types like global types that are only defined in the local scope, i.e. let the renamer deal with them entirely. Local instances are different as they must capture locally-bound variables, but there's nothing conceptually difficult about constructing new instances dynamically (this is what ImplicitParams does). There are some remaining questions around how to ensure the optimizer doesn't incorrectly swap two instances for a local type, but these seem tractable. I think Arnaud's suggestion is a promising and feasible strategy for implementing this proposal without new research, so my recommendation is that we return the proposal for revision and recommend the author incorporate Arnaud's suggestions. As usual, please provide technical feedback on the PR, and feedback on my recommendation here on the mailing list. Eric On Mon, Nov 4, 2019, at 03:21, Joachim Breitner wrote:

...

Dear Committee,

this is your secretary speaking:

Local Types has been updated by David Feuer https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc...

I propose Eric as the shepherd.

Please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you.

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Attachments: * signature.asc

Joachim Breitner

11:46 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

Hi, thanks for the great summary. My gut feeling when looking at this from afar is “I’d love to have local types and instances, but surely it must be hard and expensive to add that to Haskell, else we would already have it, so this gotta be flawed”. But that is not a fair initial sentiment. A renamer-focused approach to local types + some support for local instances sound like a reasonable way forward. Cheers, Joachim Am Samstag, den 23.11.2019, 11:32 -0500 schrieb Eric Seidel:

...

Hi all,

I am the shepherd for proposal #273: Local Types (https://github.com/ghc-proposals/ghc-proposals/pull/273).

This proposal would add support for local type and instance (class and type-family) definitions as a means of addressing the Configurations Problem, which as I understand it is essentially "How can we *implicitly* pass around dynamically determined values in a safe manner?" The `reflection` package provides an answer to this question with its `Reifies` class, but the implementation relies on `unsafeCoerce` and the implementation details of how GHC represents single-method class dictionaries. The proposal argues that we could safely implement the `reflection` package with local types and instances, if only Haskell had such things! As a motivation I find this pretty compelling.

The proposal introduces a few restrictions on local types and instances, and functions that contain them, primarily as a means of providing a no-escape property: local types must not be able to escape their defining scope. There are a couple ways this could happen. (1) The defining function could return a value of some local type. This is prohibited unless the value is wrapped in an existential, as otherwise the function simply could not be typed. (2) More interestingly, a type class with a functional dependency or a type family could leak the local type to the outer scope. Consider the following:

``` type family F x

foo x = x where data T type instance F Int = T

bar :: F Int bar = ??? ```

What type should `bar` have? The proposal says that all instances are still global, which would mean `bar :: T`, which is absurd. To avoid cases like this, the proposal introduces a restriction on local instances that says local types may not be determined by types from an outer scope (either via fundeps or type families). I believe these two restrictions are sufficient to guarantee the no-escape property.

I think the key question that is left unanswered by the proposal is how exactly we might implement local types in GHC. The proposal (as a guideline, not necessarily an implementation strategy) to think of local types as global types that are implicitly indexed by the type and value parameters of its defining function. But GHC does not yet have dependent types, so this is not a workable implementation strategy. Another possible strategy would be to add type/instance definitions to Core, but as Simon PJ points out this would be a tremendous amount of work, so also not a practical direction for the short-term. Lastly, Arnaud suggests that we treat local types like global types that are only defined in the local scope, i.e. let the renamer deal with them entirely. Local instances are different as they must capture locally-bound variables, but there's nothing conceptually difficult about constructing new instances dynamically (this is what ImplicitParams does). There are some remaining questions around how to ensure the optimizer doesn't incorrectly swap two instances for a local type, but these seem tractable.

I think Arnaud's suggestion is a promising and feasible strategy for implementing this proposal without new research, so my recommendation is that we return the proposal for revision and recommend the author incorporate Arnaud's suggestions.

As usual, please provide technical feedback on the PR, and feedback on my recommendation here on the mailing list.

Eric

On Mon, Nov 4, 2019, at 03:21, Joachim Breitner wrote:

...
Dear Committee,

this is your secretary speaking:

Local Types has been updated by David Feuer https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc...

I propose Eric as the shepherd.

Please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you.

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Attachments: * signature.asc

ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Simon Marlow

25 Nov 25 Nov

3:15 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

Having written a little C++ recently (yeah I know) where you can have local type definitions, it feels entirely natural and I started to notice the lack of them in Haskell. So I support the proposal. My intuition is that we ought to be able to treat local types in the same way as local variables: they are entities with scoping rules enforced by the renamer. That is, a local type would be an ordinary TyCon with a Name and so forth. Having only read your email and not the proposal, that sounds the same as Arnuad's suggestion. Cheers Simon On Sat, 23 Nov 2019 at 16:32, Eric Seidel wrote:

...

Hi all,

I am the shepherd for proposal #273: Local Types ( https://github.com/ghc-proposals/ghc-proposals/pull/273).

This proposal would add support for local type and instance (class and type-family) definitions as a means of addressing the Configurations Problem, which as I understand it is essentially "How can we *implicitly* pass around dynamically determined values in a safe manner?" The `reflection` package provides an answer to this question with its `Reifies` class, but the implementation relies on `unsafeCoerce` and the implementation details of how GHC represents single-method class dictionaries. The proposal argues that we could safely implement the `reflection` package with local types and instances, if only Haskell had such things! As a motivation I find this pretty compelling.

The proposal introduces a few restrictions on local types and instances, and functions that contain them, primarily as a means of providing a no-escape property: local types must not be able to escape their defining scope. There are a couple ways this could happen. (1) The defining function could return a value of some local type. This is prohibited unless the value is wrapped in an existential, as otherwise the function simply could not be typed. (2) More interestingly, a type class with a functional dependency or a type family could leak the local type to the outer scope. Consider the following:

``` type family F x

foo x = x where data T type instance F Int = T

bar :: F Int bar = ??? ```

What type should `bar` have? The proposal says that all instances are still global, which would mean `bar :: T`, which is absurd. To avoid cases like this, the proposal introduces a restriction on local instances that says local types may not be determined by types from an outer scope (either via fundeps or type families). I believe these two restrictions are sufficient to guarantee the no-escape property.

I think the key question that is left unanswered by the proposal is how exactly we might implement local types in GHC. The proposal (as a guideline, not necessarily an implementation strategy) to think of local types as global types that are implicitly indexed by the type and value parameters of its defining function. But GHC does not yet have dependent types, so this is not a workable implementation strategy. Another possible strategy would be to add type/instance definitions to Core, but as Simon PJ points out this would be a tremendous amount of work, so also not a practical direction for the short-term. Lastly, Arnaud suggests that we treat local types like global types that are only defined in the local scope, i.e. let the renamer deal with them entirely. Local instances are different as they must capture locally-bound variables, but there's nothing conceptually difficult about constructing new instances dynamically (this is what ImplicitParams does). There are some remaining questions around how to ensure the optimizer doesn't incorrectly swap two instances for a local type, but these seem tractable.

I think Arnaud's suggestion is a promising and feasible strategy for implementing this proposal without new research, so my recommendation is that we return the proposal for revision and recommend the author incorporate Arnaud's suggestions.

As usual, please provide technical feedback on the PR, and feedback on my recommendation here on the mailing list.

Eric

On Mon, Nov 4, 2019, at 03:21, Joachim Breitner wrote:

...
Dear Committee,

this is your secretary speaking:

Local Types has been updated by David Feuer https://github.com/ghc-proposals/ghc-proposals/pull/273

https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc...

...
I propose Eric as the shepherd.

Please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you.

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Attachments: * signature.asc

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Richard Eisenberg

5:38 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

I have posted on the ticket. The proposal text as it now stands does not support the idea of "just in the renamer", and I find the motivation lacking. Do we need all this power just to write `reflection`? Seems like overkill. Yes, I agree that local types would often be nice. But would that nicety be covered by local modules (either proposal)? Richard

...

On Nov 25, 2019, at 8:15 AM, Simon Marlow wrote:

Having written a little C++ recently (yeah I know) where you can have local type definitions, it feels entirely natural and I started to notice the lack of them in Haskell. So I support the proposal.

My intuition is that we ought to be able to treat local types in the same way as local variables: they are entities with scoping rules enforced by the renamer. That is, a local type would be an ordinary TyCon with a Name and so forth. Having only read your email and not the proposal, that sounds the same as Arnuad's suggestion.

Cheers Simon

On Sat, 23 Nov 2019 at 16:32, Eric Seidel mailto:eric@seidel.io> wrote: Hi all,

I am the shepherd for proposal #273: Local Types (https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/ghc-proposals/ghc-proposals/pull/273).

This proposal would add support for local type and instance (class and type-family) definitions as a means of addressing the Configurations Problem, which as I understand it is essentially "How can we *implicitly* pass around dynamically determined values in a safe manner?" The `reflection` package provides an answer to this question with its `Reifies` class, but the implementation relies on `unsafeCoerce` and the implementation details of how GHC represents single-method class dictionaries. The proposal argues that we could safely implement the `reflection` package with local types and instances, if only Haskell had such things! As a motivation I find this pretty compelling.

The proposal introduces a few restrictions on local types and instances, and functions that contain them, primarily as a means of providing a no-escape property: local types must not be able to escape their defining scope. There are a couple ways this could happen. (1) The defining function could return a value of some local type. This is prohibited unless the value is wrapped in an existential, as otherwise the function simply could not be typed. (2) More interestingly, a type class with a functional dependency or a type family could leak the local type to the outer scope. Consider the following:

``` type family F x

foo x = x where data T type instance F Int = T

bar :: F Int bar = ??? ```

What type should `bar` have? The proposal says that all instances are still global, which would mean `bar :: T`, which is absurd. To avoid cases like this, the proposal introduces a restriction on local instances that says local types may not be determined by types from an outer scope (either via fundeps or type families). I believe these two restrictions are sufficient to guarantee the no-escape property.

I think the key question that is left unanswered by the proposal is how exactly we might implement local types in GHC. The proposal (as a guideline, not necessarily an implementation strategy) to think of local types as global types that are implicitly indexed by the type and value parameters of its defining function. But GHC does not yet have dependent types, so this is not a workable implementation strategy. Another possible strategy would be to add type/instance definitions to Core, but as Simon PJ points out this would be a tremendous amount of work, so also not a practical direction for the short-term. Lastly, Arnaud suggests that we treat local types like global types that are only defined in the local scope, i.e. let the renamer deal with them entirely. Local instances are different as they must capture locally-bound variables, but there's nothing conceptually difficult about constructing new instances dynamically (this is what ImplicitParams does). There are some remaining questions around how to ensure the optimizer doesn't incorrectly swap two instances for a local type, but these seem tractable.

I think Arnaud's suggestion is a promising and feasible strategy for implementing this proposal without new research, so my recommendation is that we return the proposal for revision and recommend the author incorporate Arnaud's suggestions.

As usual, please provide technical feedback on the PR, and feedback on my recommendation here on the mailing list.

Eric

On Mon, Nov 4, 2019, at 03:21, Joachim Breitner wrote:

...
Dear Committee,

this is your secretary speaking:

Local Types has been updated by David Feuer https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/ghc-proposals/ghc-proposals/pull/273 https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc... https://github.com/treeowl/ghc-proposals/blob/local-types/proposals/0000-loc...

I propose Eric as the shepherd.

Please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you.

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Attachments: * signature.asc

ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Eric Seidel

8:44 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

On Mon, Nov 25, 2019, at 05:38, Richard Eisenberg wrote:

...

I have posted on the ticket. The proposal text as it now stands does not support the idea of "just in the renamer", and I find the motivation lacking. Do we need all this power just to write `reflection`? Seems like overkill.

Yes, I agree that local types would often be nice. But would that nicety be covered by local modules (either proposal)?

The motivating example here seems like it would require parameterized modules, ie something akin to ML functors. Neither local module proposal currently includes parameterized modules.

Richard Eisenberg

noon

New subject: Proposal #273: Local Types, Recommendation: needs revision

I mis-summarized my GitHub comment. I agree that the local modules proposals do not cover `reflection` and brought up a strawman counterproposal just to support `reflection` (and similar usages of classes); the local modules proposals cover the rest of the "would be nice" aspect of local types, in my opinion. Richard

...

On Nov 25, 2019, at 1:44 PM, Eric Seidel wrote:

On Mon, Nov 25, 2019, at 05:38, Richard Eisenberg wrote:

...
I have posted on the ticket. The proposal text as it now stands does not support the idea of "just in the renamer", and I find the motivation lacking. Do we need all this power just to write `reflection`? Seems like overkill.

Yes, I agree that local types would often be nice. But would that nicety be covered by local modules (either proposal)?

The motivating example here seems like it would require parameterized modules, ie something akin to ML functors. Neither local module proposal currently includes parameterized modules. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Sandy Maguire

26 Nov 26 Nov

12:46 a.m.

New subject: Proposal #273: Local Types, Recommendation: needs revision

I'm not particularly convinced by the motivation here, and lean towards a weak "no." On Tue, Nov 26, 2019 at 12:00 AM Richard Eisenberg wrote:

...

I mis-summarized my GitHub comment. I agree that the local modules proposals do not cover `reflection` and brought up a strawman counterproposal just to support `reflection` (and similar usages of classes); the local modules proposals cover the rest of the "would be nice" aspect of local types, in my opinion.

Richard

...
On Nov 25, 2019, at 1:44 PM, Eric Seidel wrote:

On Mon, Nov 25, 2019, at 05:38, Richard Eisenberg wrote:

...
I have posted on the ticket. The proposal text as it now stands does not support the idea of "just in the renamer", and I find the motivation lacking. Do we need all this power just to write `reflection`? Seems like overkill.

Yes, I agree that local types would often be nice. But would that nicety be covered by local modules (either proposal)?

The motivating example here seems like it would require parameterized modules, ie something akin to ML functors. Neither local module proposal currently includes parameterized modules. _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- I'm currently travelling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! https://isovector.github.io/erdos/

2002

Age (days ago)

2024

Last active (days ago)

List overview

Download

7 comments

5 participants

participants (5)

Eric Seidel
Joachim Breitner
Richard Eisenberg
Sandy Maguire
Simon Marlow