FunctionalDependencies не объединяет однозначно идентифицируемый тип

Question

Вот определение для MonadState, но вопрос относится к любому такому классу с FunctionalDependencies:

class Monad m => MonadState s m | m -> s where
...

Предположим, у меня есть тип данных, который использует s в качестве аргумента типа и типа класс, который работает, работает с ним:

data StateType s = StateType

class MonadState s m => FunDeps s m a where
  workWithStateType :: a -> StateType s -> m ()

Я могу с радостью создать экземпляр для этого класса, который компилируется и работает, как и ожидалось:

instance (MonadIO m, MonadState s m) => FunDeps s m (IORef (StateType s)) where
  workWithStateType ref a = liftIO $ writeIORef ref a

Но мне кажется, что s в FunDeps класс является избыточным, и я мог бы определить класс следующим образом:

class FunDepsProblem m a where
  workWithStateTypeNoCompile :: MonadState s m => a -> StateType s -> m ()

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  ...

Проблема заключается в том, что когда я пытаюсь его реализовать:

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  workWithStateTypeNoCompile ref a = liftIO $ writeIORef ref a

Я получаю ошибку компиляции, которая говорит мне, что он не может унифицировать токен состояния s в заголовке экземпляра и в функции:

fun-deps.hs:18:62: error: …
    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()
        at /path/to/fun-deps.hs:18:3-28
      ‘s’ is a rigid type variable bound by
        the instance declaration
        at /path/to/fun-deps.hs:17:10-78
      Expected type: StateType s
        Actual type: StateType s1
    • In the second argument of ‘writeIORef’, namely ‘a’
      In the second argument of ‘($)’, namely ‘writeIORef ref a’
      In the expression: liftIO $ writeIORef ref a
    • Relevant bindings include
        a :: StateType s1
          (bound at /path/to/fun-deps.hs:18:34)
        ref :: IORef (StateType s)
          (bound at /path/to/fun-deps.hs:18:30)
        workWithStateTypeNoCompile :: IORef (StateType s)
                                      -> StateType s1 -> m ()
          (bound at /path/to/fun-deps.hs:18:3)
   |
Compilation failed.

Я понимаю, что когда он определен в такой форме, там есть неявный forall :

  workWithStateTypeNoCompile :: forall s m a . MonadState s m => a -> StateType s -> m ()

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

Другими словами, монада m - это ты Он должен быть одинаковым в заголовке класса и в функции, поэтому он должен однозначно идентифицировать тип состояния s как в заголовке экземпляра, так и в типе функции. Итак, мой вопрос: почему это не объединяется? Есть ли теоретическая причина для этого или она просто не реализована в gh c?

На самом деле, если я переписываю MonadState в концептуально ту же функциональность, но использую TypeFamilies вместо FunctionalDependencies проблема кажется go прочь:

class Monad m => MonadStateFamily m where
  type StateToken m :: *

class Family m a where
  familyStateType :: MonadStateFamily m => a -> StateType (StateToken m) -> m ()

instance (MonadIO m, MonadStateFamily m, s ~ StateToken m) => Family m (IORef (StateType s)) where
  familyStateType ref a = liftIO $ writeIORef ref a

Answer 1

Очевидно, это известное ограничение FunctionalDependencies. Я выкопал Haskell -кафе сообщения Мануэля Чакраварти из более чем десятилетия go, в котором упоминается, что FunctionalDependencies не работает с экзистенциальными типами, и предоставлен очень краткий и ясный пример:

class F a r | a -> r
instance F Bool Int

data T a = forall b. F a b => MkT b

add :: T Bool -> T Bool -> T Bool
add (MkT x) (MkT y) = MkT (x + y)

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

    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        a pattern with constructor: MkT :: forall a b. F a b => b -> T a,
        in an equation for ‘add’

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

    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()

Я подозреваю, что здесь действуют точно такие же понятия, поскольку forall в workWithStateTypeNoCompile, переменная типа s1 в ошибке есть экзистенция.

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

class FunDepsWorks m a where
  workWithStateTypeCompile :: MonadState s m => a s -> StateType s -> m ()

newtype StateTypeRef s = StateTypeRef (IORef (StateType s))

instance MonadIO m => FunDepsWorks m StateTypeRef where
  workWithStateTypeCompile (StateTypeRef ref) a = liftIO $ writeIORef ref a

Обратите внимание, что a теперь является переменной типа с арностью один и применяется к s.

Спасибо Бену Гамари за компиляцию tf vs fd вики-страницы, иначе я бы никогда не нашел этот пример с экзистенциальными типами.