[Haskell-cafe] in-equality type constraint?
Ryan Ingram
ryani.spam at gmail.com
Fri Jul 16 19:33:31 EDT 2010
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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
More information about the Haskell-Cafe
mailing list