将关联类型同义词与类约束统一起来

Question

我有一个嵌套类型，我想使用关联的类型同义词部分指定它。下面是一些非常简化的代码来演示这个问题：

{-# LANGUAGE TypeFamilies,
FlexibleInstances,
FlexibleContexts,
MultiParamTypeClasses #-}

f :: Int -> Int
f x = x+1

data X t i
newtype Z i = Z i deriving (Eq,Show)
newtype Y q = Y (T q)

class Qux m r where
    g :: (T m) -> r

class (Integral (T a)) => Foo a where
    type T a
    -- ... functions

instance (Integral i) => Foo (X (Z i) i) where
    type T (X (Z i) i) = i

instance (Foo q) => Num (Y q) -- where ...

instance (Foo q, Foo (X m' Int)) => Qux (X m' Int) (Y q) where
    g x =  fromIntegral $ f $ x

其中（即使使用 UndecidableInstances）会导致编译器错误：

Could not deduce (T (X m' Int) ~ Int)

我知道将这个约束添加到 Qux 的实例会使编译器高兴。但是，我知道在我的程序中 (T (X arg1 arg2)) = arg2，所以我想弄清楚如何不必须编写此约束。

我的问题是：我能否让 Haskell 意识到，当我将 'Int' 作为 X 的第二个参数时，这（完全相同）与同义词 T (X a' Int) 相同？我意识到我正在使用关于我的实例外观的“特殊”知识，但我认为应该有一种方法可以将这一点传达给编译器。

谢谢

Answer 1

由于我还不确定我是否理解这个问题，所以我将讨论您编写的代码；也许我漫无边际的某些部分会为您指明一个有用的方向，或者引发一些我可能回答的尖锐问题。也就是说：警告！前面漫无边际的不回答！

首先，让我们谈谈Bar 类。

-- class (i ~ S b) => Bar b i where
--     type S b
--     ...

既然我们知道约束 i ~ S b，我们不妨放弃 i 参数，我将在接下来的讨论中这样做。

class Bar b where type S b
-- or, if the class is empty, just
-- type family S b
-- with no class declaration at all

这个新类的实例如下所示：

instance Bar (Z  i) where type S (Z  i) = i
instance Bar (Z' i) where type S (Z' i) = i

如果这对于 any 类型的构造函数来说是正确的，您可以考虑将其写为一个实例：

-- instance Bar (f i) where type S (f i) = i

现在，让我们谈谈Foo 类。要将其更改为与上述匹配，我们将编写

class Bar (T a) => Foo a where type T a

您已经声明了两个实例：

-- instance (Bar (Z i) i) => Foo (X (Z i) i) where
--     type T (X (Z i) i) = Z i
--
-- instance (Bar (Z' i) i) => Foo (X' (Z' i) i) where
--     type T (X (Z' i) i) = Z' i

我们可以像以前一样将第二个参数剥离为Bar，但我们还可以做另一件事：因为我们知道有一个Bar (Z i) 实例（我们在上面声明了它！），我们可以去掉实例约束。

instance Foo (X (Z  i) i) where type T (X (Z  i) i) = Z  i
instance Foo (X (Z' i) i) where type T (X (Z' i) i) = Z' i

是否要将 i 参数保留为 X 取决于 X 应该代表什么。到目前为止，我们还没有改变任何类声明或数据类型的语义——只改变了它们的声明和实例化方式。更改X 可能没有相同的属性；没有看到X 的定义很难说。有了数据声明和足够多的扩展，上面的前奏就可以编译了。

现在，您的投诉：

• 你说下面的不编译：

  class Qux a
  instance Foo (X  a' Int) => Qux (X  a' Int)
  instance Foo (X' a' Int) => Qux (X' a' Int)
  

  但是，使用UndecidableInstances，它确实可以在这里编译。它需要UndecidableInstances 是有道理的：没有什么可以阻止某人稍后出现并声明像

  这样的实例

  instance Qux (X Y Int) => Foo (X Y Int)
  
  Then, checking whether `Qux (X Y Int)` had an instance would require checking whether `Foo (X Y Int)` had an instance and vice versa. Loop.
  

• 你说，“它也需要实例约束S (T (X a'))) ~ Int，尽管我知道在我的程序中，这些总是同义词。”。我不知道第一个“它”是什么——我无法重现这个错误——所以我不能很好地回答这个问题。另外，正如我之前抱怨的那样，这个约束是不友好的：X :: (* -> *) -> * -> *，因此X a' :: * -> *，而T 需要一个类似* 的参数。所以我假设你的意思是S (T (X a' Int)) ~ Int。

  尽管有这些抱怨，但我们可以问为什么 S (T (X a' Int)) ~ Int 无法从我们目前的假设中得到证明。到目前为止，我们只为符合X (Z i) i 和X (Z' i) i 模式的类型声明了Foo 实例。因此类型函数T 只能在其参数类型符合其中一种模式时减少。 X a' Int 类型不太适合这两​​种模式。我们可以把它塞进正确的模式：我们可以尝试用X (Z Int) Int 来减少（比如说）。然后我们会找到T (X (Z Int) Int) ~ Z Int，因此会找到S (T (X (Z Int) Int) ~ S (Z Int) ~ Int。

  这回答了如何修复类型级别的缩减，但没有解释如何修复任何未构建的代码。为此，我们必须找出为什么类型检查器需要从 S (T (X a' Int)) 到 Int 的强制转换，并看看我们是否可以说服它使用更具体（和可满足）的强制转换，例如 S (T (X (Z Int) Int)) ~ Int，或者，使用上面建议的通用Bar 实例，S (T (X (f Int) Int)) ~ Int。如果没有足够的代码来重现您的错误，我们当然无法帮助您。

• 你问，“我能否让 Haskell 意识到，当我将 'Int' 作为 X 的第二个参数时，这与同义词 S (T (X a' Int)) （完全相同）是一样的？” .我完全不明白这个问题。您想以某种方式获得可证明的平等X a Int ~ S (T (X a' Int))？这是我从字面上阅读你的问题得到的解释。

  在上下文中，我想你可能想问你是否可以得到一个可证明的相等b ~ S (T (X a b))；在这种情况下，答案是“绝对！”。我们将滥用我们在上面知道的事实b ~ S (Z b) 将这个等式简化为更强的Z b ~ T (X a b)。然后我们可以将上面的 Foo 实例替换为做出此声明的实例，仅此而已：

  instance Foo (X a b) where T (X a b) = Z b
  

  或者，我们可以假设另一个合理的等式，T (X a b) ~ a；然后，为了证明S (T (X a b)) ~ b，我们只需要证明S a ~ b（通过减少T），所以我们可以编写另一个替代Foo实例：

  instance (Bar a, S a ~ b) => Foo (X a b) where T (X a b) = a