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

[Clinton Mead]

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 <lysxia at gmail.com> 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 <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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180508/9800efed/attachment.html>