Simplifying a IsFunction type class using type equality constraints
I recently had a need to use the IsFunction typeclass described by Oleg here: http://okmij.org/ftp/Haskell/isFunction.lhs and am wondering if the use of the TypeCast class can be correctly replaced by a type equality constraint. The IsFunction and TypeCast classes were defined as:
data HTrue data HFalse
class IsFunction a b | a -> b instance TypeCast f HTrue => IsFunction (x->y) f instance TypeCast f HFalse => IsFunction a f
-- literally lifted from the HList library class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x
I found the use of TypeCast in the IsFunction could be replaced by a type family:
class IsFunction a b | a -> b instance (f ~ TTrue) => IsFunction (x->y) f instance (f ~ TFalse) => IsFunction a f
Which, to me, is easier to understand and appears to function the same. The type equality is a stronger (?) constraint than the TypeCast class, but for the case of IsFunction the use of type equality is correct. Am I correct? Is the second definition of IsFunction actually equivalent to the original? Cheers, -Corey O'Connor
On Sat, Oct 4, 2008 at 2:58 AM, Corey O'Connor
I recently had a need to use the IsFunction typeclass described by Oleg here: http://okmij.org/ftp/Haskell/isFunction.lhs
and am wondering if the use of the TypeCast class can be correctly replaced by a type equality constraint.
I noticed this as well; it seemed to work in my tests, although I haven't seen any proof that they are equivalent. The HList paper mentions that the behavior of TypeCast is directly related to type equality coercions in System F(C), GHC's core language. So it's not that surprising that it can be replaced with a type-equality constraint, which is a more direct way of introducing the same core-language code. If you want to know for sure, you can look at the output of ghc -ddump-simpl on each program. -- ryan
Corey O'Connor:
I recently had a need to use the IsFunction typeclass described by Oleg here: http://okmij.org/ftp/Haskell/isFunction.lhs
and am wondering if the use of the TypeCast class can be correctly replaced by a type equality constraint.
The IsFunction and TypeCast classes were defined as:
data HTrue data HFalse
class IsFunction a b | a -> b instance TypeCast f HTrue => IsFunction (x->y) f instance TypeCast f HFalse => IsFunction a f
-- literally lifted from the HList library class TypeCast a b | a -> b, b->a where typeCast :: a -> b class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t-
a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t- a->b instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x = x
I found the use of TypeCast in the IsFunction could be replaced by a type family:
class IsFunction a b | a -> b instance (f ~ TTrue) => IsFunction (x->y) f instance (f ~ TFalse) => IsFunction a f
Yes, that's a fine way of simplifying the definition. In fact, you should also be able to drop the functional dependency in the IsFunction class. Manuel
participants (3)
-
Corey O'Connor -
Manuel M T Chakravarty -
Ryan Ingram