Could you write a type function to invert a constraint?

Question

Is it possible to write a type function that would take a constraint like Show and return one that constrains the RHS to types that are not an instance of Show?

The signature would be something like

type family Invert (c :: * -> Constraint) :: * -> Constraint

The answer is almost certainly "no". Can you explain what it is you're trying to use this for? — K. A. Buhr, Aug 05 '19 at 02:04
https://www.microsoft.com/en-us/research/publication/fun-type-functions/ shows a way to get a type-level predicate telling whether some type is a member of some class. By the time you've waded through that, you'll agree with "almost certainly 'no'". Consider the general problem: some type is a member of class `D` just in case it's _not_ a member of `C`. It's a member of `C` just in case it's not a member of `D`. (Of course it won't be as simple as that: there'll be a chain of inter-dependent class constraints.) The base problem is that constructivist logic can't use the law of excluded middle. — AntC, Aug 05 '19 at 04:49
To support incremental compilation, GHC can never be sure that a given instance does _not_ exist. Checking that negative constraint would require inspecting all the modules, breaking incremental compilation. — chi, Aug 05 '19 at 06:58
I'd also remark that the inability to negate constraints relates to a rather deep mathematical idiom, that of [constructive logic](https://en.wikipedia.org/wiki/Intuitionistic_logic). It turns out it's often a really good idea to avoid classical binary _true or false_ thinking. — leftaroundabout, Aug 05 '19 at 10:19

score 10 · Answer 1 · answered Aug 05 '19 at 06:18

No. It is a design principle of the language that you are never allowed to do this. The rule is if a program is valid, adding more instances should not break it. This is the open-world assumption. Your desired constraint is a pretty direct violation:

data A = A
f :: Invert Show a => a -> [a]
f x = [x]
test :: [A]
test = f A

Would work, but adding

instance Show A

would break it. Therefore, the original program should never have been valid in the first place, and therefore Invert cannot exist.

score 3 · Answer 2 · answered Aug 05 '19 at 11:03

As HTNW answered, it is in general not supposed to be possible to assert that a type is not an instance of a class. However, it is certainly possible to assert for a concrete type that it's never supposed to be possible to have an instance of some class for it. An ad-hoc way would be this:

{-# LANGUAGE ConstraintKinds, KindSignatures, AllowAmbiguousTypes
           , MultiParamTypeClasses, FlexibleInstances #-}

import GHC.Exts (Constraint)

class Non (c :: * -> Constraint) (t :: *) where
  nonAbsurd :: c t => r

But this is unsafe – the only way to write an instance is, like,

instance Non Show (String->Bool) where
  nonAbsurd = undefined

but then somebody else could come up with a bogus instance Show (String->Bool) and would then be able to use your nonAbsurd for proving the moon is made out of green cheese.

A better option to make an instance impossible is to “block” it: write that instance yourself “pre-emptively”, but in such a way that it's a type error to actually invoke it.

import Data.Constraint.Trivial -- from trivial-constraint

instance Impossible0 => Show (String->Bool) where
  show = nope

Now if anybody tries to add that instance, or tries to use it, they'll get a clear compiler error.

Could you write a type function to invert a constraint?

2 Answers2