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 由 Adjoint w m. GHC还建议开启 -XUndecidableInstances. 在这种情况下这样做安全吗？我是不是想做一些不可能的事情？

Answer 1

你的实例以你描述的方式被拒绝了，因为它不符合以下要求 保障条件 为类的功能依赖性。正如在对 为什么这个实例不符合覆盖条件？，该 Adjoint w m 在检查覆盖条件时，不会考虑到你的实例上的约束。

GHC进一步建议开启 -XUndecidableInstances. 在这种情况下，这样做安全吗？

UndecidableInstances 是一个相对无害的扩展。当你打开它的时候，最坏的情况就是因为某个实例使typechecker循环而导致构建失败。虽然GHC默认对这件事持保守态度，但有时你就是比编译器更清楚，可以确定实例解析会终止。在这种情况下，可以将 UndecidableInstances 上。尤其是这里，似乎可以做到。

---

附注：在你的代码中，我确实看到一个问题，那就是 StoreT s w 和 StateT s m 实际上并不是邻接。特别是，一个右邻点必须是可表示的，而 StateT s m 是不可表示的。即使我们能够写出 unit 和 counit 的类型检查，它们实际上不会产生一个邻接同构。也请看HaskHask判定式是如何在 Data.Functor.Adjunction.