[Haskell-cafe] How to expose if a constraint is satisfiable

[Li-yao Xia]

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 at gmail.com 
> <mailto:lysxia at 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