Opened 9 years ago
Last modified 4 months ago
#2893 new feature request
Implement "Quantified contexts" proposal
Reported by: | porges | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | ⊥ |
Component: | Compiler | Version: | 6.10.1 |
Keywords: | QuantifiedContexts | 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: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
See: QuantifiedContexts
Change History (27)
comment:1 Changed 9 years ago by
Cc: | id@… added |
---|
comment:2 Changed 9 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 9 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 8 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 7 years ago by
Type of failure: | → None/Unknown |
---|
This blog post provides an excellent motivating example for this feature.
comment:6 Changed 7 years ago by
Cc: | reiner.pope@… added |
---|
comment:7 Changed 7 years ago by
Cc: | illissius@… added |
---|
comment:8 Changed 6 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 5 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 5 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 5 years ago by
Cc: | shane@… added |
---|
comment:12 follow-up: 24 Changed 3 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 3 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 20 months ago by
Cc: | maoe added |
---|
comment:15 Changed 15 months ago by
Cc: | RyanGlScott added |
---|
comment:16 Changed 15 months ago by
Cc: | Iceland_jack added |
---|
comment:17 Changed 15 months 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 15 months 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 15 months 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 15 months 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 12 months 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 12 months 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 12 months 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 7 months 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 7 months ago by
Cc: | baramoglo added |
---|
comment:26 Changed 4 months ago by
Description: | modified (diff) |
---|
comment:27 Changed 4 months ago by
Keywords: | QuantifiedContexts added; proposal removed |
---|
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