Roberto Zunino wrote:
I'd really like to write
class (forall a . Ord p a) => OrdPolicy p where
but I guess that's (currently) not possible.
Actually, it seems that something like this can be achieved, at some price.
data O a where O :: Ord a => O a
data O1 p where O1:: (forall a . Ord a => O (p a)) -> O1 p
Ah, very nice :)
First, I change the statement ;-) to
class (forall a . Ord a => Ord p a) => OrdPolicy p
since I guess this is what you really want.
Right, modulo the fact that I also forgot the parenthesis class (forall a . Ord a => Ord (p a)) => OrdPolicy p So, the intention is to automatically have the instance instance (OrdPolicy p, Ord a) => Ord (p a) where which can be obtained from your GADT proof compare = case ordAll of O1 o -> case o of (O :: O (p a)) -> compare This instance declaration is a bit problematic because it contains only type variables. Fortunately, the phantom type approach doesn't have this problem: data OrdBy p a = OrdBy { unOrdBy :: a } data O a where O :: Ord a => O a class OrdPolicy p where -- simplified O1 ordAll :: Ord a => O (OrdBy p a) instance (Ord a, OrdPolicy p) => Ord (OrdBy p a) where compare = case ordAll of { (O :: O (OrdBy p a)) -> compare } By making the dictionary in O explicit, we can even make this Haskell98! class OrdPolicy p where compare' :: Ord a => OrdBy p a -> OrdBy p a -> Ordering instance (Ord a, OrdPolicy p) => Ord (OrdBy p a) where compare = compare' On second thought, being polymorphic in a is probably too restrictive: the only usable OrdPolicy besides the identity is Reverse :) After all, there aren't so many useful functions with type compare' :: forall a. (a -> a -> Ordering) -> (a -> a -> Ordering) So, other custom orderings usually depend on the type a . Did you have any specific examples in mind, Stephan? At the moment, I can only think of ordering Maybe a such that Nothing is either the largest or the smallest element on f g x y = g x `f` g y data Up instance Ord a => Ord (OrdBy Up (Maybe a)) where compare = f `on` unOrdBy where f Nothing Nothing = EQ f x Nothing = LT f Nothing y = GT f (Just x) (Just y) = compare x y data Down instance Ord a => Ord (OrdBy Down (Maybe a)) where compare = f `on` unOrdBy where f Nothing Nothing = EQ f x Nothing = GT f Nothing y = LT f (Just x) (Just y) = compare x y But I think that those two orderings merit special data types like data Raised a = Bottom | Raise a deriving (Eq, Ord) data Lowered a = Lower a | Top deriving (Eq, Ord) instead of type Raised a = OrdBy Down (Maybe a) type Lowered a = OrdBy Up (Maybe a) Regards, apfelmus