CODEWITHSUNDEEP
haskelltype-inferencetype-systems
plc
plc

Reputation: 944

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

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.

Upvotes: 25

Views: 3324

Answers (4)

esp
esp

Reputation: 7687

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

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

Upvotes: 3

chessai
chessai

Reputation: 126

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.

Upvotes: 1

Boldizs&#225;r N&#233;meth
Boldizs&#225;r N&#233;meth

Reputation: 1847

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

Upvotes: 11

C. A. McCann
C. A. McCann

Reputation: 77404

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'
    (...)

Upvotes: 27

Related Questions