Opened 9 years ago

Last modified 8 weeks ago

#2893 new feature request

Implement "Quantified contexts" proposal

Reported by: porges Owned by:
Priority: normal Milestone:
Component: Compiler Version: 6.10.1
Keywords: proposal 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

See: http://haskell.org/haskellwiki/Quantified_contexts

Motivating example is collapsing insomeway-identical classes such as Monoid and MonadPlus into a single class (with accompanying functions).

Change History (25)

comment:1 Changed 9 years ago by guest

Cc: id@… added

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

:: (Monad m, forall a. Monoid (m a)) => (something or other)

? 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

comment:2 Changed 9 years ago by porges

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 8 years ago by simonpj

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 porges

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 lilac

Type of failure: None/Unknown

This blog post provides an excellent motivating example for this feature.

comment:6 Changed 7 years ago by reinerp

Cc: reiner.pope@… added

comment:7 Changed 6 years ago by illissius

Cc: illissius@… added

comment:8 Changed 6 years ago by batterseapower

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 sjoerd_visscher

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 sjoerd_visscher

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 4 years ago by duairc

Cc: shane@… added

comment:12 Changed 3 years ago by heisenbug

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 simonpj

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 15 months ago by maoe

Cc: maoe added

comment:15 Changed 11 months ago by RyanGlScott

Cc: RyanGlScott added

comment:16 Changed 10 months ago by Iceland_jack

Cc: Iceland_jack added

comment:17 Changed 10 months ago by Iceland_jack

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 functor f, it should act in a uniform way on all the types f a. Therefore, we would like to assert a constraint something like forall 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 10 months ago by Iceland_jack

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 10 months ago by Iceland_jack

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)
Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:20 Changed 10 months ago by RyanGlScott

Iceland_jack, there are two problems with using typeclasses like these to "solve" this problem:

  1. 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.
  2. 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 an instance () :=> Eq ():
ins :: () :- Eq ()

But the following would not typecheck!

ins :: Eq () :- Eq ()

Because there is no instance Eq () => Eq () anywhere (and thus no instance Eq () :=> Eq ()), only instance Eq (). But the implication Eq () => Eq () should obviously hold. Does that mean we should also generate an instance Eq () :=> Eq () automatically? But what about (Eq (), Ord ()) => Eq ()? (Eq (), Ord (), Show ()) => Eq ()? There is an extremely high number of contexts in which Eq () 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 in reply to:  20 Changed 7 months ago by Iceland_jack

Replying to RyanGlScott:

  1. 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 7 months ago by goldfire

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 7 months ago by Iceland_jack

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 in reply to:  12 Changed 8 weeks ago by dfeuer

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 all Bool alternatives are covered with instance 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 8 weeks ago by baramoglo

Cc: baramoglo added
Note: See TracTickets for help on using tickets.