Quantified Constraints (#109). Recommendation: accept

The proposal for quantified constraints, #109, has been submitted for a decision. This proposal generalizes the syntax for constraints to include forall-quantification and premise constraints. For example:
data Rose f a = Branch a (f (Rose f a))
instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where Branch x1 c1 == Branch x2 c2 = x1 == x2 && c1 == c2
Note the `forall b. Eq b =>` in the constraint for this instance, which is necessary in order for the instance to be obviously terminating. There are *many* other motivations for this feature, dating back over a decade. Particularly pressing might be the fact that this feature will allow us to put `join` in the Monad type class, currently impossible due to the way roles work. See https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-u... for the details (which are not necessary in order to evaluate this proposal -- merely good motivation). The proposal introduces -XQuantfiedConstraints, which will enable the new feature, though -XExplicitForAll will also be necessary if you wish to write a `forall` explicitly (as you likely will). There are some subtleties of the typing rules, but it all basically behaves as you would expect. Quantified constraints may induce a situation where GHC must choose one of two potential routes toward proving a goal; when this happens, the program is rejected (even if one or more of the routes would have been successful). Note that quantified constraints cannot introduce incoherence, as they do not create new instances. Simon has already implemented this feature on a branch, and as I understand it, it's working swimmingly. Recommendation: accept. This feature has been wanted for a long time, is a natural extension of features GHC already has (roles, higher-rank types), and has been implemented cleanly. As usual, I will take silence as agreement. I look forward to reading your comments. Thanks, Richard

Hi, incidentially, just last week I had this interaction: me: “I’d like feature X” icelandjack: “Quantified Constraints can do that” me: “Yay!” https://ghc.haskell.org/trac/ghc/ticket/15008 Hence in favor, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

+1
Am 10.04.2018 um 02:39 schrieb Richard Eisenberg
: The proposal for quantified constraints, #109, has been submitted for a decision.
This proposal generalizes the syntax for constraints to include forall-quantification and premise constraints. For example:
data Rose f a = Branch a (f (Rose f a))
instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where Branch x1 c1 == Branch x2 c2 = x1 == x2 && c1 == c2
Note the `forall b. Eq b =>` in the constraint for this instance, which is necessary in order for the instance to be obviously terminating. There are *many* other motivations for this feature, dating back over a decade. Particularly pressing might be the fact that this feature will allow us to put `join` in the Monad type class, currently impossible due to the way roles work. See https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-u... for the details (which are not necessary in order to evaluate this proposal -- merely good motivation).
The proposal introduces -XQuantfiedConstraints, which will enable the new feature, though -XExplicitForAll will also be necessary if you wish to write a `forall` explicitly (as you likely will). There are some subtleties of the typing rules, but it all basically behaves as you would expect. Quantified constraints may induce a situation where GHC must choose one of two potential routes toward proving a goal; when this happens, the program is rejected (even if one or more of the routes would have been successful). Note that quantified constraints cannot introduce incoherence, as they do not create new instances.
Simon has already implemented this feature on a branch, and as I understand it, it's working swimmingly.
Recommendation: accept.
This feature has been wanted for a long time, is a natural extension of features GHC already has (roles, higher-rank types), and has been implemented cleanly.
As usual, I will take silence as agreement. I look forward to reading your comments.
Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Montag, den 09.04.2018, 12:39 -0400 schrieb Richard Eisenberg:
As usual, I will take silence as agreement. I look forward to reading your comments.
we have to disappoint you; no comments. But two +1 and otherwise silent agreement. I conclude that we have reached positive consensus. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/
participants (3)
-
Joachim Breitner
-
Manuel M T Chakravarty
-
Richard Eisenberg