Почему мой конфликт функциональных зависимостей исчезает, когда я расширяю определение?

Question

Я пытался реализовать целые числа на уровне типов в Haskell.Для начала я реализовал натуральные числа с помощью

data Zero
data Succ a

, а затем расширил это до целых чисел с помощью

data NegSucc a

. Затем я решил создать класс Increment, который будет увеличивать целые числа.Вот как я это сделал:

{-# Language FunctionalDependencies #-}
{-# Language UndecidableInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}

import Prelude ()

-- Peano Naturals --

data Zero
data Succ a

class Peano a
instance Peano Zero
instance (Peano a) => Peano (Succ a)

-- Integers --

data NegSucc a -- `NegSucc a` is -(a+1) so that 0 can only be expressed one way

class Integer a
instance (Peano a) => Integer a
instance (Peano a) => Integer (NegSucc a)

-- Arithmetic Operations --

class Increment a b | a -> b
instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero
instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

Однако, когда я запускаю этот GHC, жалуется на Functional dependencies conflict between instance declarations и цитирует все три моих экземпляра приращения.Эта ошибка не имеет большого смысла для меня, я не вижу конфликта между отдельными объявлениями.Еще больше меня смущает то, что если я изменю первый экземпляр на два отдельных экземпляра

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

, то компилятор вообще перестанет жаловаться.Однако правила, определяющие Peano a, говорят мне, что эти две вещи должны быть одинаковыми.

Почему у меня возникает конфликт функциональных зависимостей, когда я пишу однострочную версию, но ни один, когда я пишу двухстрочную версию?

Answer 1

Вот сообщение об ошибке, которое я вижу с оригинальной версией:

negsucc.hs:28:10: error:
    Functional dependencies conflict between instance declarations:
      instance Peano a => Increment a (Succ a)
        -- Defined at negsucc.hs:28:10
      instance Increment (NegSucc Zero) Zero
        -- Defined at negsucc.hs:29:10
      instance Peano a => Increment (NegSucc (Succ a)) (NegSucc a)
        -- Defined at negsucc.hs:30:10

Мое свободное понимание здесь таково:

• функциональная зависимость a -> b означает, что GHC будет "паттерн"match "для типа a и будет ожидать обнаружения b на основе a.
• GHC не включает ограничения суперкласса в этой логике" сопоставления с образцом ".Это важно.Интуитивно вы знаете, что NegSucc не является экземпляром Peano.Однако GHC не знает, как посмотреть на NegSucc и исключить экземпляр, который требует Peano NegSucc.(Это просто вопрос знания того, как работает выбор экземпляров GHC. Можно предположить, что будущее улучшение GHC могло бы улучшить эту ситуацию.) Поэтому GHC всегда будет выбирать
• instance Peano a => Increment a (Succ a), потому что этовсеобъемлющее Increment a.Любые другие определенные экземпляры будут конфликтовать с этим экземпляром.

Теперь, разве не для этого UndecidableInstances?Чтобы разрешить конфликтующие экземпляры и позволить GHC выбрать наиболее конкретный вариант, который применяется?Вы можете так думать.Я так и думал.Однако обратите внимание, что в сообщении об ошибке конкретно говорится о Functional dependencies conflict, что означает, что я не думаю, что UndecidableInstances реализованы адекватно для обработки перекрывающихся FunDeps таким образом.

-- pseudocode for the fundep a -> b
increment a = Succ a
increment (NegSucc Zero) = Zero
increment (NegSucc (Succ a)) = NegSucc a
-- note that this is just pseudocode; unlike Haskell,
-- instead of trying cases from top to bottom
-- all cases will be tried simultaneously

Однако эта проблема несуществует, если вы «расширите» определение, как вы это сделали.

-- pseudocode for the fundep a -> b with expanded defs
increment Zero = Succ Zero
increment (Succ a) = Succ (Succ a)
increment (NegSucc Zero) = Zero
increment (NegSucc (Succ a)) = NegSucc a
-- notice how there is now no overlap on the LHS pattern matches

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

-- pseudocode for the fundep b -> a with original defs
-- I called it "decrement" instead,
-- because from the b -> a point of view, that is what it does
decrement (Succ a) = a
decrement Zero = NegSucc Zero
decrement (NegSucc a) = NegSucc (Succ a)
-- notice how there is no overlap on the LHS pattern matches

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

Answer 2

Этот ответ является расширением этого комментария , что привело меня к пониманию того, что происходит

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

Это означает, что мы не можем сделать вывод, что NegSucc a не является членом Peano, потому что всегда возможно, что он может быть объявлен один позже.

instance Peano (NegSucc a)

Таким образом, когда компилятор видит

instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero

, он не может знать, что NegSucc Zero не будет экземпляром Peano.Если NegSucc Zero является экземпляром Peano, он будет увеличиваться до Zero и Succ (NegSucc Zero), что является конфликтом функциональной зависимости.Поэтому мы должны выбросить ошибку.То же самое относится к

instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

Здесь (NegSucc (Succ a)) также может быть экземпляром Peano.

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

В новом коде

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

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