Неоднозначный тип с использованием явных квантификаторов - PullRequest
2 голосов
/ 02 декабря 2011

Минимальный пример кода:

class IntegralAsType a where
  value :: (Integral b) => a -> b

class (Num a, Fractional a, IntegralAsType q) => Zq q a | a -> q where
  changeBase:: forall p b . (Zq q a, Zq p b) => a -> b

newtype (IntegralAsType q, Integral a) => ZqBasic q a = ZqBasic a deriving (Eq)

zqBasic :: forall q a . (IntegralAsType q, Integral a) => a -> ZqBasic q a
zqBasic x = ZqBasic (mod x (value (undefined::q)))

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = fromIntegral (value (undefined::p)) -- ZqBasic is an instance of Num

Вот небольшая справка о том, чего я пытаюсь достичь: IntegralAsType обеспечивает безопасность типов во время компиляции, предотвращая что-то вроде добавления двух чисел с различным модулем. ZqBasic является внутренним представлением типа Zq, есть и другие, поэтому Zq определяется так, как оно есть. Цель состоит в том, чтобы получить систему, прозрачную для внутреннего представления.

Моя проблема с функцией changeBase. Я использую явное forall для типа 'p', но я все еще получаю "переменную неоднозначного типа a0 в ограничении (IntegralAsType a0), возникающую в результате использования значения"

Я не понимаю, почему я получаю эту ошибку. В частности, в предыдущем посте я получил помощь по поводу чего-то вроде функции «zqBasic», которая, похоже, имеет те же настройки, что и функция changeBase. Я исправил неоднозначную ошибку переменной в zqBasic, добавив явный квантификатор 'forall q a.' Без этого квантификатора я получаю неоднозначную ошибку переменной типа. Я понимаю, зачем мне нужен квантификатор, но я не понимаю, почему он не помогает для changeBase.

Спасибо

Ответы [ 3 ]

3 голосов
/ 02 декабря 2011

Использование ScopedTypeVariables здесь не помогает, потому что p, который вы используете, в любом случае, кажется, не находится в области видимости.Сравните следующие определения:

changeBase (ZqBasic x) = fromIntegral (value (undefined::foobar))

Это дает ту же ошибку, потому что это также создает новую переменную типа.

changeBase (ZqBasic x) = fromIntegral (value (5::p))

Это, однако, дает другую ошибку.Соответствующие биты:

Could not deduce (Num p1) arising from the literal `5'
        (snip)
    or from (Zq q (ZqBasic q a), Zq p b)
      bound by the type signature for
                 changeBase :: (Zq q (ZqBasic q a), Zq p b) => ZqBasic q a -> b

Это показывает, что p создается как переменная нового типа.Я предполагаю, что forall в сигнатуре типа не вносит в область видимости (в реальных объявлениях) переменные типа, которые не являются параметрами типа класса.Однако переводит переменную в область видимости для объявления по умолчанию.

В любом случае, это ни здесь, ни там.

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

zq :: (Zq q a) => a -> q
zq _ = undefined

Это в основном просто дает вам прямой доступ на уровне терминов к функциональной зависимости, так как fundep делает q однозначно для любого конкретного a.Конечно, вы не можете получить фактическое значение, но это не главное.Если undefined беспокоит вас, используйте [] :: [q] вместо аналогичного эффекта и используйте head или что угодно только тогда, когда вам нужно.

Теперь вы можете немного обернуть вещи с помощью предложения where иличто бы принудительно вывести правильные типы:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral (value (zq b))

Здесь происходит то, что b - это то, что нам нужно, но нам нужно value, чтобы увидеть тип p, который определяетсятипа b, поэтому, присваивая временному имени результат, мы можем использовать его для получения нужного нам типа.

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

В соответствующей заметке стандартная библиотечная функция asTypeOf предназначена именно для этого типа суетыс типами.

1 голос
/ 02 декабря 2011

Вызов value (undefined::p) преобразуется из p в некоторый тип a0.Из типа value единственное, что мы можем выяснить, это то, что a0 является целочисленным типом.

Это значение передается в fromIntegral, который преобразуется из a0 в b,Из типа fromIntegral единственное, что мы можем выяснить, это то, что a0 является целочисленным типом.

Ничто не определяет, какой тип a0, поэтому аннотация типа необходима для выражения value (undefined::p) для устранения неоднозначности.Если посмотреть на ваши подписи типов, похоже, что value сможет генерировать правильный тип возвращаемого значения без каких-либо дополнительных преобразований.Вы можете просто удалить вызов на fromIntegral?

Редактировать

Вам необходимо включить добавочный номер ScopedTypeVariables.Без ScopedTypeVariables переменная типа не может быть упомянута более чем в одной сигнатуре типа.В этом случае имя переменной p не относится к одной и той же переменной в сигнатуре типа функции и в ее теле.

У меня работает следующий код:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase = zqBasicChangeBase

zqBasicChangeBase :: forall p b q a.
  (IntegralAsType q, IntegralAsType p, Integral a, Zq p b) => ZqBasic q a -> b
zqBasicChangeBase (ZqBasic x) = fromIntegral (value (undefined :: p) :: Integer)
0 голосов
/ 02 декабря 2011

Два (по существу эквивалентных?) Подходов, которые работают:

1: Использование подхода CA McCann:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral ((value (zq b))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

2: Вместо того, чтобы иметь подпись a-> b, я изменилСигнатура changeBase для b-> a. Затем работает следующее:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase x = fromIntegral ((value (zq x))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

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

Кроме того, ответ на мой вопрос о разнице между конструктором 'zqBasic' и 'changeBase' заключается в том, как указано в CAMcAnn, что 'p' не было включено в область действия в объявлениях, даже еслиявный результат.Если кто-нибудь может объяснить почему , я был бы признателен.

...