Opened 11 years ago
Closed 16 months ago
#2893 closed feature request (fixed)
Implement "Quantified constraints" proposal
Reported by: | porges | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 6.10.1 |
Keywords: | QuantifiedConstraints, GHCProposal | Cc: | id@…, reiner.pope@…, illissius@…, sjoerd@…, shane@…, ggreif@…, maoe, RyanGlScott, Iceland_jack, baramoglo |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | quantified-constraints/T2893{,a,c} |
Blocked By: | Blocking: | ||
Related Tickets: | #5927 | Differential Rev(s): | Phab:D4724 |
Wiki Page: |
Description (last modified by )
Change History (41)
comment:1 Changed 11 years ago by
Cc: | id@… added |
---|
comment:2 Changed 11 years ago by
Well here's an example: today I was trying to write an instance of Applicative for things that are Monoids and Foldable (started by generalizing from [a]):
This is currently not possible because Applicative & Foldable are both (* -> *) and Monoids are (*). As far as I can tell, the proposal would allow something like this:
instance (Foldable l, forall a. Monoid (l a)) => Applicative l where fs <*> xs = foldMap (<$> xs) fs
I may be horribly wrong, however :)
(Also I can't implement pure :P)
comment:3 Changed 11 years ago by
difficulty: | → Unknown |
---|---|
Milestone: | → _|_ |
I had trouble following the proposal. I didn't see how Section 3 addressed the issues raised in Sections 1 and 2. For example, to avoid the cascade of Typeable2
, Typeable3
etc classes the solution is presumably polymorphism at the kind level. (Tim Sheard's language Omega has this.)
Still, I recognise the merit of quantification in contexts. Indeed, Ralf Hinze and I suggested it back in 2000 in Section 7 of Derivable type classes. (This section is rather independent of the rest of the paper.)
However, attractive as it is, it's quite a big step to add something akin to local instance declarations. Our ICFP'08 paper Type checking with open type functions relies rather crucially on not having such local instances. (We've managed to simplify the algorithm quite a bit since then, but it still relies on that assumption.)
So I'm not sure I see how to make quantified contexts compatible with type functions, and all the other stuff in Haskell. But their lack is clearly a wart, and one that may become more pressing.
Meanwhile, clarifying the proposal would be a good thing, even if it's not adopted right away.
Simon
comment:4 Changed 10 years ago by
A short version... we allow contexts of the form:
(forall a. Bar f a) => Foo f
And more generally, these contexts can have contexts of their own:
(forall a. (Baz a) => Bar f a) => Foo f
I'm not sure if the 'more general' version adds extra difficulty in type-checking, as I am not very familiar with its intricacies.
Forgive my stupidity, I don't understand where the typechecking (at least in the first) becomes so difficult—the context means that there is an instance available which is free in the specified variable.
comment:5 Changed 9 years ago by
Type of failure: | → None/Unknown |
---|
This blog post provides an excellent motivating example for this feature.
comment:6 Changed 9 years ago by
Cc: | reiner.pope@… added |
---|
comment:7 Changed 8 years ago by
Cc: | illissius@… added |
---|
comment:8 Changed 8 years ago by
As the blog post points out (and I recently rediscovered) GHC already supports this feature in a more elaborate form. This works:
{-# LANGUAGE GADTs, Rank2Types, FlexibleContexts #-} class Foo a where foo :: a -> String instance Foo [b] where foo = show . length data FooDict a where FooDict :: Foo a => FooDict a f :: (forall b. FooDict [b]) -> String f FooDict = foo "Hello" ++ foo [1, 2, 3] use_foo :: String use_foo = f FooDict
But this is rejected:
g :: (forall b. Foo [b]) => String g = foo "Hello" ++ foo [1, 2, 3] use_foo' :: String use_foo' = g
So there doesn't seem to be a fundamental difficulty here.
comment:9 Changed 7 years ago by
Cc: | sjoerd@… added |
---|
I don't see why this needs "local instances". The instances are not the problem, we can already do polymorphic instances, i.e. instance Monoid [a]. Even specifying the forall constraint now (accidentally) works in GHC 7.4.1.
As I see it, the problem is with matching the need for a constraint with the available constraints or instances. See #7019, the error is "Could not deduce (Monoid [b]) from the context (forall a. Monoid [a])".
Even g from the previous comment now compiles (with ConstraintKinds and UndecidableInstances), except when evaluating it, you get the error: "Could not deduce (forall b. Foo [b]) arising from a use of `g'".
So it seems that with implementing ConstraintKinds, there has been made a big step towards an implementation of quantified contexts.
comment:10 Changed 7 years ago by
Edward Kmett created a workaround: Data.Constraint.Forall
It works like this: if you have p A and p B, for unexported A and B, then you must have forall a. p a. Then unsafeCoerce is used to coerce p A to p a.
comment:11 Changed 7 years ago by
Cc: | shane@… added |
---|
comment:12 follow-up: 24 Changed 5 years ago by
Cc: | ggreif@… added |
---|
Copying a use-case from #9196:
My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-*
kind, that is an ADT.
See:
class Foo a where ... data Bar (b :: Bool) x = ... instance Foo (Bar True x) where ... instance Foo (Bar False x) where ... test :: (forall b. Foo (Bar b x)) =>...
Here the forall
condition is satisfiable, as all Bool
alternatives are covered with instance
declarations.
comment:13 Changed 5 years ago by
The trouble is that I don't know how to do type inference in the presence of polymorphic constraints. It is not a small change.
It would be a useful feature. I've wanted it since at least 2000 (see Derivable Type Classes).
Simon
comment:14 Changed 4 years ago by
Cc: | maoe added |
---|
comment:15 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:16 Changed 3 years ago by
Cc: | Iceland_jack added |
---|
comment:17 Changed 3 years ago by
Moved from #5927.
Use case from How to Twist Pointers without Breaking Them:
class Monoid m => Action m a where act :: m -> a -> a[...]
We first formalise the action of monoids on functors. Intuitively, for a monoid
m
to act on the functorf
, it should act in a uniform way on all the typesf a
. Therefore, we would like to assert a constraint something likeforall a. Action m (f a)
. Unfortunately, Haskell does not allow the use of universally quantified constraints and hence we need a new type class.class (Monoid m, Functor f) => ActionF m f where act' :: m -> f a -> f a
comment:18 Changed 3 years ago by
This functionality does my head in so bear with me.
In the definition of Fmt, constraints of (p a, p b, p (a, b))
are assumed for :&
data Fmt :: (* -> Constraint) -> (* -> *) -> * -> * where Int :: p Int => Fmt p r Int (:&) :: (p a, p b, p (a,b)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b) Lift :: p (r a) => r a -> Fmt p r a
(p a, p b)
often implies p (a, b)
, would this be captured by QuantifiedConstraints
?
(:&) :: (p a, p b, forall xx yy. (p xx, p yy) => p (xx, yy)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b)
Does this even give us any additional power? Is this more or less powerful than the :=>
class from constraints?
class b :=> h | h -> b where ins :: b :- h instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict instance (Bounded a, Bounded b) :=> Bounded (a, b) where ins = Sub Dict instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict ...
What if we assume that GHC generates instances of :=>
?
comment:19 Changed 3 years ago by
Has there been any discussion about GHC generating instances of :=> and Class
-- Given -- class Foo a => Bar a -- GHC should generate -- instance Class (Foo a) (Bar a) where -- cls :: Bar a :- Foo a -- cls = Sub Dict class Class b h | h -> b where cls :: h :- b
or Lifting
class Lifting p f where lifting :: p a :- p (f a) class Lifting2 p f where lifting2 :: p a :- Lifting p (f a)
comment:20 follow-up: 21 Changed 3 years ago by
Iceland_jack, there are two problems with using typeclasses like these to "solve" this problem:
- They're based on explicit
Dict
values. As a result, using them requires lots of pattern matching and type variable scoping hullabaloo, which gets annoying pretty quickly. - What does it mean to automatically generate instances for
(:=>)
? Do we only generate instances that correspond to actual instance contexts? If so, then the following would typecheck, since there is aninstance () :=> Eq ()
:
ins :: () :- Eq ()
But the following would not typecheck!
ins :: Eq () :- Eq ()
Because there is no
instance Eq () => Eq ()
anywhere (and thus noinstance Eq () :=> Eq ()
), onlyinstance Eq ()
. But the implicationEq () => Eq ()
should obviously hold. Does that mean we should also generate aninstance Eq () :=> Eq ()
automatically? But what about(Eq (), Ord ()) => Eq ()
?(Eq (), Ord (), Show ()) => Eq ()
? There is an extremely high number of contexts in whichEq ()
holds, and generating every possible one of them would result in a combinatorial explosion.
While those classes are neat tricks that can get you some of the functionality of
QuantifiedConstraints
/ImplicationConstraints
, they don't go all the way. I really feel that some compiler smarts would make these features manageable.
comment:21 Changed 3 years ago by
Replying to RyanGlScott:
- What does it mean to automatically generate instances for
(:=>)
?
That is the question isn't it, I imagined it as Typeable
or Coercible
where the compiler creates instances on the fly but which instances I do not know.
While those classes are neat tricks that can get you some of the functionality of
QuantifiedConstraints
/ImplicationConstraints
, they don't go all the way.
QuantifiedConstraints
and ImplicationConstraints
would certainly be preferable! Are there any plans to research / implement such features? They would enable a lot of awesome code that is currently beyond reach.
comment:22 Changed 3 years ago by
I have no specific, concrete plans to work on implication constraints, but I have a few enterprising students who may be looking for a project next semester. Implementation implication constraints is on the shortlist of projects to consider.
comment:23 Changed 3 years ago by
I want to mention an example from 1997: Type classes: an exploration of the design space
What we really want is universal quantification:
class (forall s. Monad (m s)) => StateMonad m where get :: m s s set :: s -> m s ()
which can be defined as
class ForallF Monad m => StateMonad m where get :: m s s set :: s -> m s ()
How does it compare to MonadState
.
comment:24 Changed 2 years ago by
Replying to heisenbug:
Copying a use-case from #9196:
My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-
*
kind, that is an ADT.See:
class Foo a where ... data Bar (b :: Bool) x = ... instance Foo (Bar True x) where ... instance Foo (Bar False x) where ... test :: (forall b. Foo (Bar b x)) =>...Here the
forall
condition is satisfiable, as allBool
alternatives are covered withinstance
declarations.
Actually, the forall
condition is not satisfiable. The smaller problem is that stuck type families like Any
can inhabit Bool
without being 'True
or 'False
. The bigger problem is that Haskell's "logic" is inherently constructive. The claim that for any type b :: Bool
there exists some instance Foo b x
does not translate to a way to actually get the dictionary representing that instance. So I think your beautiful dream is, sadly, almost certainly unrealizable.
comment:25 Changed 2 years ago by
Cc: | baramoglo added |
---|
comment:26 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:27 Changed 2 years ago by
Keywords: | QuantifiedContexts added; proposal removed |
---|
comment:28 Changed 20 months ago by
I've build an implementation of QuantifiedConstraints
, held on wip/T2893
. Here's the commit message
commit dbcf8d0b9076ae32b9138623eb84f67c18ed3dab Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Sat Jan 27 14:32:34 2018 +0000 Implement QuantifiedConstraints We have wanted quantified constraints for ages and, as I hoped, they proved remarkably simple to implement. All the machinery was already in place. The main ticket is Trac #2893, but also relevant are #5927 #8516 #9123 (especially! higher kinded roles) #14070 #14317 The wiki page is https://ghc.haskell.org/trac/ghc/wiki/QuantifiedContexts Here is the relevant Note: Note [Quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The -XQuantifiedConstraints extension allows type-class contexts like this: data Rose f x = Rose x (f (Rose f x)) instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2 Note the (forall b. Eq b => Eq (f b)) in the instance contexts. This quantified constraint is needed to solve the [W] (Eq (f (Rose f x))) constraint which arises form the (==) definition. Here are the moving parts * Language extension {-# LANGUAGE QuantifiedConstraints #-} and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension * A new form of evidence, EvDFun, that is used to discharge such wanted constraints * checkValidType gets some changes to accept forall-constraints only in the right places. * Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints * TcSMonad.InertCans gets an extra field, inert_insts, which holds all the Given forall-constraints. In effect, such Given constraints are like local instance decls. * When trying to solve a class constraint, via TcInteract.matchInstEnv, use the InstEnv from inert_insts so that we include the local Given forall-constraints in the lookup. (See TcSMonad.getInstEnvs.) * TcCanonical.canForAll deals with solving a forall-constraint. See Note [Solving a Wanted forall-constraint] Note [Solving a Wanted forall-constraint] * We augment the kick-out code to kick out an inert forall constraint if it can be rewritten by a new type equality; see TcSMonad.kick_out_rewritable Still to come - User manual documentation - A GHC Proposal
I'll try to get it up on Phabricator on Monday, unless someone would care to beat me to it.
Please give it a try!
comment:29 Changed 20 months ago by
Differential Rev(s): | → Phab:D4353 |
---|
You can review the code at Phab:D4353
comment:30 Changed 20 months ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
comment:31 Changed 20 months ago by
Description: | modified (diff) |
---|---|
Summary: | Implement "Quantified contexts" proposal → Implement "Quantified constraints" proposal |
comment:32 Changed 20 months ago by
Description: | modified (diff) |
---|
comment:33 Changed 19 months ago by
Related Tickets: | → #5927 |
---|
comment:34 Changed 19 months ago by
I've added the superclass stuff
commit 910dfcfeadc4f132e887bc4adf5ac2e17a29d99b Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Thu Mar 1 23:32:29 2018 +0000 Add superclasses to quantified constraints This patch adds suppport for superclasses to quantified constraints. For example (contrived): f :: (forall a. Ord a => Ord (m a)) => m a -> m a -> Bool f x y = x==y Here we need (Eq (m a)); but the quantifed constraint deals only with Ord. But we can make it work by using its superclass. This behaviour finally delivers on the promise of comment:30 of Trac #9123: we can write an implication constraint that solves the problem of higher-kinded roles. Test quantified-constraints/T8123 demonstrates this in action. compiler/basicTypes/Id.hs | 2 +- compiler/typecheck/Inst.hs | 4 +- compiler/typecheck/TcCanonical.hs | 180 ++++++++++++++--------- compiler/typecheck/TcErrors.hs | 4 +- compiler/typecheck/TcEvTerm.hs | 5 +- compiler/typecheck/TcEvidence.hs | 74 ++++++---- compiler/typecheck/TcHsSyn.hs | 23 ++- compiler/typecheck/TcInstDcls.hs | 2 +- compiler/typecheck/TcInteract.hs | 61 ++++---- compiler/typecheck/TcMType.hs | 6 +- compiler/typecheck/TcPatSyn.hs | 7 +- compiler/typecheck/TcPluginM.hs | 2 +- compiler/typecheck/TcRnTypes.hs | 62 ++++++-- compiler/typecheck/TcSMonad.hs | 119 +++++++-------- compiler/typecheck/TcSimplify.hs | 2 +- compiler/typecheck/TcType.hs | 2 +- compiler/types/Class.hs | 54 ++++--- compiler/types/Kind.hs | 2 + testsuite/tests/quantified-constraints/T2893b.hs | 24 --- testsuite/tests/quantified-constraints/T2893c.hs | 15 ++ testsuite/tests/quantified-constraints/T9123.hs | 24 +++ testsuite/tests/quantified-constraints/T9123a.hs | 26 ++++ testsuite/tests/quantified-constraints/all.T | 5 + 23 files changed, 426 insertions(+), 279 deletions(-)
So now all the features I was planning are implemented.
Give it a whirl!
comment:35 Changed 19 months ago by
... superclass stufff ... Give it a whirl!
Terrific. I'd appreciate if someone could test my hypothesis of a use case [1]. Note this using QuantifiedConstraints purely as implications with nothing forall
'd.:
Consider modelling the logic for somewhat-injective type functions. Take type-level Boolean
And
[5].
And
is not fully injective but:
- If the result is True, the two arguments must be True.
- If the result is False and one argument is True, the other must be False.
class ( (b3 ~ True) => (b1 ~ True, b2 ~ True), (b3 ~ False, b1 ~ True) => b2 ~ False, (b3 ~ False, b2 ~ True) => b1 ~ False ) => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool) | b1 b2 -> b3 where {} instance And True b2 b2 instance And False b2 False x3 = undefined :: (And b1 b2 True) => (b1, b2) -- should infer x3's type as :: (True, True)
[1]
comment:36 follow-up: 37 Changed 19 months ago by
f
should have an Ord a
constraint right?
f :: (Ord a, forall x. Ord x => Ord (m x)) => m a -> m a -> Bool
comment:37 Changed 19 months ago by
Replying to Iceland_jack:
f
should have anOrd a
constraint right?
You mean in the commit message? Yes, you're right.
(Before putting this on master I'll squash all the commits and write a new message.)
comment:38 Changed 16 months ago by
Differential Rev(s): | Phab:D4353 → Phab:D4724 |
---|
OK, finally I have a single squashed commit, rebased on master, ready to push to HEAD.
It's in Phab:D4724. Please review!
Simon
comment:40 Changed 16 months ago by
Keywords: | GHCProposal added |
---|
comment:41 Changed 16 months ago by
Milestone: | ⊥ → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Test Case: | → quantified-constraints/T2893{,a,c} |
My initial sense is this is a nice proposal.
I wonder a little bit how this would interact with other typeclass needs.
What's an example of a function that would need to be typed
? And would the compiler be able to infer the signature if it wasn't written?
(and is this even the right forum to be asking these questions in? Who wrote the proposal, and when?)
-Isaac Dupree