[Haskell-cafe] Data.Ord and Heaps (Was: Why functional programming
matters)
Roberto Zunino
zunino at di.unipi.it
Tue Feb 5 10:07:40 EST 2008
(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.
More information about the Haskell-Cafe
mailing list