Автоматическое получение ограничений класса типов с помощью GADT

Я пишу библиотеку для работы с бесконечными последовательностями, используя ленивую оценку. Для краткости я использую обобщенные алгебраические типы данных (GADT), чтобы установить ограничение Ord для индекса каждого термина в последовательности. Отсюда следующие проверки типов:

{-# LANGUAGE GADTs #-}

data Term ix cff where
  Term :: (Ord ix) => ix -> cff -> Term ix cff

data Sequence ix cff where
  Seq :: [Term ix cff] -> Sequence ix cff

f (Seq (Term i x:_)) (Seq (Term j y:_)) = i < j

{-
add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (ix -> ix -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []
-}

Как и ожидалось, GHCi сообщает мне, что f :: Sequence t t1 -> Sequence t t2 -> Bool. Для сравнения i < j требуется экземпляр Ord, но об этом заботится ограничение (Ord ix) в определении Term.

Однако, когда нижний блок раскомментирован, функция add не проходит проверку типов с ошибкой No instance for (Ord ix) arising from the use of ``<''. Разве он не должен вычислить (Ord ix) из Term ix cff, которое появляется в определении Sequence?


types type-inference haskell algebraic-data-types gadt
person Herng Yi    schedule 05.07.2016    source источник

Ответы (1)


arrow_upward
6
arrow_downward

Термы, связанные с аргументом функции, по умолчанию мономорфны (т. е. полиморфны ранга 0), потому что Haskell98 поддерживает полиморфизм только ранга 1, а полиморфный аргумент делает функцию полиморфной ранга 2.

Следовательно, в Seq (addAlong (<) tms1 tms2) компилятор может рассматривать только < как мономорфное сравнение жесткого типа ix. Чтобы рассматривать < как мономорфную функцию, компилятору необходимо разрешить экземпляр Ord. Однако в этот момент экземпляр Ord ix недоступен, так как он может быть сопоставлен только из Term!

Решение, наиболее близкое к вашему исходному коду, состоит в том, чтобы явно сделать полиморфным addAlong rank-2:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (∀ ix' . Ord ix' -> ix' -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []

Таким образом, < просто передается как есть (как полиморфный метод Ord => ...), поэтому компилятору не нужно иметь экземпляр, доступный в Seq (addAlong (<) tms1 tms2), но он может разрешить его позже, когда у вас будут доступны Term.

Вы, конечно, должны подумать, действительно ли вам это нужно. Хранение словаря Ord в каждом Term кажется мне довольно расточительным — проблема не возникла бы, если бы вместо этого вы сохранили ограничение в Seq:

data Term ix cff where Term :: ix -> cff -> Term ix cff

data Sequence ix cff where
  Seq :: Ord ix => [Term ix cff] -> Sequence ix cff

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (ix -> ix -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []
person leftaroundabout    schedule 05.07.2016
comment
В первом add, я думаю, ∀ ix' . ix' -> ix' -> Bool должно быть ∀ ix' . Ord ix' => ix' -> ix' -> Bool. Кроме того, второй add должен требовать ScopedTypeVariables и add :: forall ix. ..., иначе ix в addAlong :: (ix -> ... не совпадает. - person chi; 05.07.2016