Is it possible to place inequality constraints on haskell type variables?

Question

Is it possible to place an inequality constraint on the typevariables of a function, à la foo :: (a ~ b) => a -> b as in GHC type family docs, except inequality rather than equality?

I realise that there is possibly no direct way to do this (as the ghc docs doesn't list any to my knowledge), but I would be almost puzzled if this weren't in some way possible in light of all the exotic type-fu I have been exposed to.

Britten

For which usecase, do you think, would an inequality constraint be useful? – Clarke

Specifically, I'm trying to model quantities of goods, i.e. numbers with a tag, for example enabling you to express the notion of having 10 apples and 2 pears, and provoking a type error if you want to add pears and apples. That in itself is simple enough. Where I fell short however, is when trying to define a price of one good in terms of another, e.g. 2 apples per pear.. Naturally, a price only makes sense if the type of goods being sold is different from the type of goods being bought.. (At least in my head). So, out of curiosity I just wondered if it was in fact possible to express this :) – Britten

My suspicion is that, while it may be silly, the price is well-defined (1 for 1, obviously), so it's probably not worth the hassle of trying to put a static requirement on the types being different. – Antihistamine

I have a use case :) I'm trying to model lists of two alternating types [a,b,a,b,a] where the type of the last element is statically known. That allows to write a type-safe last function over the lists that have the same type for first and last element, because the compiler could rule out the Nil case as having an incompatible type, only if types a and b are different. – Janitress

Answer 1

First, keep in mind that distinct type variables are already non-unifiable within their scope--e.g., if you have \x y -> x, giving it the type signature a -> b -> c will produce an error about not being able to match rigid type variables. So this would only apply to anything calling the function, preventing it from using an otherwise simple polymorphic function in a way that would make two types equal. It would work something like this, I assume:

const' :: (a ~/~ b) => a -> b -> a
const' x _ = x

foo :: Bool
foo = const' True False -- this would be a type error

Personally I doubt this would really be useful--the independence of type variables already prevents generic functions from collapsing to something trivial, knowing two types are unequal doesn't actually let you do anything interesting (unlike equality, which lets you coerce between the two types), and such things being declarative rather than conditional means that you couldn't use it to distinguish between equal/unequal as part of some sort of specialization technique.

So, if you have some specific use in mind where you want this, I'd suggest trying a different approach.

On the other hand, if you just want to play with ridiculous type-hackery...

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

-- The following code is my own hacked modifications to Oleg's original TypeEq. Note
-- that his TypeCast class is no longer needed, being basically equivalent to ~.

data Yes = Yes deriving (Show)
data No = No deriving (Show)

class (TypeEq x y No) => (:/~) x y
instance (TypeEq x y No) => (:/~) x y

class (TypeEq' () x y b) => TypeEq x y b where
    typeEq :: x -> y -> b
    maybeCast :: x -> Maybe y

instance (TypeEq' () x y b) => TypeEq x y b where
    typeEq x y = typeEq' () x y
    maybeCast x = maybeCast' () x

class TypeEq' q x y b | q x y -> b where
    typeEq' :: q -> x -> y -> b
    maybeCast' :: q -> x -> Maybe y

instance (b ~ Yes) => TypeEq' () x x b where
    typeEq' () _ _ = Yes
    maybeCast' _ x = Just x

instance (b ~ No) => TypeEq' q x y b where
    typeEq' _ _ _ = No
    maybeCast' _ _ = Nothing

const' :: (a :/~ b) => a -> b -> a
const' x _ = x

Well, that was incredibly silly. Works, though:

> const' True ()
True
> const' True False

<interactive>:0:1:
    Couldn't match type `No' with `Yes'
    (...)

Antihistamine

Thank you for a very elaborate answer -- exactly the kind of thing to satisfy my curiosity :-) .. And sorry for not motivating my question - I've elaborated on my mind in a comment to the question :-) – Britten

Note to readers: the class functions (typeEq, maybeCast, etc.) are irrelevant to the example and can be ignored / deleted. – Venule

Are you sure this works? while const' True () seems to work ok, const' 2 () is returning an error, as well as const' 'a' 8. I am using ghc 7.4.1 – Barbecue

@tohava: It certainly worked in whatever GHC version I was using at the time, probably a 7.0 release, and nonsense like this breaking on newer GHCs would not surprise me at all. That said, it will definitely fail on polymorphic arguments like numeric literals. Try const' (2 :: Int) () instead. That is one (of many) reasons why silly tricks like this aren't worth the effort. – Antihistamine

Answer 2

From GHC 7.8.1. closed type families are available. The solution is much simpler with them:

data True
data False

type family TypeEqF a b where
  TypeEqF a a = True
  TypeEqF a b = False

type TypeNeq a b = TypeEqF a b ~ False

Cano

I'm trying to use this technique to disambiguate overlapping typeclass instances, but can't seem to get it to work. See #38549674 – Vesuvius

Answer 3

Now one can use == from Data.Type.Equality (or from singletons library) with DataKinds extension:

foo :: (a == b) ~ 'False => a -> b

Isallobar

Note that == itself is just a simple closed type family and not a new language feature that enables one to break new ground. hackage.haskell.org/package/base-4.19.0.0/docs/src/… – Wakeless

Answer 4

Improving on Boldizsar's answer, which is itself an improvement of the accepted answer:

{-# language DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))

data Foo = Foo

data Bar = Bar

notBar :: Neq Bar a => a -> ()
notBar _ = ()

type family Neq a b :: Constraint where
  Neq a a = TypeError
    ( 'Text "Expected a type that wasn't "
    ':<>: 'ShowType a
    ':<>: 'Text "!"
    )
  Neq _ _ = ()

*Main> notBar Foo
()
*Main> notBar Bar

<interactive>:12:1: error:
    • Expected a type that wasn't Bar!
    • In the expression: notBar Bar
      In an equation for ‘it’: it = notBar Bar

The type errors for this are good, and it is very readable.

Phocaea