<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">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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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/" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">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" 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" 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>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<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><br>
</blockquote></div>