特定情况下的功能依赖性

Question

作为介绍，请参阅this question和my answer。我最后注意到，您似乎可以消除对具有功能依赖性的无关类型规范的需求。这是代码：

{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}

data Nil
data TList a b where
    TEmpty :: TList Nil Nil
    (:.) :: c -> TList d e -> TList c (TList d e)
infixr 4 :.

class TApplies f h t r where
    tApply :: f -> TList h t -> r

instance TApplies a Nil Nil a where
    tApply a _ = a

instance TApplies f h t r => TApplies (a -> f) a (TList h t) r where
    tApply f (e :. l) = tApply (f e) l]

现在，对我来说直观的事情似乎是将fundep f h t -> r添加到 TApplies类型类中。但是，当我这样做时，GHC抱怨TApplies的递归实例如下：

Illegal instance declaration for
‘TApplies (a -> f) a (TList h t) r’
The coverage condition fails in class ‘TApplies’
   for functional dependency: ‘f h t -> r’
Reason: lhs types ‘a -> f’, ‘a’, ‘TList h t’
   do not jointly determine rhs type ‘r’

最后两行对我来说似乎不对，虽然我希望我只是误解了一些东西。我的推理如下：

1. 如果我们有a -> f和a，那么我们有f。
2. 如果我们有TList h t那么我们有h和t。
3. 由于我们有TApplies f h t r，我们有fundep f h t -> r。
4. 因此，因为我们有f，h和t，我们有r。

这对我来说意味着功能依赖是满足的。有人可以指出我的逻辑中的缺陷，也可能建议更合适的功能依赖选择？ （请注意，GHC允许使用类似f r -> h的东西，但似乎没有在类型指示方面提供太多余地。）

Answer 1

首先，我不知道你为什么要使用如此复杂的数据类型 - 所以我将使用简化的数据类型来解决你的问题。但是，同样的原则适用于您的确切情况。

将数据类型简单地定义为：

data TList (xs :: [*]) where 
  Nil :: TList '[]
  (:.) :: x -> TList xs -> TList (x ': xs) 

infixr 4 :.

然后你的类只有一个类型参数：

class TApplies f (xs :: [*]) r | f xs -> r where ...

并且有问题的实例看起来像

instance TApplies g ys q => TApplies (y -> g) (y ': ys) q where 

现在，检查一下它产生的错误（它与你的问题基本相同） - 即，注意它说“覆盖条件在类'TApplies'中失败”。那么这个“覆盖条件”是什么？ user guide有这样说：

覆盖条件。对于类的每个函数依赖，tvsleft - > tvsright，S中的每个类型变量（tvsright）必须出现在S（tvsleft）中，其中S是将类声明中的每个类型变量映射到实例中相应类型的替换宣言。

这是过于技术性的，但基本上它表示右侧的类型变量集 - 在这种情况下，即{q}，必须是左侧变量集的一个子集 - 这里是{y, g, ys}。显然情况并非如此。

您会注意到覆盖条件没有说明实例的上下文。这是你问题的根源！在决定功能依赖性是否成立时，不考虑上下文。我想你会同意我的看法，实际上instance TApplies (y -> g) (y ': ys) q where ...实际上是失败的，这是编译器所看到的。

解决方案很简单：将{-# LANGUAGE UndecidableInstances #-}添加到文件的顶部。除其他外，覆盖条件的目的是确保实例解析终止。如果您启用UndecidableInstances，您说“相信我，它会终止”。

---

作为旁注，目前的配方使用起来不是很好。例如，tApply (+) (1 :. 2 :. Nil)产生“模糊类型”错误，或类似的东西。更糟糕的是，tApply (+) (1 :. "s" :. Nil)产生了同样的“模糊类型”错误！对于尝试使用此类编写代码的任何人都没有帮助。您必须在任何地方指定单形类型签名以使其按原样工作。

解决方案是将实例声明发生在以下情况：

instance (a ~ a') => TApplies a '[] a' where
instance (TApplies g ys q, y ~ y') => TApplies (y -> g) (y' ': ys) q where 

然后，第一种情况按原样编译，输入默认值，然后打印“3”。在第二种情况下，你得到No instance for (Num [Char])，这实际上是有帮助的。

这样做的原因是，实例解析只关心实例头，而不关心上下文。 instance TApplies (y -> g) (y' ': ys) q是编译器看到的，显然y和y'可以是任何不相关的类型。只有在最后，当打印值时，编译器需要解析y ~ y'约束，此时你只需要表达式(+) 1 2。

---

您可以实现没有数据类型的类型，如下所示：

{-# LANGUAGE GADTs #-}
data Cons a b 
data Nil

data TList xs where
  Nil  :: TList Nil
  (:.) :: x -> TList xs -> TList (Cons x xs)

然而，没有真正的理由这样做，因为DataKinds无法破坏其他工作代码。