时间戳

首页 > 解决方案 > Haskell 中伴随函子的函数依赖

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

问题描述

在 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. 在这种情况下这样做是否安全？我在尝试做一些不可能的事情吗？

标签： haskellfunctional-programmingmonadsfunctorfunctional-dependencies

解决方案

您的实例以您描述的方式被拒绝，因为它不遵循类的功能依赖项的覆盖条件。正如在为什么此实例无法满足覆盖条件的答案中所讨论的那样？，Adjoint w m在检查覆盖条件时不考虑对您的实例的约束。

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

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

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

推荐阅读