GHC: Ticket #2893: Implement "Quantified contexts" proposal
http://ghc.haskell.org/trac/ghc/ticket/2893
<p>
See: <a class="ext-link" href="http://haskell.org/haskellwiki/Quantified_contexts"><span class="icon"></span>http://haskell.org/haskellwiki/Quantified_contexts</a>
</p>
<p>
Motivating example is collapsing insomeway-identical classes such as Monoid and MonadPlus into a single class (with accompanying functions).
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2893
Trac 1.0.1guestTue, 23 Dec 2008 16:09:15 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:1
<ul>
<li><strong>cc</strong>
<em>id@…</em> added
</li>
</ul>
<p>
My initial sense is this is a nice proposal.
</p>
<p>
I wonder a little bit how this would interact with other typeclass needs.
</p>
<p>
What's an example of a function that would need to be typed
</p>
<pre class="wiki">:: (Monad m, forall a. Monoid (m a)) => (something or other)
</pre><p>
? And would the compiler be able to infer the signature if it wasn't written?
</p>
<p>
(and is this even the right forum to be asking these questions in? Who wrote the proposal, and when?)
</p>
<p>
-Isaac Dupree
</p>
TicketporgesWed, 24 Dec 2008 11:43:26 GMT
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:2
<p>
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]):
</p>
<p>
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:
</p>
<pre class="wiki">instance (Foldable l, forall a. Monoid (l a)) => Applicative l where
fs <*> xs = foldMap (<$> xs) fs
</pre><p>
I may be horribly wrong, however :)
</p>
<p>
(Also I can't implement pure :P)
</p>
TicketsimonpjMon, 29 Dec 2008 15:30:30 GMTdifficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:3
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>_|_</em>
</li>
</ul>
<p>
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 <tt>Typeable2</tt>, <tt>Typeable3</tt> etc classes the solution is presumably polymorphism at the kind level. (Tim Sheard's language Omega has this.)
</p>
<p>
Still, I recognise the merit of quantification in contexts. Indeed, Ralf Hinze and I suggested it back in 2000 in Section 7 of <a class="ext-link" href="http://research.microsoft.com/en-us/um/people/simonpj/papers/derive.htm"><span class="icon"></span>Derivable type classes</a>. (This section is rather independent of the rest of the paper.)
</p>
<p>
However, attractive as it is, it's quite a big step to add something akin to local instance declarations. Our ICFP'08 paper <a class="ext-link" href="http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm"><span class="icon"></span>Type checking with open type functions</a> relies rather crucially on <em>not</em> having such local instances. (We've managed to simplify the algorithm quite a bit since then, but it still relies on that assumption.)
</p>
<p>
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.
</p>
<p>
Meanwhile, clarifying the proposal would be a good thing, even if it's not adopted right away.
</p>
<p>
Simon
</p>
TicketporgesSun, 28 Jun 2009 23:00:45 GMT
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:4
<p>
A short version... we allow contexts of the form:
</p>
<pre class="wiki">(forall a. Bar f a) => Foo f
</pre><p>
And more generally, these contexts can have contexts of their own:
</p>
<pre class="wiki">(forall a. (Baz a) => Bar f a) => Foo f
</pre><p>
I'm not sure if the 'more general' version adds extra difficulty in type-checking, as I am not very familiar with its intricacies.
</p>
<p>
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.
</p>
TicketlilacWed, 22 Sep 2010 15:27:05 GMTfailure set
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:5
<ul>
<li><strong>failure</strong>
set to <em>None/Unknown</em>
</li>
</ul>
<p>
<a class="ext-link" href="http://mainisusuallyafunction.blogspot.com/2010/09/higher-rank-type-constraints.html"><span class="icon"></span>This blog post</a> provides an excellent motivating example for this feature.
</p>
TicketreinerpWed, 20 Oct 2010 04:37:59 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:6
<ul>
<li><strong>cc</strong>
<em>reiner.pope@…</em> added
</li>
</ul>
TicketillissiusSat, 30 Apr 2011 11:18:26 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:7
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:7
<ul>
<li><strong>cc</strong>
<em>illissius@…</em> added
</li>
</ul>
TicketbatterseapowerSat, 10 Sep 2011 19:37:24 GMT
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:8
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:8
<p>
As the blog post points out (and I recently rediscovered) GHC already supports this feature in a more elaborate form. This works:
</p>
<pre class="wiki">{-# 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
</pre><p>
But this is rejected:
</p>
<pre class="wiki">g :: (forall b. Foo [b]) => String
g = foo "Hello" ++ foo [1, 2, 3]
use_foo' :: String
use_foo' = g
</pre><p>
So there doesn't seem to be a fundamental difficulty here.
</p>
Ticketsjoerd_visscherSat, 30 Jun 2012 12:07:01 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:9
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:9
<ul>
<li><strong>cc</strong>
<em>sjoerd@…</em> added
</li>
</ul>
<p>
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.
</p>
<p>
As I see it, the problem is with matching the need for a constraint with the available constraints or instances. See <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/7019" title="bug: Wrong error message when using forall in constraints (closed: fixed)">#7019</a>, the error is "Could not deduce (Monoid [b]) from the context (forall a. Monoid [a])".
</p>
<p>
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'".
</p>
<p>
So it seems that with implementing ConstraintKinds, there has been made a big step towards an implementation of quantified contexts.
</p>
Ticketsjoerd_visscherSat, 14 Jul 2012 11:19:55 GMT
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:10
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:10
<p>
Edward Kmett created a workaround: <a class="ext-link" href="http://hackage.haskell.org/packages/archive/constraints/0.3.1/doc/html/Data-Constraint-Forall.html"><span class="icon"></span>Data.Constraint.Forall</a>
</p>
<p>
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.
</p>
TicketduaircTue, 12 Mar 2013 13:55:14 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:11
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:11
<ul>
<li><strong>cc</strong>
<em>shane@…</em> added
</li>
</ul>
TicketheisenbugSun, 13 Jul 2014 11:27:36 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:12
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:12
<ul>
<li><strong>cc</strong>
<em>ggreif@…</em> added
</li>
</ul>
<p>
Copying a use-case from <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9196" title="bug: Higher-rank constraint treated as type instead (closed: fixed)">#9196</a>:
</p>
<p>
My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-<tt>*</tt> kind, that is an ADT.
</p>
<p>
See:
</p>
<pre class="wiki">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)) =>...
</pre><p>
Here the <tt>forall</tt> condition is satisfiable, as all <tt>Bool</tt> alternatives are covered with <tt>instance</tt> declarations.
</p>
TicketsimonpjMon, 14 Jul 2014 07:56:25 GMT
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:13
http://ghc.haskell.org/trac/ghc/ticket/2893#comment:13
<p>
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.
</p>
<p>
It would be a useful feature. I've wanted it since at least 2000 (see <a class="ext-link" href="http://research.microsoft.com/en-us/um/people/simonpj/papers/derive.htm"><span class="icon"></span>Derivable Type Classes</a>).
</p>
<p>
Simon
</p>
Ticket