Проблема с созданием класса типов для гетерогенной операции - PullRequest
0 голосов
/ 21 сентября 2018

Ниже приводится очень упрощенная версия того, что я пытаюсь сделать.

Предположим, я хочу создать общую разностную операцию, которая может принимать операнды разных типов.

class Diff a b c where
    diff :: a -> b -> c

Естественно, мы можем применить эту операцию к числам.

instance Num a ⇒ Diff a a a where
    diff = (-)

Но не только к числам.Если мы скажем два момента времени, то разница между ними будет временным интервалом.

newtype TimePoint = TP Integer deriving Show -- seconds since epoch
newtype TimeInterval = TI Integer deriving Show -- in seconds

instance Diff TimePoint TimePoint TimeInterval where
    diff (Tp x) (Tp y) = TI (x-y)

Все хорошо.За исключением случаев, когда я пытаюсь проверить мой diff в GHCi, я получаю следующее:

*Example λ diff 5 3

<interactive>:1:1: error:
    • Could not deduce (Diff a0 b0 c)
      from the context: (Diff a b c, Num a, Num b)
        bound by the inferred type for ‘it’:
                   forall a b c. (Diff a b c, Num a, Num b) => c
        at <interactive>:1:1-8
      The type variables ‘a0’, ‘b0’ are 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 c. (Diff a b c, Num a, Num b) => c
*Example λ

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

Давайте попробуем немного помочь.

class Diff a b c | a b -> c where
  diff ∷ a -> b -> c

Теперь он сможет определить тип результата!К сожалению, это не компилируется:

[1 of 1] Compiling Example          ( Example.hs, interpreted )

Example.hs:8:10: error:
    Functional dependencies conflict between instance declarations:
      instance Num a => Diff a a a -- Defined at Example.hs:8:10
      instance Num a => Diff (TimePoint a) (TimePoint a) (TimeInterval a)
        -- Defined at Example.hs:14:10
  |
8 | instance Num a => Diff a a a where
  |          ^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude GOA λ 

Кстати, я пробовал также связанные семейства типов вместо fundeps, с предсказуемо похожими результатами.

Теперь я прекрасно понимаю, почему это происходит.Есть два экземпляра Diff a a a и Diff (TimePoint a) (TimePoint a) (TimeInterval a), и они не могут сосуществовать с установленным fundep.Вопрос в том, как мне обойти эту проблему?Обтекание чисел в новом типе не является жизнеспособным решением, мне нужно уметь писать diff 5 3 и diff time1 time2, и типы этих выражений должны быть выведены из операндов.

Я знаю, что мог бы определитьотдельные экземпляры для Diff Int Int Int и Diff Double Double Double и Diff Rational Rational Rational, но это не идеальное решение, поскольку могут быть определены новые экземпляры Num, и код должен обрабатывать их, не определяя дополнительный экземпляр Diffдля каждого из них.

Ниже приведен минимальный полный пример:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}

module Example where

class Diff a b c | a b -> c where
  diff :: a -> b -> c

instance Num a => Diff a a a where
  diff = (-)

data TimePoint a = TP a deriving Show
data TimeInterval a = TI a deriving Show

instance Num a => Diff (TimePoint a) (TimePoint a) (TimeInterval a) where
  diff (TP x) (TP y) = TI (x - y)

Ответы [ 2 ]

0 голосов
/ 21 сентября 2018

Вы можете попробовать общий трюк, чтобы избежать проблемы соответствия головы, которую @leftaroundabout описал в своем ответе

instance {-# OVERLAPPABLE #-} (a ~ b, a ~ c, Num a) => Diff a b c where
    diff = (-)

Для этого требуется UndecidableInstances и TypeFamilies для включения ограничения объединения, и он не будетработать, если результат diff не будет окончательно напечатан, поэтому некоторый уровень вывода, например, в GHCi, невозможен.

0 голосов
/ 21 сентября 2018

Проблема в том, что Diff (TimePoint a) (TimePoint a) является частным случаем Diff a a.Вы можете подумать, что «это не из-за ограничения Num a», но помните, что вы никогда не сможете доказать, что тип является , а не экземпляром некоторого класса, потому что экземпляр все еще может быть добавлен позже.

Решение состоит в том, чтобы не определять экземпляр Diff a a a.Вместо этого определите Diff Int Int Int и Diff Double Double Double и Diff Rational Rational Rational отдельно.

...