Что вызывает эту двусмысленность типа? - PullRequest
Новая
       21

Что вызывает эту двусмысленность типа?

4 голосов
/ 26 апреля 2020

У меня есть два относительно простых класса, MSet: 

{-# Langage MultiParamTypeClasses #-}

-- A generalization of G set to Magmas
class MSet a b where
  (+>>) :: a -> b -> a

instance MSet Integer Integer where
  (+>>) = (+)

-- (+>>) constrained to a Magma
(<<+>>) ::
  ( MSet a a
  )
    => a -> a -> a
(<<+>>) = (+>>)

Когда я загружаюсь в ghci и пытаюсь проверить их, у меня возникает проблема: 

*Main> 1 <<+>> 2
3
*Main> 1 +>> 2

<interactive>:31:1: error:
    • Could not deduce (MSet a b0)
      from the context: (MSet a b, Num a, Num b)
        bound by the inferred type for ‘it’:
                   forall a b. (MSet a b, Num a, Num b) => a
        at <interactive>:31:1-7
      The type variable ‘b0’ is ambiguous
    • In the ambiguity check for the inferred type for ‘it’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the inferred type
        it :: forall a b. (MSet a b, Num a, Num b) => a

Хотя (+>>) работает, когда оно ограничено Magma, но неоднозначно, когда это не так.

Теперь я могу сделать: 

*Main> :set -XFlexibleContexts
*Main> 1 +>> (2 :: Integer)
3

Но я не понимаю, что здесь происходит или почему эта аннотация помогает. Я действительно не понимаю, как средство проверки типов устраняет неоднозначность (<<+>>). Если я добавлю другой экземпляр, скажем, Int, он продолжит функционировать, даже если кажется, что должно быть неоднозначно, является ли 1 Int или Integer.

Почему один из эти ошибки и почему два других нет?

1 Ответ

1 голос
/ 27 апреля 2020

По существу - вы просите GH C решить "что такое тип 1 и 2 в выражении 1 +>> 2, и ваши классы типов означают, что ответ неоднозначен.

Подробно

<<+>>

Какого типа 1 <<+>> 2? Почему, конечно, (Num a, MSet a a) => a, потому что GH C должен иметь возможность превращать литералы в значения ( Num), а затем +>> их (MSet) и сигнатура типа <<+>> говорит, что оба литерала будут иметь одинаковый тип.

Что происходит, когда вы просите GHCi напечатать значение 1 <<+>> 2? Он пытается установить значение по умолчанию от a до Integer, что успешно, потому что Num Integer и MSet Integer Integer. Затем он вычисляет выражение по умолчанию для типа.

Это причина, по которой Int экземпляр не вносит двусмысленности - GHCi не пытается определить конкретный экземпляр c для использования, вместо этого он выводит тип и затем устанавливает значения по умолчанию для переменных, оставляя только проверку экземпляра.

+>>

Какой тип 1 +>> 2? Ну ... (Num a, Num b, MSet a b) => a, похоже. вам нужно MSet, но больше нет гарантии, что a и b объединятся. К сожалению, b не появляется в типе термина - который является источником неоднозначности типа. Система типов не знает, какой вариант b использовать.

Что произойдет, когда вы попросите GHCi напечатать значение 1 +>> 2? Сначала он выводит тип термина и получает вышеуказанный тип - и теперь он сталкивается с ошибкой вывода типа, прежде чем попытается установить значение по умолчанию от a до Integer.

Почему исправления работают?

Добавление информации о типе предотвратит ошибку 

> 1 +>> (2 :: Integer) -- fine

, поскольку эти изменения устраняют неоднозначность b. GH C не нужно выводить b, поэтому он не вызывает ошибку вывода.

Странно, и я не до конца понимаю причину этого, добавив аннотацию для a также, кажется, предотвращает ошибку 

> (1 :: Integer) +>> 2 -- fine
> (1 +>> 2) :: Integer -- fine

, хотя я подозреваю, что это еще один трюк, заданный GHCi c, который по умолчанию b - Integer в (1 +>>) :: (Num b, MSet Integer b) => b -> Integer. Не цитируйте меня об этом, однако.

С fundeps

Можно устранить неоднозначность типа, используя FunctionalDependencies

class MSet a b | a -> b where
  ...

, хотя это не так Похоже, это подходит для вашего случая использования. Это решает проблему логического вывода, потому что в (Num a, Num b, MSet a b) => a знание a будет достаточно для вывода b из fundep в MSet. Позже, когда GHCi по умолчанию a до Integer, он может просто посмотреть тип b.

...