0

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

{-# 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) （完全相同）是一样的？我意识到我正在使用关于我的实例的外观的“特殊”知识，但我认为应该有一种方法可以将它传达给编译器。

谢谢

4

1 回答 1

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

如果这对于任何类型的构造函数都是正确的，那么您可以考虑将其写为一个实例：

-- 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期望一个 kind 的论点*。所以我假设你的意思是S (T (X a' Int)) ~ Int。

    尽管有这些抱怨，但我们可以问为什么S (T (X a' Int)) ~ Int不能从我们迄今为止的假设中得到证明。到目前为止，我们只Foo为符合模式的类型声明了实例，X (Z i) i并且X (Z' i) i. 因此，类型函数T只有在其参数类型符合其中一种模式时才能减少。该类型X a' Int不太适合这两​​种模式。我们可以把它塞进正确的模式：我们可以尝试减少 withX (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))to强制转换的原因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
于 2012-07-16T16:15:03.333 回答