Hi, Am Freitag, den 23.02.2018, 15:52 +0000 schrieb Simon Peyton Jones:

Why do we need this now? There's lots of new syntax. Is it solving tomorrow's problems, or todays?

Does the proposal subsume #81 (syntax for visible dependent quantification)? That one /does/ have a current motivation.

Perhaps #102 is just a grander version of #81, reserving the syntax but with #81 as the sole current motivation?

when #81 was proposed, Roman (as the shepherd) complained that on its own, the choice of syntax in #81 was not very well motivated just by that proposal. Maybe, if #81 was all there is to do, we’d choose a different syntax! So really, the syntax in #81 is motivated by coming up with a consistent and comprehensive syntax scheme for _all_ variations of the quantifier, and Roman asked Richard to write that up as one proposal, instead of introducing the syntax piece by piece. And that’s now #102. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I'm on a train, and don't have access to the proposals, but here's are some thoughts: * #54 is about letting users write kind signatures for type constructors, just as they can write type signatures for term variables. It's amazing we have lasted so long without this ability, but it's really really hurting us. I feel strongly that we should fix this: we need SOME way to write a kind signature for a type constructor. * To write such a kind signature we need something like the T :: forall a b -> blah syntax, to indicate which of T's arguments should be written positionally (like the Int in Proxy Int) and which are hidden (like the * in Proxy Int). By hook or by crook we must be able to express this. And that's #81. * The worry with #81 was whether it would be painting us into a corner. Hence #102. But I regard #102 as an existence proof that the corner has an exit, not as something we should espouse now. (Tell me if you disagree Richard.) It is far off our radar, and premature to make a commitment. Richard: you could add the analysis in your email about "why 12" to the proposal. So I suggest that we accept #54 and #81, and simply punt on #102. Simon | -----Original Message----- | From: ghc-steering-committee On Behalf Of Richard Eisenberg | Sent: 27 March 2018 04:36 | To: Iavor Diatchki | Cc: ghc-steering-committee@haskell.org; Joachim Breitner | Subject: Re: [ghc-steering-committee] DH quantifiers (#102), | Recommendation: accept | | I'd like to restart this thread, both as the Grand Poobah of Dependent | Haskell and because Proposal #102 (this one) is holding up #81 (the | `forall x y z ->` syntax), which is, in turn, holding up #54 (a plan to | eliminate the need for CUSKs), which is implicated in quite a few bugs. | | I think Iavor makes some good criticisms below, which I'll address | individually: | | > On Feb 23, 2018, at 12:12 PM, Iavor Diatchki | wrote: | > | > * it is premature to "reserve" syntax for a future extension | | This is a hard one. The full implementation of dependent types in | Haskell is still years away. But decisions we make now may affect the | eventual concrete syntax. While a ghc-proposal is ill-fitted with | reserving syntax, I think Roman was right to request that #81 be | considered in the context of the larger syntactic changes. Maybe the | "right" answer here is for the committee to conclude that the proposed | syntax is generally plausible, paving the way for #81 but without making | a solid commitment. On the other hand, if we can identify a better | syntax for the overall design of dependent types in Haskell, that might | affect the syntax used in #81/#54. | | > * I am not convinced that a design with 12 quantifiers is what I'd | want to use | | Neither am I! | | For a moment, let's take the desire for dependent types to be a given. | (I'll address this more below.) GHC currently has 3 quantifiers (`forall | a.`, `ty ->`, and `ty =>`). To preserve type erasure, we need to | distinguish between arguments needed at runtime and those that can be | erased. | | Coq does this through its Set-vs-Prop mechanism, where erased arguments | live in their own sort. Such a route is viable for Haskell, I think, but | I've never been much enamored of it, personally. For example, the Nat in | a vector type really can be erased, while Nats in many other places | can't be, and it seems a shame to need two different Nat types to pull | off this dichotomy. | | Agda uses the term "irrelevant" to describe type indices that are | ignored during type equality checks. This is related to the type erasure | property, but it's not quite the same thing. It's unclear to me what | types Agda can erase, and I don't think Agda gives any solid guarantees | as to erasure. (As a language aiming for performance, Haskell needs to | provide such a guarantee.) | | Idris does whole-program analysis to determine erasability. I can't | imagine this scales well. | | The choice I've made in the design of Dependent Haskell is to have the | user choose whether to keep an argument or not, leading to the | forall/foreach distinction. This brings us from 3 quantifiers to 4. In | truth, 4 is enough to power dependent types! But read on. | | All dependently typed languages give a facility for the user to control | the visibility of arguments. If we want to do the same, we go from 4 | quantifiers to 6. (We don't go to 8 because the original -> and => | already differ in visibility.) Note, though, that Coq doesn't consider | visibility as a feature of a type, instead using, essentially, pragmas | to control visibility. This has some benefits (higher-order usages of | functions can't fall over based on visibility), but it doesn't seem | well-suited for Haskell. | | Quite separately, we also will likely want to allow currying in type- | level operations. Partially-applied type families are currently | forbidden because doing so would wreak havoc with type inference. | (Imagine if we're unifying `m a` with `Maybe Int` but that `m` might | unify with a type family `Id`!) The solution I've proposed here is a | notion of *matchability*, described in Section 4.2.4 of my thesis (which | can be read independently of the rest of it). A function is *matchable* | iff it is generative and injective -- in other words, if equalities over | function applications can be decomposed. When some functions (like Maybe | and Either Int) are matchable and some (like Id and any other type | family) are not, then type inference can decompose matchable things and | not decompose unmatchable things. It turns out that all previous 6 | quantifiers are useful in both the matchable and unmatchable varieties, | bringing us to 12. | | Note that other dependently typed languages don't have a notion of | matchability. They generally also don't have injective type constructors | (you can't derive (a ~ b) from (Maybe a ~ Maybe b)) and don't have the | guess-free type inference Haskell has. Instead, those languages | generally rely on higher-order unification, which is a best-guess | algorithm (as I understand it). GHC has stayed away from guessing. We | might imagine a future for GHC that allows partially-applied type | functions without using matchability, but I conjecture that any such | future would also have to offer weaker guarantees for the predictability | and stability of type inference. It might be a fruitful debate to see | which is better -- stable type inference or fewer quantifiers. | | My bottom line: I don't like the 12 quantifiers either. And dependent | types require really only 1 new one. Two more come along for the | convenience of invisible arguments. And then we have to double for | matchability. (Note that matchability can be considered quite | orthogonally to dependent types -- it has even been proposed separately | in #52.) Perhaps I've overshot in the design here and some healthy | debate here can whittle the number down. | | > * I am not convinced about the utility of the "dependent haskell" | extension in the first place. | | This is the bigger question. Chapter 3 of my thesis lays out some | motivation for dependent types, as does Chapter 8 of Adam Gundry's. | Historically, every feature (fundeps, type families, GADTs, kind | polymorphism, higher-rank types, type applications) that has moved GHC | closer to having dependent types has been eagerly adopted. I've heard | some push-back over the years about this, but the biggest complaint I've | gotten is around termination: people don't want GHC to reject non- | terminating functions. When I explain that doing so has never been part | of the plan, then generally the objection is retracted. | | What are the downsides of adding dependent types? | | - The language becomes more complicated. Haskell already has a | reputation of being impossible to learn, and if dependent types appear | everywhere, this reputation will be reinforced, to the language's | detriment. I am indeed worried about this. Care will have to be taken by | library authors to make dependent types an opt-in experience. | | - Error messages might worsen. I'm actually not terribly worried about | this, as I believe clever engineering can avoid it. Other than #11198 | (which is now fixed), there has not been a degradation in error messages | from -XTypeInType. Errors still use the words "kind" and "type" to mean | different things! Even forgetting about dependent types, I think GHC's | error messages need an overhaul, basically to become more like Idris's. | (That is, interactive.) Especially if we have interactivity in error | messages, then there are even more ways to mitigate the potential | trouble of dependent types. Note that Haskell's tradition of language | extensions help us here: if a user makes a type error in simple code -- | but that code might have a meaning in a dependently typed setting -- | then we can use the presence or absence of language extensions to tailor | the message. (In particular, we might want to be conservative in | recommending that the user enable -XDependentTypes.) | | - The abstraction will sometimes leak. The most glaring example of this | is when the type of ($) started muttering about levity polymorphism. | That was terrible! I do think that, with care, we can avoid this, by | continuing to use compiler flags to tailor output and/or adding | interactivity to GHC's output. | | - The implementation becomes more complicated. Well, yes, though perhaps | we'll lose some duplication once GHC no longer has separate Expr and | Type types. | | ----------------------------------------- | | What to do next? If others on the committee are worried about the | desire/utility of dependent types, it might be good to seek input from | the community. Beyond that, I'll reiterate 4 possible actions we might | take on #102, specifically: | | 1. Reject the syntax. If we do this, I'd love to open a larger | conversation of ways forward -- do we want tweaks to the syntax or a | wholly new approach? | | 2. Put this idea on hold, with a plan to accept or reject #81 on its own | merits. | | 3. Accept the proposal, but put implementation on the back burner. This | would serve to reserve the syntax, without burdening our users until the | features are more fully-formed. | | 4. Accept the proposal and plan to implement. | | Looking forward to seeing your thoughts on this, | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Mittwoch, den 28.03.2018, 13:10 -0400 schrieb Richard Eisenberg:

Agreed with all points Simon makes below -- including on punting on #102 with a personal hope to return some day not too distant from now. I'll update the proposal with my analysis from the email.

did you do this update? If so, you can change the label of the proposal to “Needs revision” or “dormant” or something similar. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I said three weeks ago: | So I suggest that we accept #54 and #81, and simply punt on #102. Richard agreed to punt on #102. Are we agreed to accept these two? * #54 https://github.com/ghc-proposals/ghc-proposals/pull/54 * #81 https://github.com/ghc-proposals/ghc-proposals/pull/81 RSVP. I'd really like to unglue this log-jam! Simon PS: Richard hasn't yet formally submitted #54, but will do so later today | -----Original Message----- | From: ghc-steering-committee On Behalf Of Simon Peyton Jones | Sent: 27 March 2018 23:11 | To: Richard Eisenberg ; Iavor Diatchki | | Cc: ghc-steering-committee@haskell.org; Joachim Breitner | | Subject: Re: [ghc-steering-committee] DH quantifiers (#102), | Recommendation: accept | | I'm on a train, and don't have access to the proposals, but here's are | some thoughts: | | * #54 is about letting users write kind signatures for type | constructors, | just as they can write type signatures for term variables. It's | amazing we have lasted so long without this ability, but it's really | really hurting us. I feel strongly that we should fix this: we | need | SOME way to write a kind signature for a type constructor. | | * To write such a kind signature we need something like the | T :: forall a b -> blah syntax, to indicate which of T's | arguments should be written positionally (like the Int in Proxy Int) | and which are hidden (like the * in Proxy Int). By hook or by | crook we must be able to express this. And that's #81. | | * The worry with #81 was whether it would be painting us into a | corner. Hence #102. But I regard #102 as an existence proof that | the corner has an exit, not as something we should espouse now. | (Tell me if you disagree Richard.) It is far off our radar, and | premature to make a commitment. | | Richard: you could add the analysis in your email about "why 12" | to the proposal. | | So I suggest that we accept #54 and #81, and simply punt on #102. | | Simon | | | -----Original Message----- | | From: ghc-steering-committee On Behalf Of Richard Eisenberg | | Sent: 27 March 2018 04:36 | | To: Iavor Diatchki | | Cc: ghc-steering-committee@haskell.org; Joachim Breitner | | | | Subject: Re: [ghc-steering-committee] DH quantifiers (#102), | | Recommendation: accept | | | | I'd like to restart this thread, both as the Grand Poobah of | Dependent | | Haskell and because Proposal #102 (this one) is holding up #81 (the | | `forall x y z ->` syntax), which is, in turn, holding up #54 (a plan | | to eliminate the need for CUSKs), which is implicated in quite a few | bugs. | | | | I think Iavor makes some good criticisms below, which I'll address | | individually: | | | | > On Feb 23, 2018, at 12:12 PM, Iavor Diatchki | | wrote: | | > | | > * it is premature to "reserve" syntax for a future extension | | | | This is a hard one. The full implementation of dependent types in | | Haskell is still years away. But decisions we make now may affect | the | | eventual concrete syntax. While a ghc-proposal is ill-fitted with | | reserving syntax, I think Roman was right to request that #81 be | | considered in the context of the larger syntactic changes. Maybe the | | "right" answer here is for the committee to conclude that the | proposed | | syntax is generally plausible, paving the way for #81 but without | | making a solid commitment. On the other hand, if we can identify a | | better syntax for the overall design of dependent types in Haskell, | | that might affect the syntax used in #81/#54. | | | | > * I am not convinced that a design with 12 quantifiers is what | | > I'd | | want to use | | | | Neither am I! | | | | For a moment, let's take the desire for dependent types to be a | given. | | (I'll address this more below.) GHC currently has 3 quantifiers | | (`forall a.`, `ty ->`, and `ty =>`). To preserve type erasure, we | need | | to distinguish between arguments needed at runtime and those that | can | | be erased. | | | | Coq does this through its Set-vs-Prop mechanism, where erased | | arguments live in their own sort. Such a route is viable for | Haskell, | | I think, but I've never been much enamored of it, personally. For | | example, the Nat in a vector type really can be erased, while Nats | in | | many other places can't be, and it seems a shame to need two | different | | Nat types to pull off this dichotomy. | | | | Agda uses the term "irrelevant" to describe type indices that are | | ignored during type equality checks. This is related to the type | | erasure property, but it's not quite the same thing. It's unclear to | | me what types Agda can erase, and I don't think Agda gives any solid | | guarantees as to erasure. (As a language aiming for performance, | | Haskell needs to provide such a guarantee.) | | | | Idris does whole-program analysis to determine erasability. I can't | | imagine this scales well. | | | | The choice I've made in the design of Dependent Haskell is to have | the | | user choose whether to keep an argument or not, leading to the | | forall/foreach distinction. This brings us from 3 quantifiers to 4. | In | | truth, 4 is enough to power dependent types! But read on. | | | | All dependently typed languages give a facility for the user to | | control the visibility of arguments. If we want to do the same, we | go | | from 4 quantifiers to 6. (We don't go to 8 because the original -> | and | | => already differ in visibility.) Note, though, that Coq doesn't | | consider visibility as a feature of a type, instead using, | | essentially, pragmas to control visibility. This has some benefits | | (higher-order usages of functions can't fall over based on | | visibility), but it doesn't seem well-suited for Haskell. | | | | Quite separately, we also will likely want to allow currying in | type- | | level operations. Partially-applied type families are currently | | forbidden because doing so would wreak havoc with type inference. | | (Imagine if we're unifying `m a` with `Maybe Int` but that `m` might | | unify with a type family `Id`!) The solution I've proposed here is a | | notion of *matchability*, described in Section 4.2.4 of my thesis | | (which can be read independently of the rest of it). A function is | | *matchable* iff it is generative and injective -- in other words, if | | equalities over function applications can be decomposed. When some | | functions (like Maybe and Either Int) are matchable and some (like | Id | | and any other type | | family) are not, then type inference can decompose matchable things | | and not decompose unmatchable things. It turns out that all previous | 6 | | quantifiers are useful in both the matchable and unmatchable | | varieties, bringing us to 12. | | | | Note that other dependently typed languages don't have a notion of | | matchability. They generally also don't have injective type | | constructors (you can't derive (a ~ b) from (Maybe a ~ Maybe b)) and | | don't have the guess-free type inference Haskell has. Instead, those | | languages generally rely on higher-order unification, which is a | | best-guess algorithm (as I understand it). GHC has stayed away from | | guessing. We might imagine a future for GHC that allows | | partially-applied type functions without using matchability, but I | | conjecture that any such future would also have to offer weaker | | guarantees for the predictability and stability of type inference. | It | | might be a fruitful debate to see which is better -- stable type | inference or fewer quantifiers. | | | | My bottom line: I don't like the 12 quantifiers either. And | dependent | | types require really only 1 new one. Two more come along for the | | convenience of invisible arguments. And then we have to double for | | matchability. (Note that matchability can be considered quite | | orthogonally to dependent types -- it has even been proposed | | separately in #52.) Perhaps I've overshot in the design here and | some | | healthy debate here can whittle the number down. | | | | > * I am not convinced about the utility of the "dependent | haskell" | | extension in the first place. | | | | This is the bigger question. Chapter 3 of my thesis lays out some | | motivation for dependent types, as does Chapter 8 of Adam Gundry's. | | Historically, every feature (fundeps, type families, GADTs, kind | | polymorphism, higher-rank types, type applications) that has moved | GHC | | closer to having dependent types has been eagerly adopted. I've | heard | | some push-back over the years about this, but the biggest complaint | | I've gotten is around termination: people don't want GHC to reject | | non- terminating functions. When I explain that doing so has never | | been part of the plan, then generally the objection is retracted. | | | | What are the downsides of adding dependent types? | | | | - The language becomes more complicated. Haskell already has a | | reputation of being impossible to learn, and if dependent types | appear | | everywhere, this reputation will be reinforced, to the language's | | detriment. I am indeed worried about this. Care will have to be | taken | | by library authors to make dependent types an opt-in experience. | | | | - Error messages might worsen. I'm actually not terribly worried | about | | this, as I believe clever engineering can avoid it. Other than | #11198 | | (which is now fixed), there has not been a degradation in error | | messages from -XTypeInType. Errors still use the words "kind" and | | "type" to mean different things! Even forgetting about dependent | | types, I think GHC's error messages need an overhaul, basically to | become more like Idris's. | | (That is, interactive.) Especially if we have interactivity in error | | messages, then there are even more ways to mitigate the potential | | trouble of dependent types. Note that Haskell's tradition of | language | | extensions help us here: if a user makes a type error in simple code | | -- but that code might have a meaning in a dependently typed setting | | -- then we can use the presence or absence of language extensions to | | tailor the message. (In particular, we might want to be conservative | | in recommending that the user enable -XDependentTypes.) | | | | - The abstraction will sometimes leak. The most glaring example of | | this is when the type of ($) started muttering about levity | polymorphism. | | That was terrible! I do think that, with care, we can avoid this, by | | continuing to use compiler flags to tailor output and/or adding | | interactivity to GHC's output. | | | | - The implementation becomes more complicated. Well, yes, though | | perhaps we'll lose some duplication once GHC no longer has separate | | Expr and Type types. | | | | ----------------------------------------- | | | | What to do next? If others on the committee are worried about the | | desire/utility of dependent types, it might be good to seek input | from | | the community. Beyond that, I'll reiterate 4 possible actions we | might | | take on #102, specifically: | | | | 1. Reject the syntax. If we do this, I'd love to open a larger | | conversation of ways forward -- do we want tweaks to the syntax or a | | wholly new approach? | | | | 2. Put this idea on hold, with a plan to accept or reject #81 on its | | own merits. | | | | 3. Accept the proposal, but put implementation on the back burner. | | This would serve to reserve the syntax, without burdening our users | | until the features are more fully-formed. | | | | 4. Accept the proposal and plan to implement. | | | | Looking forward to seeing your thoughts on this, Richard | | _______________________________________________ | | ghc-steering-committee mailing list | | ghc-steering-committee@haskell.org | | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | committ | | ee | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering- | committee