[Haskell-cafe] How to expose if a constraint is satisfiable
Li-yao Xia
lysxia at gmail.com
Tue May 8 03:34:38 UTC 2018
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
More information about the Haskell-Cafe
mailing list