<div dir="auto">For whatever it's worth, it seems to me that the two next steps, in no particular order, should likely be<div dir="auto"><br></div><div dir="auto">1. Add quantified contexts. These should obsolete Data.Constraint.Forall by offering a much nicer API (without needing to use `inst`, etc., manually).</div><div dir="auto"><br></div><div dir="auto">2. Add the ability to at least express constraint implication at the constraint level, and propagate some of that information automatically. Trying to be too clever seems to run into backtracking, so it's not clear that we should try to jump straight to a full constraint implication system. If we could even get a version that requires manual guidance to use (like Data.Constraint.Forall does today), we'd surely be making some progress.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Jan 2, 2018 5:08 AM, "Simon Peyton Jones via Libraries" <<a href="mailto:libraries@haskell.org">libraries@haskell.org</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">





<div lang="EN-GB" link="blue" vlink="purple">
<div class="m_491593542455268203WordSection1">
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Getting this stuff into GHC is the tricky part!<u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Indeed… but step 1 is to articulate a well-formed specification.  I’m not close enough to this conversation to understand all the details, let alone form a specification.  But perhaps some of you are.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">I think (2) is described here:
<a href="https://ghc.haskell.org/trac/ghc/wiki/QuantifiedContexts" target="_blank">https://ghc.haskell.org/trac/<wbr>ghc/wiki/QuantifiedContexts</a>.  I have been keen on this proposal for years, just lacking time to execute on it.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Libraries [mailto:<a href="mailto:libraries-bounces@haskell.org" target="_blank">libraries-bounces@<wbr>haskell.org</a>]
<b>On Behalf Of </b>Edward Kmett<br>
<b>Sent:</b> 27 December 2017 19:18<br>
<b>To:</b> Ryan Reich <<a href="mailto:ryan.reich@gmail.com" target="_blank">ryan.reich@gmail.com</a>><br>
<b>Cc:</b> Haskell Libraries <<a href="mailto:libraries@haskell.org" target="_blank">libraries@haskell.org</a>><br>
<b>Subject:</b> Re: Constraint implication<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Just a few old observations I've made from implementing these things into type systems of my own:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
1.) An internal hom for the category of constraints is admissible:<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
(|-) :: Constraint -> Constraint -> Constraint<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
models entailment, and effectively brings into scope a local rule, but global instance resolution isn't lost if this is only produced from existing instances.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
To your point, this is analogous to the (:-) :: Constraint -> Constraint -> * external hom for the category of constraints provided by my constraints package, but it is internal, with all of the appropriate CCC operations.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
2.) Quantification over constraints is also admissible.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Neither one compromises the "thinness" of the category of constraints that provides us global coherence of instance resolution<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
In this case the property that if D is thin, so is [C,D]. forall here can quantify over any other kind you want.<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Unfortunately, neither implemented in Haskell.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
You'd need both of them to be able to talk about constraints like (forall a. Eq a |- Eq (f a)). <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Together could eliminate, morally, the entire Data.Functor.Classes mess. (That said, as implemented those classes are a bit stronger than the quantified form)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
3.) Constraint also admits a sum type, (\/) but it acts more like a least upper bound than an either.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
It is much easier to talk about in the category of constraints using the first part above.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Given (p |- r, q |- r), (p \/ q) |- r and vice versa.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
The key to keeping the category of constraints thin is that you can't case analyze on it, its more like if you look at, say, Ord [a] \/ Eq a you can get to any constraint that you could get to given the intersection of both, not using the particulars of either.
 e.g. its morally as powerful as Eq [a] in this case.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Getting this stuff into GHC is the tricky part!<u></u><u></u></p>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
-Edward<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Wed, Dec 27, 2017 at 2:50 AM, Ryan Reich <<a href="mailto:ryan.reich@gmail.com" target="_blank">ryan.reich@gmail.com</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
The Constraint kind appears to lack an interface to an important capability that is already part of the type checker: constraint implication.  Namely, the ability to provide a witness for the statement "constraint c1 implies constraint c2" or, more importantly,
 "for all a, constraint (c1 a) implies constraint (c2 a)", where c1 and c2 are now constraint-valued type functions (and possibly even for constraint functions with multiple parameters).  It seems to me that this can follow the pattern of the "magic" Coercible
 type class and the (non-magic) Coercion data type; it provides the programmer with an analogous value to this example that can be obtained in apparently no other way.<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
<br>
______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Flibraries&data=04%7C01%7Csimonpj%40microsoft.com%7C8f41822fa9ff4b253ea808d54d5e9adc%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636499991092450873%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwifQ%3D%3D%7C-1&sdata=QquaudC3jd%2FHr33l6N3e0OCRRK8%2F2qhYX7p5m3uSyAc%3D&reserved=0" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
</div>
</div>

<br>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">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-<wbr>bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div></div>