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

Hi Li-yao I understand this issue, but I think what your describing doesn't relate to what I'm talking about uniquely. For example: instance {-# OVERLAPPABLE #-} Num x => C x where ... instance {-# OVERLAPPING #-} C Int where ... is completely legal, and the instance used depends on context. 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. On Tue, May 8, 2018 at 1:34 PM, Li-yao Xia wrote:

Hi Clinton,

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

...

On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia > 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