Menu
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.
773
An inequality constraint g(x, y) ≤ b is called binding (or active) at a point. (x, y) if g(x, y) = b and not binding (or inactive) if g(x, y) < b.
Constraint families allow constraints to be indexed by a type in the same way that type families and data families allow types to be indexed by types. For example, constraint families let us define a generalized version of the Monad class where we can impose some constraints on the element it can contain.
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' (...) If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
