How to expose if a constraint is satisfiable

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
18 messages Options
Reply | Threaded
Open this post in threaded view
|

How to expose if a constraint is satisfiable

Clinton Mead
It's occurred to me that one could write a class C t which is satisfied whenever (A t) or (B t) is satisfied like so:

---

data Satisfied

type family IsSatisfiable :: Constraint -> Type

class A t

class B t

class C' t ta tb

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

class C' t ( IsSatisfiable (A t)) ( IsSatisfiable (B t)) => C t

---

We may need overlapping instances (with all the caveats that come with it) but it should be fine otherwise.

"IsSatisfiable" here is defined as follows:

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

That's all that's needed. And it seems to be a reasonable type function. I note classes are open, so perhaps it could be dangerous to state that a constraint is not satisfiable (because it might be in another part of a program) but simply not reducing if we can't satisfy the constraint locally should be fine I think. At worst we'll get a compile error, but we shouldn't get inconsistent types. 

Is there anyway to implement this type function, or alternatively an approach which allows this type of "inherit from two classes" idea?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

AntC
It's occurred to me that one could write a class C t which is satisfied
> whenever (A t) or (B t) is satisfied like so:

Hi Clinton, this sounds like you might want "Choosing a type-class instance based on the context"

> --- > > data Satisfied > > type family IsSatisfiable :: Constraint -> Type

That type family is doing the same job as auxiliary class `ShowPred` on that wiki page.

Rather than all the machinery you give for the disjunction, you could use another type family:

type family EitherSatisfied :: Type -> Type -> Type
instance EitherSatisfied Satisfied tb = Satisfied
instance EitherSatisfied ta Satisfied = Satisfied

Those two instances do overlap (as you expected); and they exhibit confluence, aka coincident overlap (they produce the same result); so that's fine.

But you haven't given any instances for `IsSatisfiable`. How do you expect to get from the Constraint to the `Satisfied` type?

You say

> IsSatisfiable c = Satisfied -- (if c is satisfiable)

What are you going to put for `c`? If you follow that wiki page, you'll need to in effect repeat every instance decl for classes `A, B`:

instance A Int where ...

type instance IsSatisfiable (A Int) = Satisfied

(The wiki page was written before there were type families, so type class `ShowPred` has a Functional Dependency giving a type-level Boolean result.)
Your `C t` class becomes
class EitherSatisfied ( IsSatisfiable (A t)) ( IsSatisfiable (B t)) ~ Satisfied => C t where ...

----

Nowadays there's a better way: make Associated Types for the two classes, give them a default instance:

class A t where
type APred t
type instance APred t = Satisfied
...

class B t where
type BPred t
type instance BPred t = Satisfied
...

Now every instance defined for `A, B` in effect automatically gives you `APred, BPred` instances. Then

class EitherSatisifed (APred t) (BPred t) ~ Satisfied => C t where ...


AntC


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Clinton Mead
Hi Anthony

Perhaps I've misunderstood, but there's a few issues with the approaches you suggest:

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

I also tried the associated types approach you suggested towards the end of your email previously. This works perfectly fine if you can edit the base class, but I can't edit say, "Applicative" or "Num". I did something like the following, but I ran into a problem:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

data Satisfied

class Num t => MyNum t where
  type IsNum t
instance Num t => MyNum t where
  type IsNum t = Satisfied

data D = D

f :: IsNum t ~ Satisfied => t -> ()
f _ = ()

main = print $ f D

Ideally this should not compile, but unfortunately it happily compiles, showing that GHC generates an "IsNum" type family instance for "D", despite the fact that "Num D" is not satisfied. 

Any suggestions going forward from here?


On Mon, May 7, 2018 at 9:11 PM, Anthony Clayden <[hidden email]> wrote:
It's occurred to me that one could write a class C t which is satisfied
> whenever (A t) or (B t) is satisfied like so:

Hi Clinton, this sounds like you might want "Choosing a type-class instance based on the context"

> --- > > data Satisfied > > type family IsSatisfiable :: Constraint -> Type

That type family is doing the same job as auxiliary class `ShowPred` on that wiki page.

Rather than all the machinery you give for the disjunction, you could use another type family:

type family EitherSatisfied :: Type -> Type -> Type
instance EitherSatisfied Satisfied tb = Satisfied
instance EitherSatisfied ta Satisfied = Satisfied

Those two instances do overlap (as you expected); and they exhibit confluence, aka coincident overlap (they produce the same result); so that's fine.

But you haven't given any instances for `IsSatisfiable`. How do you expect to get from the Constraint to the `Satisfied` type?

You say

> IsSatisfiable c = Satisfied -- (if c is satisfiable)

What are you going to put for `c`? If you follow that wiki page, you'll need to in effect repeat every instance decl for classes `A, B`:

instance A Int where ...

type instance IsSatisfiable (A Int) = Satisfied

(The wiki page was written before there were type families, so type class `ShowPred` has a Functional Dependency giving a type-level Boolean result.)
Your `C t` class becomes
class EitherSatisfied ( IsSatisfiable (A t)) ( IsSatisfiable (B t)) ~ Satisfied => C t where ...

----

Nowadays there's a better way: make Associated Types for the two classes, give them a default instance:

class A t where
type APred t
type instance APred t = Satisfied
...

class B t where
type BPred t
type instance BPred t = Satisfied
...

Now every instance defined for `A, B` in effect automatically gives you `APred, BPred` instances. Then

class EitherSatisifed (APred t) (BPred t) ~ Satisfied => C t where ...


AntC


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Li-yao Xia-2
In reply to this post by Clinton Mead
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).

I'm not sure "unify" is the right term when talking about this behavior
of type families, but it's the one used in describing the instance
resolution algorithm ("find all instances that unify with the target
constraint"):
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances

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)


Regards,
Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Clinton Mead


On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <[hidden email]> 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"?
 
I'm not sure "unify" is the right term when talking about this behavior of type families, but it's the one used in describing the instance resolution algorithm ("find all instances that unify with the target constraint"): https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances

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. 
 

Regards,
Li-yao

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Brandon Allbery
In reply to this post by Clinton Mead
On Mon, May 7, 2018 at 7:50 AM, Clinton Mead <[hidden email]> wrote:
class Num t => MyNum t where
  type IsNum t
instance Num t => MyNum t where
  type IsNum t = Satisfied

This looks wrong to me: given how instance resolution works, I'd expect this to match every type and produce Satisfied, and later rejection based on the context wouldn't affect it. But I could well be thinking about it incorrectly.

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

David Kraeutmann

Correct. That instance won't work as expected.

On 5/7/2018 8:21 PM, Brandon Allbery wrote:
On Mon, May 7, 2018 at 7:50 AM, Clinton Mead <[hidden email]> wrote:
class Num t => MyNum t where
  type IsNum t
instance Num t => MyNum t where
  type IsNum t = Satisfied

This looks wrong to me: given how instance resolution works, I'd expect this to match every type and produce Satisfied, and later rejection based on the context wouldn't affect it. But I could well be thinking about it incorrectly.

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

AntC
In reply to this post by Clinton Mead

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead <[hidden email]> wrote:

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

Yes that approach does need declaring instances of `ShowPred` (or in general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`). That approach is making a closed world: for every type `t`, return either `True` or `False` that it has an instance for `Show`.

I'm not sure what you mean by "write them the normal way"? Just declaring `t` an instance of `Show` doesn't expose that in any way you can run type-level functions over it.


I also tried the associated types approach you suggested towards the end of your email previously. This works perfectly fine if you can edit the base class, but I can't edit say, "Applicative" or "Num".

Your O.P. talked about classes `A, B`, which I assumed you were writing fresh. What is your use case for wanting `EitherSatisfied (Applicative t) (Num t)` for the same `t`? (Those two classes want a `t` of different kind/arity, for one thing.)


I did something like the following, but I ran into a problem:

...
class Num t => MyNum t where
  type IsNum t
instance Num t => MyNum t where
  type IsNum t = Satisfied

No that won't work (as others have pointed out). That `MyNum t` instance makes every type an instance of `MyNum`, so `(IsNum t)` always returns `Satisfied`. And it'll always compile because the instance constraint `Num t` is ignored for associated types. (Note that an Assoc type is just syntactic sugar for a type family, and you can't put constraints on TF equations.)



Any suggestions going forward from here?

I'm puzzled what it is you're trying to do. Your O.P. on the cafe talked about satisfying one or both of two constraints. Neither that nor your StackOverflow original question 'Reducing satisfied constraints to ordinary types' mentioned you want to use this for `Prelude` classes. Which specific classes? There is a ghc extension coming along soon which supports some limited froms of implications over types and instances. I'm not going to suggest it until I know what you're trying to do.

I have a nervous feeling that you nurse incorrect expectations. This

instance Num t => MyNum t where

_does not_ say "if `t` is an instance of `Num`, it's thereby an instance of `MyNum`". It says "every `t` is an instance of `MyNum`; if I use some method from `MyNum` on some particular type `t0`, validate that also `Num t0`".

There's a deep reason why Haskell works like that. See my added note to the SO answer.

AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Clinton Mead


On Tue, May 8, 2018 at 11:17 AM, Anthony Clayden <[hidden email]> wrote:

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead <[hidden email]> wrote:

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

Yes that approach does need declaring instances of `ShowPred` (or in general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`). That approach is making a closed world: for every type `t`, return either `True` or `False` that it has an instance for `Show`.

I'm not sure what you mean by "write them the normal way"? Just declaring `t` an instance of `Show` doesn't expose that in any way you can run type-level functions over it.

By normal way as in if I need to list every instance as "ShowPred", I might as well just scrap "ShowPred" and just write them directly as instances of "Print". i.e.

instance Print Int where print = show
instance Print Char where print = show

Seems not much more work than:

instance ShowPred Int = HTrue
instance ShowPred Bool = HTrue
 
etc so why use "ShowPred" at all?

I'm puzzled what it is you're trying to do. 

I'm trying to select instances based on whether constraints are fulfilled. 

For example:

class Join m where
  join :: m (m a) -> m a

instance Monad m => Join m where
  join x = x >>= id

instance Comonad m => Join m where
  join = extract

Obviously I can't do this, but consider:

class Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
  join :: m (m a) -> m a

instance  Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
  join = join'

instance Monad m => Join' m Satisfied t2 where
  join' x = x >>= id

instance Comonad m => Join' m t1 Satisfied where
  join' = extract

instance Comonad m => Join' m Satisfied Satisfied where
  join' = extract

If I'm in a room, I can quite correctly assert things do exist if I can see them. But I can't assert things can't exist. Asserting things don't exist would violate the open world assumption, but only asserting when they do exist should not.

"IsSatisfied" only needs to assert when the constraint is satisfied, it doesn't need to assert when it isn't, so I don't think it violates the open world assumption. Also GHC has this information to give an answer to IsSatisfied, it simply has to try to solve the constraint and if it succeeds reduce it to Satisfied, and if it doesn't it just does nothing. I just need a way to entice GHC to do that. 

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Li-yao Xia-2
In reply to this post by Clinton Mead
Hi Clinton,

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

>
>
> On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <[hidden email]
> <mailto:[hidden email]>> 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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email] <mailto:[hidden email]>> 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


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Brandon Allbery
On Mon, May 7, 2018 at 11:45 PM, Clinton Mead <[hidden email]> wrote:
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.

Int can be verified as more specific than "matches any type". Two instance heads differing *only* in context cannot.

--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Clinton Mead


Int can be verified as more specific than "matches any type". Two instance heads differing *only* in context cannot.


I realise this, but the instances heads I proposed also don't only differ in context. 

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

AntC
In reply to this post by Clinton Mead

On Tue, 8 May 2018 at 2:00 PM, Clinton Mead <[hidden email]> wrote:
On Tue, May 8, 2018 at 11:17 AM, Anthony Clayden <[hidden email]> wrote:

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead <[hidden email]> wrote:

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

Yes that approach does need declaring instances of `ShowPred` (or in general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`). That approach is making a closed world: for every type `t`, return either `True` or `False` that it has an instance for `Show`.

I'm not sure what you mean by "write them the normal way"? Just declaring `t` an instance of `Show` doesn't expose that in any way you can run type-level functions over it.

By normal way as in if I need to list every instance as "ShowPred", I might as well just scrap "ShowPred" and just write them directly as instances of "Print". i.e.

No you haven't got it: there's a default/fallback instance for `Print` that applies if `ShowPred` comes out `False`. Also if you have `True/False` you can do Boolean logic over the result:

type instance ShowPred [a] = ShowPred a                                              -- implication
type instance ShowPred (a, b) = And (ShowPred a) (ShowPred b)       -- conjunction

including either/or logic, which is where your O.P. started. (Although we seem to have come a long way from that.) So turning to your latest example ...


I'm puzzled what it is you're trying to do. 

I'm trying to select instances based on whether constraints are fulfilled. 

... consider:

class Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
  join :: m (m a) -> m a

instance  Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
  join = join'

?? I think that context needs something like

instance Join' m (IsMonad m) (IsComonad m) => Join m where ...


instance Monad m => Join' m Satisfied t2 where
  join' x = x >>= id

instance Comonad m => Join' m t1 Satisfied where
  join' = extract

instance Comonad m => Join' m Satisfied Satisfied where
  join' = extract

So if some `m0` is both a `Comonad` and a `Monad`, you want to prefer the `Comonad` method. If `m0` is a `Monad` but not a `Comonad`, use the `Monad` method.

You've just invoked a closed world: you're relying on the compiler determining some `m0` is _not_ a `Comonad`.

Technically: your instances for `Join'` overlap. So the compiler's inference selection must determine which is the more specific, given some particular `m0` with its `t1, t2` result from `IsSatisfied`. It can select head `Join' m Satisfied t2` only if it can prove `t2` is apart from `Satisfied`. 

...

"IsSatisfied" only needs to assert when the constraint is satisfied, it doesn't need to assert when it isn't, ...

Yes it does for what you're asking to do.


so I don't think it violates the open world assumption. Also GHC has this information to give an answer to IsSatisfied, it simply has to try to solve the constraint and if it succeeds reduce it to Satisfied, and if it doesn't it just does nothing.

To the contrary: what you want it to do is select a different instance.


AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Li-yao Xia-2
In reply to this post by Clinton Mead
On 05/07/2018 11:45 PM, Clinton Mead wrote:

> 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.
>
No instance for the C type class above will be picked until x is equal
to some applied type constructor; it will be more challenging to break
coherence with that than using what you're proposing.

It seems difficult to make a clear point because the whole topic of
coherence with Haskell type classes is already a minefield.

Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

Oliver Charles-3
I've only skimmed the thread, so sorry if this is a red herring, but could this be helpful? https://github.com/rampion/constraint-unions/blob/master/README.md

On Tue, May 8, 2018 at 12:49 PM, Li-yao Xia <[hidden email]> wrote:
On 05/07/2018 11:45 PM, Clinton Mead wrote:
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.

No instance for the C type class above will be picked until x is equal to some applied type constructor; it will be more challenging to break coherence with that than using what you're proposing.

It seems difficult to make a clear point because the whole topic of coherence with Haskell type classes is already a minefield.


Li-yao
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

David Feuer
Maybe look at https://www.reddit.com/r/haskell/comments/6k86je/constraint_unions_bringing_or_to_the_language_of/
(relating to the repository Oliver links to) and note also Edward
Kmett's response.

On Tue, May 8, 2018 at 9:52 AM, Oliver Charles <[hidden email]> wrote:

> I've only skimmed the thread, so sorry if this is a red herring, but could
> this be helpful?
> https://github.com/rampion/constraint-unions/blob/master/README.md
>
> On Tue, May 8, 2018 at 12:49 PM, Li-yao Xia <[hidden email]> wrote:
>>
>> On 05/07/2018 11:45 PM, Clinton Mead wrote:
>>>
>>> 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.
>>>
>> No instance for the C type class above will be picked until x is equal to
>> some applied type constructor; it will be more challenging to break
>> coherence with that than using what you're proposing.
>>
>> It seems difficult to make a clear point because the whole topic of
>> coherence with Haskell type classes is already a minefield.
>>
>>
>> Li-yao
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to expose if a constraint is satisfiable

AntC
In reply to this post by Clinton Mead
Thanks David, Oliver, I'll leave it so Clinton whether that helps his use case.

I see the write-ups for both the Constraint Unions package and ifCxt mentioned on the reddit thread talk about needing large amounts of boilerplate. That is, an instance for each class and type that effectively tells the class has an instance for that type. So that's the same as the AdvancedOverlap I linked to -- from Oleg + SPJ.

IIUC, what Clinton's asking is: since there are already instances for `Show Int`, `Ord Float`, etc (declared in the Prelude), why can't ghc 'just know' that and expose it to type-level logic that can say: if there's `Show a` do this, otherwise do that?


AntC
> On Tue May 8 22:29:20 UTC 2018, David Feuer wrote:
> Maybe look at https://www.reddit.com/r/haskell/comments/6k86je/constraint_unions_bringing_or_to_the_language_of/
> (relating to the repository Oliver links to) and note also Edward Kmett's response.

Eurrm. Could somebody explain that response using familiar language. I think the `:-` operator might be referring to Edward's & David's 'constraints' package on github, for which I've asked if there's human-facing documentation.
Also asked if it'll be superseded by the 'Qualified Constraints' new development.

>> On Tue, May 8, 2018 at 9:52 AM, Oliver Charles <ollie at ocharles.org.uk> wrote:
>> I've only skimmed the thread, so sorry if this is a red herring, but could
>> this be helpful?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.