GHC rewrite rule specialising a function for a type class

Question

Using the GHC RULES pragma, it is possible to specialise a polymorphic function for specific types. Example from the Haskell report:

genericLookup :: Ord a => Table a b   -> a   -> b
intLookup     ::          Table Int b -> Int -> b

{-# RULES "genericLookup/Int" genericLookup = intLookup #-}

This would make GHC use intLookup on an integer-indexed table and the generic version otherwise, where intLookup would probably be more efficient.

I would like to accomplish something similar, using functions like the following (slightly simplified) ones:

lookup    :: Eq a  => [(a, b)] -> a -> b
lookupOrd :: Ord a => [(a, b)] -> a -> b

where lookupOrd creates a Map from the input list and then uses Map.lookup, which requires that a be a member of Ord.

Now I would like to tell GHC that lookupOrd should be used instead of lookup whenever a is indeed a member of the Ord type class. The following rule, however, does not typecheck:

{-# RULES "lookup/Ord" lookup = lookupOrd #-}

GHC (rightfully) complains that it cannot deduce (Ord a) from the context (Eq a). Is there a rewrite rule that would allow me to perform this sort of type class-based specialisation?

Confocal

That's pretty much running into the old open-world problem: you're trying to make a decision based on whether or not a type is in some type class. But Haskell has no notion of not being in a type class! It is always assumed that any type might be in any class (even if no such instance has been encountered yet, someone might still add it later). – Incongruous

@Incongruous that problem is not too severe; a best-effort approach to applying such a rule could be imagined (if GHC would support it in the first place). – Solid

Answer 1

While this is an old question, future Google'ers might be interested in knowing that there is a way to do what the OP wanted, using the ifcxt package.

You can check out the documentation for more examples, but basically you would use the second example, Example 2: make your code asymptotically efficient, as the basis.

With the two functions,

lookup    :: Eq a  => [(a, b)] -> a -> b
lookupOrd :: Ord a => [(a, b)] -> a -> b

You would make,

cxtLookup :: forall a. (Eq a, IfCxt (Ord a)) => [(a, b)] -> a -> b
cxtLookup = ifCxt (Proxy::Proxy (Ord a)) lookupOrd lookup

Which will allow you to choose the most effective function depending on which typeclasses your data structure implements.

Note, that I don't know how much it'll affect the performance, but I imagine it being trivial compared to the runtime of the lookup functions, and therefore indeed be worth it.

Angeli

Answer 2

I don’t think there is, and there is a reason why it is not easily possible with GHC’s current implementation:

Although you specify rules in Haskell syntax, they are going to be applied to GHC’s Core language. There, type class constraints have been turned into dictionary arguments, so the function

lookup :: Eq a => a -> [(a,b)] -> Maybe b

has now type

lookup :: forall a b. Eq a -> a -> [(a, b)] -> Maybe b

while your lookupOrd would have type

lookupOrd :: forall a b. Ord a -> a -> [(a, b)] -> Maybe b

where Eq a and Ord a have become ordinary data types. In particular, at this stage, there is no notion of the type class for a type any more; all that has been resolved earlier.

So now assume the compiler finds an occurrence of

lookup (dict :: Eq MyType) (x :: MyType) (list :: [(MyType, String)])

What should it replace it with? You told him that x and list can be passed to lookupOrd as well, but that function also wants a value of type Ord MyType, which does not occur on the left-hand side of the rule. So GHC has to give up.

A rule like

{-# RULES "lookup/Ord" forall a x. lookup a x = lookupOrd (a::()) x #-}

works, though, as here the problematic argument (the Ord dictionary) is already fixed in the rule, and does not need to be found when applying the rule.

In principal, other compiler designs might allow rules of the form that you want.

Solid

GHC 8.0.1 doesn't complain if you write {-# RULES "lookup/Ord" forall (e :: Ord k => k) (l :: [(k,a)]) . lookup e l = lookupOrd e l #-}, but the rule doesn't seem to actually fire. – Brave

Both this and specialization in the face of GADTs might become tractable if GHC were to hold on to its instance resolution machinery after type checking. – Lisette