时间戳

首页 > 解决方案 > 不可判定的函数依赖

haskell - 不可判定的函数依赖

问题描述

我正在阅读左边的小丑，右边的小丑并玩解剖类，我遇到了覆盖条件错误。代码：

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies #-}
import Data.Bifunctor
import GHC.Generics

data Add2 p q x y = L2 (p x y) | R2 (q x y)

instance (Bifunctor p, Bifunctor q) => Bifunctor (Add2 p q) where
  bimap f g (L2 p) = L2 (bimap f g p)
  bimap f g (R2 q) = R2 (bimap f g q)

class (Functor p, Bifunctor p') => Diss p p' | p -> p' where

instance (Diss p p', Diss q q') => Diss (p :+: q) (Add2 p' q')

GHC 错误信息：

cj.hs:13:10: error:
    • Illegal instance declaration for ‘Diss (p :+: q) (Add2 p' q')’
        The coverage condition fails in class ‘Diss’
          for functional dependency: ‘p -> p'’
        Reason: lhs type ‘p :+: q’ does not determine rhs type ‘Add2 p' q'’
        Un-determined variables: p', q'
        Using UndecidableInstances might help
    • In the instance declaration for ‘Diss (p :+: q) (Add2 p' q')’
   |
13 | instance (Diss p p', Diss q q') => Diss (p :+: q) (Add2 p' q')
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

我很难理解给出的原因：我觉得类型p :+: q应该确定 rhs 类型，因为依赖关系p -> p'以及q -> q'约束Diss p p'和Diss q q'. 启用 UndecidableInstances 确实消除了错误，但我想了解为什么在这种情况下它是必要的。

标签： haskell

解决方案

GHC 文档对类似情况有这样的说法：

class Mul a b c | a b -> c where
  (.*.) :: a -> b -> c

instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

（回答者注：与您的示例一样，您可能会认为在此Mul a b c => Mul a [b] [c]实例中，由于a b确定c，它也应该是a [b]明确确定的情况[c]。）

三审声明不符合覆盖条件；确实是（有点奇怪）的定义：

f = \ b x y -> if b then x .*. [y] else y

使实例推理进入循环，因为它需要约束Mul a [b] b。

因此，覆盖条件明确排除了像您这样看起来良性但可能不是的情况。

推荐阅读