[Haskell-cafe] Data.Ord and Heaps (Was: Why functional programming matters)

[Roberto Zunino]

(Sorry for the late reply.)

apfelmus at quantentunnel.de 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.

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.

Then, we reify the Ord class with a GADT:

   data O a where O :: Ord a => O a

Then, we reify the forall, using GADT+impredicativity:

   data O1 p where O1:: (forall a . Ord a => O (p a)) -> O1 p

We can express the constraint with a class OrdAll, providing the GADT proof:

   class OrdAll p where
       ordAll :: O1 p

Instances are easy to define, I think:

   instance OrdAll [] where
       ordAll = O1 O

Your class becomes then:

   class OrdAll p => OrdPolicy p where ...

Actually, using this is not exactly nice, since you have to 
'instantiate' the forall on your own. For example,

fooSort :: forall p a . (OrdPolicy p, Ord a) => [p a] -> [p a]
fooSort = case ordAll of
                   O1 o -> case o of
                             (O :: O (p a)) -> sort

* * *

Actually, a simpler (untested) approach could be:

    class OrdAll p where
       ordAll :: Ord a => O (p a)

This would make the O1 hack useless.

Regards,
Zun.