<div dir="ltr"><div>as an additional point of data, <br></div><div><a href="https://github.com/ekmett/bytes/pull/49#issuecomment-580924670">https://github.com/ekmett/bytes/pull/49#issuecomment-580924670</a> and the indirectly linked ticket <a href="https://gitlab.haskell.org/ghc/ghc/issues/17767#note_251123">https://gitlab.haskell.org/ghc/ghc/issues/17767#note_251123</a></div><div>is an example of how not trivial a pretty simple use of quantified constraints / related machinery can be!</div><div><br></div><div><br></div><div>a good "guiding light" for core libraries in haskell perhaps should be "what choices jointly give the best type inference, composability, generality, performance, and usability" and when we hit a trade off for these parameters, make sure we understand those and have very well understood tradeoffs.</div><div><br></div><div>@daniel for these sorts of instance renovation proposals, its probably best to show case "heres the type and instance and uses" in each of the K different flavors and what gets better/easier/harder simpler. I honestly dont do it as often as I should myself!</div><div><br></div><div>In this case, putting together a tiny repo with different module doing the various flavors and how they work might be best for grounding this. bonus points if its cabalized so that folks on different lagging rates of ghc versions can poke around :) <br></div><div><br></div><div>(one idea i've been thinking about is how to best make various phases of possibly nontrivial proposals easy to evaluate and compare for impact and benefit, but thats a discussion for another time)</div><div><br></div><div>as ever, be well all on this bizarre spring we're all experiencing <br></div><div><br></div><div>-Carter<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Mar 14, 2020 at 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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">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">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">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">rae@richarde.dev</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="overflow-wrap: break-word;"><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" 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">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">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" 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" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>