Converting an arbitrary class constraint `C a` into `C a Bool`

Question

So there are many advantages of having typeclasses in C a Bool form. Mostly because they let you do any logical operation between two constraints when the normal C a just implicitly ANDs everything.

If we consider ~ a class constraint, this can be done like so

class Equal x y b | x y -> b
instance Equal x x True
instance False ~ b => Equal x y b

But what makes this case special is the fact that putting x x in the head of the instance is equivalent to x ~ y => and then x y in the head. This is not the case for any other typeclass. So if we try to do something similar for a class C we get something like

class C' x b | x -> b
instance C x => C' x True
instance False ~ Bool => C' x b

Unfortunately this doesn't work since only one of those instances will ever be picked because they don't discriminate on the type x so any type matches both heads.

I've also read https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap which again doesn't apply for any class C because it requires you to rewrite all the instances of the original class. Ideally, I'd like my code to work with GHC.Exts.Constraint and KindSignatures so that C can be parametric.

So, for a class like this

class Match (c :: * -> Constraint) x b | c x -> b

How do I write the instances so that Match c x True if and only if c x, Match c x False otherwise?

The C a Bool form is stronger than C a. You are essentially asking how to collect the set of instances of a type class, which is impossible. — user2407038
@user2407038 Not that I'm doubting you but I have heard 'impossible' with regards to the type system before and it turned out to be false. — Luka Horvat
I don't know if I can make a convincing argument, but I will try. Suppose you have written Match. In module A I define data X = X, and class A b x | b -> x; a :: Proxy b -> x; instance A True Int; instance A False Bool, test :: forall x b y . (Match Eq x b, A b y) => x -> y; test _ = a (Proxy :: Proxy b). I have module B (imports A), in which the type of test X must be Int. In module C (import A) I have instance Eq X so test X :: Bool. Module D imports B and C. Module D can't can't force B and C to recompile, so test X must paradoxically have two types at once. — user2407038
By default the compiler only accepts instances it can prove will not cause non-termination. UndecidableInstances simple removes this restriction (applies to type families as well). Such an extension would essentially eliminate module boundaries - each module would have to know about each other module. Fairly non-trivial, I imagine, to implement. Even if it existed, it wouldn't give you the ability to write the desired class - there still is not a mechanism for "reify the constraint C to a value". — user2407038

bennofs bennofs · Accepted Answer · 2015-02-13T23:51:04

This is impossible in Haskell due to the so-called Open World Assumption. It states that the set of instances for typeclasses is open, which means that you can make new instances any time (as opposed to a closed world, where there must be a fixed set of instances). For example, while the Functor typeclass is defined in the Prelude, I can still make instances for it in my own code which is not in the Prelude.

To implement what you've proposed, the compiler would need a way to check whether a type T is an instance of a class C. This, however, requires that the compiler knows all the possible instances of that class and that is not possible because of the open world assumption (while compiling the Prelude, a compiler can't yet know that you later make YourOwnFunctor an instance of Functor too).

The only way to make it work would be to only consider the instances that are currently visible (because they were defined in the current module or any of its imports). But that would lead to quite unpredictable behaviour: the set of visible instances depends not only on the imports of the module, but also on the imports of the imports since you cannot hide instances. So the behaviour of your code would depend on implementation details of your dependencies.

If you want a closed world, you can instead use closed type families, which were introduced in GHC 7.8. Using them, you can write:

type family Equal a b :: Bool where
  Equal x x = True
  Equal x y = False

Converting an arbitrary class constraint `C a` into `C a Bool`

1 Answers