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
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