<div dir="ltr">Hi Li-yao<div><br>I understand this issue, but I think what your describing doesn't relate to what I'm talking about uniquely.</div><div><br></div><div>For example:</div><div><br></div><div>instance {-# OVERLAPPABLE #-} Num x => C x where ...</div><div>
<div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">instance {-# OVERLAPPING #-} C Int where ...<br><br></div></div><div>is completely legal, and the instance used depends on context.</div><div><br></div><div>This is an issue with overlapping instances, but already GHC allows it. I don't think what I'm proposing is any worse to what's already legal.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, May 8, 2018 at 1:34 PM, Li-yao Xia <span dir="ltr"><<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Clinton,<br>
<br>
On 05/07/2018 08:39 AM, Clinton Mead wrote:<span class=""><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
<br>
On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a> <mailto:<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a>>> wrote:<br>
<br>
Hi Clinton,<br>
<br>
instance A t => C' t Satisfied tb where<br>
...<br>
<br>
instance B t => C' t ta Satisfied where<br>
...<br>
<br>
instance (A t, B t) => C' t Satisfied Satisfied where<br>
...<br>
<br>
<br>
The first two instances will only be picked if `ta` or `tb` can be<br>
determined to not "unify" with `Satisfied`. But a type family that<br>
cannot reduce will still "unify" with anything (it might just be<br>
that the rules to reduce it exist but are not in scope).<br>
<br>
Why is this the case? Can't the first instance be picked even if tb hasn't been determined not to unify with "Satisfied", as long as the 2nd type variable does unify with "Satisfied"?<br>
</blockquote>
<br></span>
If you pick an instance to solve a constraint that still unifies with another one, the broken assumption is uniqueness of instances. Many libraries assume instances are unique. The most common example is containers, which uses Ord to implement Set/Map with binary search trees. (De)serialization libraries are another example.<br>
<br>
For a concrete illustration, consider the following newtype, whose Ord instance depends on the existence of Ord or Show for the wrapped type:<br>
<br>
<br>
newtype T a = T a<br>
<br>
instance OrdIf a (IsSatisfiable (Ord a)) (IsSatisfiable (Show a))<br>
=> Ord (T a) where<br>
compare = compareIf<br>
<br>
class OrdIf a ta tb where<br>
compareIf :: a -> a -> Ordering<br>
<br>
instance Ord a => OrdIf a Satisfied tb where<br>
compareIf (T a) (T b) = compare a b<br>
<br>
instance Show a => OrdIf a ta Satisfied where<br>
compareIf (T a) (T b) = compare (show a) (show b)<br>
<br>
instance Ord a => OrdIf a Satisfied Satisfied where<br>
compareIf (T a) (T b) = compare b a -- flipped<br>
<br>
<br>
We can have the following three definitions, that use three different instances for (Ord (T a)).<br>
<br>
<br>
f1 :: Ord a => T a -> T a -> Ordering<br>
f1 = compare -- first OrdIf instance<br>
<br>
f2 :: Show a => T a -> T a -> Ordering<br>
f2 = compare -- second OrdIf instance<br>
<br>
f3 :: (Ord a, Show a) => T a -> T a -> Ordering<br>
f3 = compare -- third OrdIf instance<br>
<br>
<br>
Now specialize them to a type that has both Ord and Show instances.<br>
<br>
<br>
g1 :: T Int -> T Int -> Ordering<br>
g1 = f1<br>
<br>
g2 :: T Int -> T Int -> Ordering<br>
g2 = f2<br>
<br>
g3 :: T Int -> T Int -> Ordering<br>
g3 = f3<br>
<br>
<br>
Referential transparency is lost. If you replace fi (for i=1,2,3) with its body (compare), only g3 doesn't change meaning (and that's assuming the most specific instance was picked in f3, which can be nontrivial to guarantee in general without that rule about ensuring there is no other unifiable instance).<br>
<br>
<br>
g4 :: T Int -> T Int -> Ordering<br>
g4 = compare<br>
<br>
<br>
Perhaps a more general litmus test for features related to instance resolution is: can the meaning of a well-typed polymorphic function change if I make it (more) monomorphic, or if I add instances to the context? I believe I demonstrated that can happen above, which is bad.<br>
<br>
The rationale is that we should be able to understand what a function does without keeping track of all instances we import (it's right there in the PVP that new non-orphan instances are not breaking changes), and without knowing the exact types of local functions (it happens often that a function has a much more general inferred type than what we have in mind).<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
These instances are only useful if we can actually decide<br>
satisfiability of constraints, which contradicts the open-world<br>
assumption as you mentioned.<br>
<br>
<br>
IsSatisfiable c = Satisfied -- (if c is satisfiable)<br>
IsSatisfiable c = Unsatisfiable -- (if c is not satisfiable)<br>
<br>
But your example is different to mine. I've said I'm looking for the following:<br>
<br>
IsSatisfiable c = Satisfied -- (if c is satisfiable)<br></span>
IsSatisfiable c =*IsSatisfiable c*-- (if c is not satisfiable)<span class=""><br>
<br>
Notice I never mentioned "Unsatisfiable". Without "Unsatisfiable", I don't see how this violates the open-world assumption.<br>
<br>
</span></blockquote>
<br>
Sorry, that was a clumsy way for me to say that this approach you propose would not work.<br>
<br>
Regards,<br>
Li-yao<br>
</blockquote></div><br></div>