Hi Clinton,

On 05/07/2018 08:39 AM, Clinton Mead wrote:

On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <lysxia@gmail.com <mailto:lysxia@gmail.com>> wrote:

    Hi Clinton,

        instance A t => C' t Satisfied tb where
            ...

        instance B t => C' t ta Satisfied where
            ...

        instance (A t, B t) => C' t Satisfied Satisfied where
            ...


    The first two instances will only be picked if `ta` or `tb` can be
    determined to not "unify" with `Satisfied`. But a type family that
    cannot reduce will still "unify" with anything (it might just be
    that the rules to reduce it exist but are not in scope).

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"?

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.

For a concrete illustration, consider the following newtype, whose Ord instance depends on the existence of Ord or Show for the wrapped type:


newtype T a = T a

instance OrdIf a (IsSatisfiable (Ord a)) (IsSatisfiable (Show a))
  => Ord (T a) where
  compare = compareIf

class OrdIf a ta tb where
  compareIf :: a -> a -> Ordering

instance Ord a => OrdIf a Satisfied tb where
  compareIf (T a) (T b) = compare a b

instance Show a => OrdIf a ta Satisfied where
  compareIf (T a) (T b) = compare (show a) (show b)

instance Ord a => OrdIf a Satisfied Satisfied where
  compareIf (T a) (T b) = compare b a  -- flipped


We can have the following three definitions, that use three different instances for (Ord (T a)).


f1 :: Ord a => T a -> T a -> Ordering
f1 = compare  -- first OrdIf instance

f2 :: Show a => T a -> T a -> Ordering
f2 = compare  -- second OrdIf instance

f3 :: (Ord a, Show a) => T a -> T a -> Ordering
f3 = compare  -- third OrdIf instance


Now specialize them to a type that has both Ord and Show instances.


g1 :: T Int -> T Int -> Ordering
g1 = f1

g2 :: T Int -> T Int -> Ordering
g2 = f2

g3 :: T Int -> T Int -> Ordering
g3 = f3


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).


g4 :: T Int -> T Int -> Ordering
g4 = compare


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.

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).

    These instances are only useful if we can actually decide
    satisfiability of constraints, which contradicts the open-world
    assumption as you mentioned.


    IsSatisfiable c = Satisfied -- (if c is satisfiable)
    IsSatisfiable c = Unsatisfiable -- (if c is not satisfiable)

But your example is different to mine. I've said I'm looking for the following:

IsSatisfiable c = Satisfied -- (if c is satisfiable)
IsSatisfiable c =*IsSatisfiable c*-- (if c is not satisfiable)

Notice I never mentioned "Unsatisfiable". Without "Unsatisfiable", I don't see how this violates the open-world assumption.

Sorry, that was a clumsy way for me to say that this approach you propose would not work.

Regards,
Li-yao