<div dir="auto">That's definitely part of the problem, but the way QuantifiedConstraints leads to local overlap is also generally troubling.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Apr 20, 2020, 9:44 PM John Ericson <john.ericson@obsidian.systems> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<p>I think that the problem there is not QuantifiedConstraints, but
Coercible (and likewise ~ and ~~) not working well with local
constraints of any sort. That's a problem I very much want fixed,
but still separate. It should be possible to turn a `Foo =>
Bar` into a `Dict Foo -> Dict Bar` can get oneself unstuck.</p>
<p>John<br>
</p>
<div>On 4/18/20 2:51 PM, David Feuer wrote:<br>
</div>
<blockquote type="cite">
<div dir="auto">It's been some months, but the last time I messed
with quantified constraints I found they didn't work well at all
with Coercible.</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Mar 14, 2020, 11:44 AM
Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi" target="_blank" rel="noreferrer">oleg.grenrus@iki.fi</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<p>QuantifiedConstraints are not buggy, but they are not
_complete_<br>
(I do mean that as "buggy" = not sound, properly
expressive = complete).<br>
<br>
There are at least three issues:<br>
<br>
1. Instance definition need UndecidableInstances (in my
opinion this is big deal)<br>
2. Instances are not elegant (easy to write, but not
elegant).<br>
3. QuantifiedConstraints resists to be abstracted over<br>
<br>
See <a href="https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8" rel="noreferrer noreferrer" target="_blank">https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8</a>
for<br>
the standalone code file.<br>
<br>
For the reasons below I wouldn't recommend using
QuantifiedConstraints.<br>
I very like them, but I'm not convinced the feature is
ready for "prime time".<br>
To put into perspective, I think code classes of
`singletons` are more ready to<br>
be included in `base` than changing instances of
Data.Functor.Sum and .Product.<br>
I do use singletons in my code more than
QuantifiedConstraints. :)<br>
<br>
I'm very worried how this change will affect libraries
like `free` and<br>
`recursion-schemes` and what builds on top of them.<br>
This is not only change to `base`, it strongly guides how
downstream<br>
libraries should be written (or changed) as well.<br>
<br>
On the other hand, I don't feel strongly about<br>
<br>
instance (Eq (f a), Eq (g a)) => Eq (Product f g a)<br>
<br>
Yet, in the light of `free` it is "a step backwards".<br>
See <a href="https://hackage.haskell.org/package/free-5/changelog" rel="noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/free-5/changelog</a><br>
<br>
---<br>
<br>
Simple example with `newtype Fix f = Fix (f (Fix f))`<br>
<br>
class Eq1 f where<br>
liftEq :: (a -> b -> Bool) -> f a -> f
b -> Bool<br>
<br>
class Eq1 f => Ord1 f where<br>
liftCompare :: (a -> b -> Ordering) -> f
a -> f b -> Ordering<br>
<br>
instance Eq1 f => Eq (Fix f) where<br>
(==) = eq where eq (Fix x) (Fix y) = liftEq eq x y<br>
<br>
instance Ord1 f => Ord (Fix f) where<br>
compare = cmp where cmp (Fix x) (Fix y) =
liftCompare cmp x y<br>
<br>
works. It's boilerplate, but it's already written.<br>
<br>
However, if we want to use QuantifiedConstraints,<br>
then we<br>
<br>
1. need UndecidableInstances<br>
2. and then the code turns out to be less elegant:<br>
<br>
instance (forall x. Eq x => Eq (f x)) => Eq (Fix f)
where<br>
(==) = eq where eq (Fix x) (Fix y) = x == y<br>
<br>
instance (forall x. Ord x => Ord (f x)) => Ord (Fix
f) where<br>
compare = cmp where cmp (Fix x) (Fix y) = compare x y<br>
<br>
fails to compile with<br>
<br>
GHCi, version 8.8.3: <a href="https://www.haskell.org/ghc/" rel="noreferrer noreferrer" target="_blank">https://www.haskell.org/ghc/</a>
:? for help<br>
[1 of 1] Compiling Main ( Ord1.hs,
interpreted )<br>
<br>
Ord1.hs:28:10: error:<br>
• Could not deduce (Ord x)<br>
arising from the superclasses of an instance
declaration<br>
<br>
we need to write Ord instance differently<br>
<br>
instance (forall x. Ord x => Ord (f x), forall x. Eq
x => Eq (f x)) => Ord (Fix f) where<br>
compare = cmp where cmp (Fix x) (Fix y) = compare x
y<br>
<br>
<br>
This _cannot_ be made to work:<br>
<br>
forall x. Ord x => Ord (f x)<br>
<br>
doesn't entail<br>
<br>
forall x. Eq x => Eq (f x)<br>
<br>
If you try to write defaultLiftEq using liftCompare<br>
<br>
defaultLiftEq :: Ord1 f => (a -> b -> Bool)
-> f a -> f b -> Bool<br>
defaultLiftEq eq x y = EQ == liftCompare _problem_ x y<br>
<br>
then you will se a problem.<br>
<br>
---<br>
<br>
Third issue is that We cannot abstract over
QuantifiedConstraints.<br>
<br>
Take an example `Dict`. We can use `Dict` for various
things.<br>
<br>
data Dict :: (k -> Constraint) -> k -> *
where<br>
Dict :: c a => Dict c a<br>
<br>
It nicely uses PolyKinds extension so we can write:<br>
<br>
eqInt :: Dict Eq Int<br>
eqInt = Dict<br>
<br>
eq1List :: Dict Eq1 []<br>
eq1List = Dict<br>
<br>
And we can use Dict to *manually* thread information<br>
<br>
entail :: Dict Ord1 f -> Dict Eq1 f<br>
entail Dict = Dict<br>
<br>
The selling pitch of QuantifiedConstraints, that we could
get this for free.<br>
Above Ord (Fix) example however makes me suspicious. Let's
try:<br>
<br>
eqQList :: Dict (forall x. Eq x => Eq (f x)) []<br>
eqQList = undefined<br>
<br>
But it doesn't work!<br>
<br>
Ord1.hs:53:28: error:<br>
• Expected kind ‘(* -> *) -> Constraint’,<br>
but ‘Eq (f x)’ has kind ‘*’<br>
• In the first argument of ‘Dict’, namely<br>
‘(forall x. Eq x => Eq (f x))’<br>
In the type signature:<br>
eqQList :: Dict (forall x. Eq x => Eq (f
x)) []<br>
|<br>
53 | eqQList :: Dict (forall x. Eq x => Eq (f x))
[]<br>
|<br>
<br>
Ord1.hs:53:36: error:<br>
• Expected a type, but ‘Eq (f x)’ has kind
‘Constraint’<br>
• In the first argument of ‘Dict’, namely<br>
‘(forall x. Eq x => Eq (f x))’<br>
In the type signature:<br>
eqQList :: Dict (forall x. Eq x => Eq (f
x)) []<br>
|<br>
53 | eqQList :: Dict (forall x. Eq x => Eq (f x))
[]<br>
| ^^^^^^^^<br>
<br>
Then we remember that we have seen that,<br>
we **cannot define** type synonyms for quantified
constraints<br>
<br>
type Eq1' f = forall x. Eq x => Eq (f x)<br>
<br>
errors with<br>
<br>
Ord1.hs:56:33: error:<br>
• Expected a type, but ‘Eq (f x)’ has kind
‘Constraint’<br>
<br>
Luckily GHC-8.10.1 (which is not released at the moment of
writing)<br>
will give us ability to say<br>
<br>
type Eq1' :: (* -> *) -> Constraint<br>
type Eq1' f = forall x. Eq x => Eq (f x)<br>
<br>
This is promising! Let's try to fix eqQList<br>
<br>
eqQList2 :: Dict Eq1' []<br>
eqQList2 = undefined<br>
<br>
But that doesn't work. Type-aliases have to be fully
applied!<br>
<br>
How in Haskell we fix issues when type-aliases (of
classes) need to be partially<br>
evaluated? We defined<br>
<br>
class ... => Example a b c<br>
instance ... => Example a b c<br>
<br>
Third try<br>
<br>
eqQList3 :: Dict Eq1'' f<br>
eqQList3 = Dict<br>
<br>
The type signature is accepted, but the implementation is
not<br>
<br>
Ord1.hs:67:12: error:<br>
• Could not deduce (Eq (f x)) arising from a use of
‘Dict’<br>
<br>
At this point I'm clueless.<br>
<br>
---<br>
<br>
Best regards,<br>
Oleg<br>
<br>
P.S. If we would like to take QuantifiedConstraints
somewhere into use, then IMO we should start with
MonadTrans class. IIRC it's well motivated in the paper.
But UndecidableInstances is very unfortunate.<br>
</p>
<div>On 14.3.2020 16.10, chessai . wrote:<br>
</div>
<blockquote type="cite">
<div dir="auto">I can second Richard's estimation of
QuantifiedConstraints, I have used them a lot in my own
code since they were in HEAD. I consider it a
sufficiently stable feature to include in base or any
library. </div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Mar 14, 2020,
4:16 AM Richard Eisenberg <<a href="mailto:rae@richarde.dev" rel="noreferrer noreferrer" target="_blank">rae@richarde.dev</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word;line-break:after-white-space"><br>
<div><br>
<blockquote type="cite">
<div>On Mar 14, 2020, at 4:14 AM, Eric Mertens
<<a href="mailto:emertens@gmail.com" rel="noreferrer noreferrer noreferrer" target="_blank">emertens@gmail.com</a>>
wrote:</div>
<br>
<div><span style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline!important">The
last thing I'd heard about quantified
constraints was that they were buggy and
I've been avoiding relying on them. (I
should probably review that assumptions at
some point.)</span></div>
</blockquote>
</div>
<br>
<div>Without expressing an opinion about chessai's
proposal (which I have not really thought about):
quantified constraints are in good shape and ready
for prime time. They have limitations (e.g. you
can't mention a type family to the right of the
=>), but when they are valid, they work well.
I'll never swear that a feature is bug-free, but I
think it's reasonable to consider using quantified
constraints in `base`.</div>
<div><br>
</div>
<div>Richard</div>
</div>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Libraries mailing list
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Libraries mailing list
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank" rel="noreferrer">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</div>
</blockquote></div>