Правило перезаписи GHC, специализирующееся на функции для класса типа

Используя GHC RULES прагма, можно специализировать полиморфную функцию для определенных типов. Пример из отчета Haskell:

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

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

Это приведет к тому, что GHC будет использовать intLookup в таблице с индексом целых чисел и в общей версии, где intLookup, вероятно, будет более эффективным.

Я хотел бы выполнить нечто подобное, используя следующие функции (несколько упрощенные):

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

где lookupOrd создает Map из списка ввода, а затем использует Map.lookup, для чего a является членом Ord.

Теперь я хотел бы сказать GHC, что lookupOrd следует использовать вместо lookup, когда a действительно является членом класса типа Ord. Однако следующее правило не проверяет тип:

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

GHC (по праву) жалуется, что он не может вывести (Ord a) из контекста (Eq a). Есть ли правило перезаписи, которое позволило бы мне выполнить такую специализацию на основе класса?

Ответ 1

Я не думаю, что есть, и есть причина, почему это нелегко с текущей реализацией GHC:

Хотя вы указываете правила в синтаксисе Haskell, они будут применяться к основному языку GHCs. Там, типы ограничений класса были превращены в словарные аргументы, поэтому функция

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

теперь имеет тип

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

в то время как ваш lookupOrd будет иметь тип

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

где Eq a и Ord a стали обычными типами данных. В частности, на этом этапе уже нет понятия типа-типа для типа; все, что было разрешено ранее.

Итак, теперь предположим, что компилятор обнаруживает появление

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

Что он должен заменить? Вы сказали ему, что x и list также могут быть переданы в lookupOrd, но эта функция также хочет значение типа Ord MyType, которое не встречается в левой части правила. Поэтому GHC должен отказаться.

Правило вроде

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

работает, хотя, как здесь, в правиле уже исправлен проблематичный аргумент (словарь Ord), и при применении правила его не нужно искать.

В принципе, другие конструкции компилятора могут разрешать правила формы, которые вы хотите.

Ответ 2

Хотя это старый вопрос, будущие пользователи Google могут быть заинтересованы в том, чтобы знать, что есть способ сделать то, что хотел OP, используя ifcxt.

Вы можете проверить документацию для большего количества примеров, но в основном вы использовали бы второй пример, пример 2: сделать свой код асимптотически эффективным в качестве основы.

С помощью двух функций

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

Вы сделали бы,

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

Это позволит вам выбрать наиболее эффективную функцию, зависящую от того, какие типы стеков реализует ваша структура данных.

Заметьте, что я не знаю, насколько это повлияет на производительность, но я полагаю, что это тривиально по сравнению с временем выполнения функций поиска, и поэтому действительно стоит того.