用类约束统一关联类型同义词 [英] Unifying associated type synonyms with class constraints

问题描述

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

  { - ＃LANGUAGE TypeFamilies，
 FlexibleInstances，
 FlexibleContexts，
 MultiParamTypeClasses＃ - } 
 
f :: Int  - > Int b $ bfx = x + 1 
 
 data X ti 
 newtype Z i = Z i导出（Eq，Show）
 newtype Y q = Y（T q）
 
 class Qux mr其中$ b $ ::（T m） - > r 
 
 class（Integral（T a））=> Foo a其中
类型T a 
  -  ...函数
 
实例（Integral i）=> Foo（X（Z i）i）其中
 type T（X（Z i）i）= i 
 
 instance（Foo q）=> Num（Y q） - 其中... 
 
实例（Foo q，Foo（X m'Int））=> Qux（X m'Int）（Y q）其中
gx = fromIntegral $ f $ x 
  

哪些（即使与UndecidableInstances）导致编译器错误：

pre $ 无法推断（T（X m'Int）〜Int ）


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

我的问题是：我可以让Haskell认识到，当我将'Int'作为第二个参数写入X时，它与同义词T（X a'Int）是同一个事物吗？我意识到我正在使用关于实例外观的特殊知识，但是我认为应该有一种方式将其传达给编译器。

谢谢

因为我不确定我是否理解这个问题，所以我将讨论你写的代码;也许我漫不经心的一部分或者会指向你一个有用的方向，或者引发一些有可能让我回答的尖锐问题。这就是说：警告！首先，我们来讨论一下 Bar 类。

   -  class（i〜S b）=> Bar bi where 
  -  type S b 
  -  ... 
  

既然我们知道约束条件 i〜S b ，我们也可以放弃 i 参数，我会这样做对于剩下的讨论。

  class Bar b其中类型S b 
  - 或者，如果类是空，只是
型家庭S b 
  - 根本没有类声明
  

下面是这个新类的实例的样子：

  instance Bar（Z i）其中type S（Z i）= i 
实例Bar（Z'i）其中S（Z'i）= i 
  

如果这适用于任何类型的构造函数，那么可以考虑将其写成一个实例：

   - 实例Bar（fi）其中S（fi）= i 
  

现在，我们来讨论 Foo 类。要改变它与上面的匹配，我们会写成：

  class Bar（T a）=> Foo a类型T a 
  

你已经声明了两个实例：

   -  instance（Bar（Z i）i）=> Foo（X（Z i）i）其中
  -  type T（X（Z i）i）= Z i 
  -  
  -  instance（Bar（Z'i）i ）=> Foo（X'（Z'i）i）其中
  -  type T（X（Z'i）i）= Z'i 
  

我们可以像前面一样去除第二个参数到 Bar ，但是我们也可以做另一件事情：因为我们知道有一个 Bar（Z i） instance（我们在上面声明！），我们可以拿走实例约束。 （X（Z i）i）= Z
实例Foo（X（Z'i）i）其中类型T （X（Z'i）i）= Z'i

是否要保留 i 参数 X 取决于什么 X 应该是代表。到目前为止，我们还没有改变任何类声明或数据类型的语义 - 只有它们是如何声明和实例化的。更改 X 可能不具有相同的属性;没有看到 X 的定义很难说。通过数据声明和足够多的扩展，上面的序言编译完成。

现在，您的抱怨：

$ ul b $ b

你说以下不会编译：

  class Qux a 
实例Foo（X a'Int）=> Qux（X a'Int）
实例Foo（X'a'Int）=> Qux（X'a'Int）
  

但是，使用 UndecidableInstances ，它在这里编译。它有意义，它需要 UndecidableInstances ：没有什么可阻止某人稍后再来，并声明像

的实例

  instance Qux（XY Int）=> Foo（X Y Int）
 
然后，检查`Qux（X Y Int）`是否有实例需要检查`Foo（X Y Int）`是否有实例，反之亦然。循环。 
  

你说，它也希望实例约束 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 和<模式>的类型声明 Foo code> X（Z'i）i 。因此，类型函数 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））是一样的吗？我不明白这一点问题，你想以某种方式有一个可证的equa lity X a Int〜S（T（X a'Int））？这是我从阅读你的问题时得到的解释。

（T（X ab））;在这种情况下，答案是绝对！。我们将滥用我们上面知道的事实： b〜S（Z b）将这个方程简化为更强的一个 Z b〜T（X AB）。然后，我们可以用上面的> Foo 实例来替换这个声明，而不是更多：

 实例Foo（X ab）其中T（X ab）= Z b 
  

或者，我们可以假设另一个合理的等式： T（X ab）〜a ;那么，为证明 S（T（X ab））〜b ，我们只需要证明 S a〜b （通过减少 T ），所以我们可以编写其他的 Foo 实例：

  instance（Bar a，S a〜b）=> Foo（X a b）其中T（X a b）= a 
  

I have a nested type that I want to partially specify using associated type synonyms. Below is some extremely reduced code that demonstrates the problem:

{-# 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

which (even with UndecidableInstances) leads to the compiler error:

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

I know that adding this constraint to the instance of Qux makes the compiler happy. However, I know that in my program (T (X arg1 arg2)) = arg2, so I am trying to figure out how to not have to write this constraint.

My question is: can I make Haskell realize that when I write 'Int' as the second parameter to X, that this is (identically) the same thing as the synonym T (X a' Int)? I realize I'm using "special" knowledge about how my instances will look, but I think there should be a way to convey this to the compiler.

Thanks

解决方案

Since I'm not sure I understand the question yet, I'm going to discuss the code you wrote; perhaps some part of my rambling will either point you in a helpful direction or spark some pointed questions that are possible for me to answer. That is to say: warning! rambling non-answer ahead!

First, let's talk about the Bar class.

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

Since we know the constraint i ~ S b, we might as well drop the i argument, and I will do so for the rest of the discussion.

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

Here's how the instances for this new class would look:

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

If this is meant to be true for any type constructor, you could consider writing this as one instance instead:

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

Now, let's talk about the Foo class. To change it to match with the above, we would write

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

You've declared two instances:

-- 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

We can strip the second argument to Bar as before, but we can also do another thing: since we know there's a Bar (Z i) instance (we declared it above!), we can take away the instance constraint.

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

Whether you want to keep the i argument to X or not depends on what X is supposed to represent. So far, we haven't changed the semantics of any of the class declarations or data types -- only how they were declared and instanced. Changing X may not have the same property; it's hard to say without seeing the definition of X. With the data declarations and sufficiently many extensions, the above prelude compiles.

Now, your complaints:

• You say that the following doesn't compile:

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

  But, with UndecidableInstances, that does compile here. And it makes sense for it to need UndecidableInstances: there's nothing to stop somebody from coming along later and declaring an instance like

  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.
  

• You say, "It also wants the instance constraint S (T (X a'))) ~ Int, even though I know that in my program, these are always just synonyms.". I don't know what the first "it" is -- I can't reproduce this error -- so I can't answer this very well. Also, as I complained before, this constraint is ill-kinded: X :: (* -> *) -> * -> *, therefore X a' :: * -> *, and T expects an argument of kind *. So I'm going to assume you meant S (T (X a' Int)) ~ Int instead.

  Despite these complaints, we can ask why S (T (X a' Int)) ~ Int is not provable from the assumptions we have so far. So far, we've only declared Foo instances for types that fit the pattern X (Z i) i and X (Z' i) i. So the type function T can only reduce when its argument type fits one of those patterns. The type X a' Int doesn't quite fit either of those patterns. We could cram it into the right pattern: we could try reducing with X (Z Int) Int instead (say). Then we would find that T (X (Z Int) Int) ~ Z Int, and therefore S (T (X (Z Int) Int) ~ S (Z Int) ~ Int.

  This answers how to fix the type-level reduction, but doesn't explain how to fix whatever code is not building. To do that, we'd have to find out why the type checker needs a coercion from S (T (X a' Int)) to Int, and see if we can convince it that a more specific (and satisfiable) coercion like S (T (X (Z Int) Int)) ~ Int, or, with the suggested generalized Bar instance above, S (T (X (f Int) Int)) ~ Int. We certainly can't help you with that without having enough code to reproduce your error.

• You ask, "can I make Haskell realize that when I write 'Int' as the second parameter to X, that this is (identically) the same thing as the synonym S (T (X a' Int))?". I don't understand this question at all. You want to somehow have a provable equality X a Int ~ S (T (X a' Int))? That's the interpretation I get from a literal reading of your question.

  In context, I think you may have wanted to ask whether you can get a provable equality b ~ S (T (X a b)); in that case, the answer is, "Definitely!". We'll abuse the fact we know above that b ~ S (Z b) to reduce this equation to the stronger one Z b ~ T (X a b). Then we can just replace the Foo instances above with one that makes this declaration and nothing more:

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

  Alternately, we could postulate the other reasonable equation, T (X a b) ~ a; then, to prove that S (T (X a b)) ~ b we would just need to prove that S a ~ b (by reducing T), so we could write this other alternate Foo instance:

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

这篇关于用类约束统一关联类型同义词的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！