<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Dec 28, 2017 at 2:44 AM, Ryan Reich <span dir="ltr"><<a href="mailto:ryan.reich@gmail.com" target="_blank">ryan.reich@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Your 1) is a very erudite way of saying "you forgot about my 'constraints' package" :)  Which I did.  </div></div></blockquote><div><br></div><div>Not exactly. The constraints package can construct </div><div><br></div><div>(:-) :: Constraint -> Constraint -> *</div><div><br></div><div>but</div><div><br></div><div>(|-) :: Constraint -> Constraint -> Constraint</div><div><br></div><div>would really need compiler support to work correctly. That said, it might be able to be written as a GHC plugin, now that I think about it. (3) could also most likely be handled that way.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Although it's just a little more awkward syntactically to write `(a :- b) -> whatever` instead of `(a |- b) => whatever`, which is only possible with a GHC extension, it obviously solves the problem of using constraints of the form `c1 implies c2`, i.e. 0-ary constraint functions.  If I understand you correctly, you are saying that an internal entailment operator is consistent with the other workings of constraints, and pointing out the concepts that need to be handled in implementing this in GHC?<br></div></div></blockquote><div> </div><div>Yep.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Re 2): I am probably missing something when I think that `type (c1 :: * -> Constraint) ::- (c2 :: * -> Constraint) = forall a. (c1 a :- c2 a)` works for 1-ary entailment; for instance `Sub Dict :: Ord ::- Eq` appears not to bother ghci.</div></div></blockquote><div><br></div><div>data Jet f a = a :- Jet f (f a)</div><div><br></div><div>is an example of a data type for which show, (==), compare, etc. are a pain in the neck to write.</div><div><br></div><div>For that you really want something like</div><div><br></div><div>instance (Ord a, forall x. Ord x |- Ord (f x)) => Ord (Jet f a)</div><div><br></div><div>In the constraints vocabulary today this particular usecase can sort of be faked by using Lifting:</div><div><br></div><div>instance (Lifting Ord f, Ord a) => Ord (Jet f a)</div><div><br></div><div>but GHC doesn't know enough to automatically bring the right stuff into scope to make it automatically work, you have to write a crapload of manual Lifting instances you might not expect, and you have to open the dictionary from Lifting by hand, and its generally a mess to use.</div><div><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 dir="ltr"><div></div><div>3) It would be neat, for sure, to have this sum type.  Is that the full extent of boolean logic you can define on Constraint without losing thinness?</div></div></blockquote><div><br></div><div>Technically it is a Heyting algebra. You can go a bit crazier with the type theory for the category of constraints and show that its locally cartesian closed, which seems to admit some funny interpretations of MLTT in it as well.</div><div><br></div><div>-Edward</div><div><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 class="gmail-HOEnZb"><div class="gmail-h5"><div class="gmail_extra"><div class="gmail_quote">On Wed, Dec 27, 2017 at 11:17 AM, Edward Kmett <span dir="ltr"><<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Just a few old observations I've made from implementing these things into type systems of my own:</div><div><br></div>1.) An internal hom for the category of constraints is admissible:<div><br></div><div>(|-) :: Constraint -> Constraint -> Constraint</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>2.) Quantification over constraints is also admissible.</div><div><br></div><div>Neither one compromises the "thinness" of the category of constraints that provides us global coherence of instance resolution</div><div><br></div><div><div>In this case the property that if D is thin, so is [C,D]. forall here can quantify over any other kind you want.</div></div><div><br></div><div>Unfortunately, neither implemented in Haskell.</div><div><br></div><div>You'd need both of them to be able to talk about constraints like (forall a. Eq a |- Eq (f a)). </div><div><br></div><div>Together could eliminate, morally, the entire Data.Functor.Classes mess. (That said, as implemented those classes are a bit stronger than the quantified form)</div><div><br></div><div>3.) Constraint also admits a sum type, (\/) but it acts more like a least upper bound than an either.</div><div><br></div><div>It is much easier to talk about in the category of constraints using the first part above.</div><div><br></div><div>Given (p |- r, q |- r), (p \/ q) |- r and vice versa.</div><div><br></div><div>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.</div><div><br></div><div>Getting this stuff into GHC is the tricky part!</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote"><span>On Wed, Dec 27, 2017 at 2:50 AM, Ryan Reich <span dir="ltr"><<a href="mailto:ryan.reich@gmail.com" target="_blank">ryan.reich@gmail.com</a>></span> wrote:<br></span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span><div dir="ltr"><div>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.<br></div></div>
<br></span>______________________________<wbr>_________________<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-bi<wbr>n/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div></div>