Семейство связанных типов жалуется на `pred :: T a -> Bool` с" NB: ‘T’ - это функция типа, и она не может быть инъективной " - PullRequest
Новая
       32

Семейство связанных типов жалуется на `pred :: T a -> Bool` с" NB: ‘T’ - это функция типа, и она не может быть инъективной "

0 голосов
/ 03 мая 2018

Этот код: 

{-# LANGUAGE TypeFamilies #-}

module Study where

class C a where
    type T a :: *
    pred :: T a -> Bool

- выдает эту ошибку: 

.../Study.hs:7:5: error:
    • Couldn't match type ‘T a’ with ‘T a0’
      Expected type: T a -> Bool
        Actual type: T a0 -> Bool
      NB: ‘T’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘Study.pred’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        Study.pred :: forall a. A a => T a -> Bool
      In the class declaration for ‘A’
  |
7 |     pred :: T a -> Bool
  |     ^^^^^^^^^^^^^^^^^^^

Замена ключевого слова type исправлениями data.

  • Почему одно неверно, а другое правильно?
  • Что они подразумевают под "не может быть инъективным"? Что это за функция, если ей даже не разрешено быть один в один? И как это связано с типом pred?

1 Ответ

0 голосов
/ 03 мая 2018 
instance C Int where
  type T Int = ()
  pred () = False

instance C Char where
  type T Char = ()
  pred () = True

Итак, теперь у вас есть два определения pred. Поскольку семейство типов присваивает только, ну, в общем, синонимы типов, эти два определения имеют сигнатуры 

pred :: () -> Bool

и 

pred :: () -> Bool

Хм, выглядит довольно похоже, не так ли? Тип проверки не может отличить их друг от друга. Что же тогда является 

pred ()

должно быть? True или False?

Чтобы решить эту проблему, вам нужен какой-то явный способ предоставления информации о том, к какому экземпляру должен принадлежать конкретный pred в некоторых случаях использования. Один из способов сделать это, как вы обнаружили, состоит в том, чтобы перейти к связанному семейству data: data T Int = TInt и data T Char = TChar будут двумя различимыми новыми типами, а не синонимами к типам, которые не имеют возможности обеспечить они на самом деле разные. То есть семейства данных всегда инъективны; типа семьи иногда нет. При отсутствии других подсказок компилятор предполагает, что семейство типов no является инъективным.

Вы можете объявить инъекцию семейства типов с другим расширением языка: 

{-# LANGUAGE TypeFamilyDependencies #-}
class C a where
  type T a = (r :: *) | r -> a
  pred :: T a -> a

= просто связывает r результат T с именем, поэтому он находится в области действия для аннотации инъективности r -> a, которая читается как функциональная зависимость: r результат T достаточно, чтобы определить a параметр. Вышеуказанные случаи в настоящее время являются незаконными; type T Int = () и type T Char = () вместе нарушают приемистость. Допустим только один.

Кроме того, вы можете следовать подсказке компилятора; -XAllowAmbiguousTypes делает исходный код компилируемым. Однако затем вам потребуется -XTypeApplications для разрешения экземпляра на сайте использования: 

pred @Int () == False
pred @Char () == True
...