Haskell 中伴随函子的函数依赖

Question

在 Haskell 中描述 adjunction 很容易：

class Functor f where
  map :: (a -> b) -> f a -> f b

class Functor m => Monad m where
  return :: a -> m a
  join :: m (m a) -> m a

class Functor w => Comonad w where
  extract :: w a -> a
  duplicate :: w a -> w (w a)

class (Comonad w, Monad m) => Adjoint w m | w -> m, m -> w where
  unit :: a -> m (w a)
  counit :: w (m a) -> a

但是，我很难证明 StoreT s w 和 StateT s m 是伴随的。

instance Adjoint w m => Adjoint (StoreT s w) (StateT s m) where
  -- ...

GHC 抱怨m 不能被StoreT s w 确定，因为m 没有出现在StoreT s w 中：

• Illegal instance declaration for
    ‘Adjoint (StoreT s w) (StateT s m)’
    The coverage condition fails in class ‘Adjoint’
      for functional dependency: ‘w -> m’
    Reason: lhs type ‘StoreT s w’
      does not determine rhs type ‘StateT s m’
    Un-determined variable: m
    Using UndecidableInstances might help
• In the instance declaration for
    ‘Adjoint (StoreT s w) (StateT s m)’

我真的不明白为什么这是一个问题，因为 w -> m by Adjoint w m。 GHC 进一步建议开启-XUndecidableInstances。在这种情况下这样做是否安全？我在尝试做一些不可能的事情吗？

Answer 1

您的实例以您描述的方式被拒绝，因为它不遵循 the coverage condition 的类的功能依赖关系。正如Why does this instance fail the coverage condition? 的答案中所讨论的，在检查覆盖条件时不会考​​虑您实例上的Adjoint w m 约束。

GHC 进一步建议开启-XUndecidableInstances。在这种情况下这样做是否安全？

UndecidableInstances 是一个相对无害的扩展。打开它时可能发生的最糟糕的事情是构建失败，因为某些实例使类型检查器循环。虽然 GHC 在这件事上默认是保守的，但有时你只是比编译器更了解，并且可以确定实例解析将终止。在这种情况下，可以打开UndecidableInstances。特别是，在这里做似乎很好。

---

旁注：我在您的代码中看到的一个问题是 StoreT s w 和 StateT s m 实际上并不是伴随的。特别是，右伴随词必须是可表示的，而StateT s m 是不可表示的。即使我们设法编写了类型检查的unit 和counit 的实现，它们实际上也不会产生附加同构。另请参阅 Data.Functor.Adjunction 中如何制定 Hask/Hask 附加语。