haskell - Haskell 中伴随仿函数的函数依赖

Question

在 Haskell 中描述附属很容易:

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来自 Adjoint w m . GHC 进一步建议开启 -XUndecidableInstances .在这种情况下这样做是否安全？我是在尝试做一些不可能的事情吗？

Answer 1

您的实例以您描述的方式被拒绝，因为它不遵循 the coverage condition对于类的函数依赖。正如对 Why does this instance fail the coverage condition? 的回答中所讨论的, Adjoint w m检查覆盖条件时不考虑对您的实例的约束。

GHC further suggests turning on -XUndecidableInstances. Would it be safe to do this in this case?

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

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