I was wondering this. I was recently able to write some code for negation of type equality, using the encoding "Not p" == "p -> forall a. a" But it doesn't generalize; you need to create a witness of inequality for every pair of types you care about. {-# LANGUAGE RankNTypes, TypeFamillies, ExistentialQuantification #-} module NotEq where data TypeEqual a b = (a ~ b) => Refl newtype Void = Void { voidElim :: forall a. a } type Not p = (p -> Void) data family IntVsBool a newtype instance IntVsBool Int = OK () newtype instance IntVsBool Bool = NotOK Void liftEq :: TypeEqual a b -> TypeEqual (f a) (f b) liftEq Refl = Refl cast :: TypeEqual a b -> a -> b cast Refl = id int_neq_bool :: Not (TypeEqual Int Bool) int_neq_bool = \int_eq_bool -> case (cast (liftEq int_eq_bool) (OK ())) of (NotOK v) -> v On Fri, Jul 16, 2010 at 4:08 PM, Paul L <ninegua@gmail.com> wrote:
Does anybody know why the type families only supports equality test like a ~ b, but not its negation?
-- Regards, Paul Liu
Yale Haskell Group http://www.haskell.org/yale _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe