Implement "Quantified contexts" proposal

[porges]

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).

[guest]

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

[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)

[simonpj]

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

[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.

[lilac]

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

[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.

[sjoerd_visscher]

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.

[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.