[Haskell-cafe] Re: Data.Ord and Heaps

[apfelmus]

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