重叠实例-如何规避它们



我是Haskell的初学者,所以请宽容。由于这里不重要的原因,我试图定义一个运算符<^>,它接受一个函数和一个参数,并通过参数返回函数的值,而不管函数和参数中的哪一个先出现。简而言之,我希望能够写以下内容:

foo :: Int -> Int
foo x = x * x
arg :: Int
arg = 2
foo <^> arg -- valid, returns 4
arg <^> foo -- valid, returns 4

我试图通过类型族来实现这一点,如下所示:

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
class Combine t1 t2 where
type Output t1 t2 :: *
(<^>) :: t1 -> t2 -> Output t1 t2
instance Combine (a->b) a where
type Output (a->b) a = b
f <^> x = f x
instance Combine a (a->b) where
type Output a a->b = b
x <^> f = f x

在这个代码上,GHC抛出一个Conflicting family instance declarations。我的猜测是,GHC抱怨的重叠发生在类型a->b和类型a相同时。我对Haskell还不够了解,但我怀疑使用递归类型定义,可能能够构建这样的情况。我有几个问题:

  • 由于这是一个相当遥远的场景,在我的应用程序中永远不会发生(尤其是上面的fooarg),我想知道是否有一种方法可以指定一个虚拟默认实例来在重叠的情况下使用?我尝试过不同的OVERLAPSOVERLAPPING标志,但它们没有任何效果
  • 如果没有,有没有更好的方法来实现我想要的

谢谢!

在我看来,这是个坏主意,但我会同意的。

一个可能的解决方案是切换到功能依赖关系。通常,我倾向于避免使用fundepps来支持类型族,但在这里,它们以一种简单的方式编译实例。

class Combine t1 t2 r | t1 t2 -> r where
(<^>) :: t1 -> t2 -> r
instance Combine (a->b) a b where
f <^> x = f x
instance Combine a (a->b) b where
x <^> f = f x

注意,如果我们使用多态函数,这个类可能会在类型推断过程中引起问题。这是因为,使用多态函数,代码很容易变得模棱两可。

例如,id <^> id可以选择这两个实例中的任何一个。以上,melpomine已经报道const <^> id也不明确。


以下是弱相关的,但我无论如何都想分享它:

那么类型族呢?我试着做了一些实验,但我发现了一个我不知道的局限性。考虑封闭式系列

type family Output a b where
Output (a->b) a = b
Output a (a->b) = b

上面的代码编译了,但类型Output a (a->b)被卡住了。第二个方程式没有得到应用,就好像第一个方程式可能匹配一样。

通常,我可以在其他一些场景中理解这一点,但在这里统一

Output (a' -> b') b' ~ Output a (a -> b)

似乎失败了,因为我们需要a ~ (a' -> b') ~ (a' -> a -> b),这是不可能的,具有有限的类型。出于某种原因,GHC没有使用这个参数(它是否假装在这个检查中存在无限类型?为什么?)

不管怎么说,这似乎让用类型家庭取代fundeps变得比可能的更困难。我不知道为什么GHC接受我发布的fundeps代码,但拒绝OP的代码,这基本上是一样的,除了使用类型族。

@chi关闭;使用FunDeps或闭型族的方法是可能的。但CCD_ 11实例与CTF CCD_。

当池说FunDep代码被接受时,这只是一半的事实:GHC平原带你走上花园小路。它会接受这些实例,但随后你发现你无法使用它们/你会收到奇怪的错误消息。请参阅"潜在重叠"中的《用户指南》。

如果您希望解决可能不明确的Combine约束,则可能会收到一个错误,建议您尝试IncoherentInstances(或INCOHERENT杂注)。不要那样做。你有一个真正语无伦次的问题;所要做的就是将问题推迟到其他地方。避免Incoherent总是可能的——前提是您可以重新调整实例(如下所示),并且它们不会被锁在库中。

请注意,由于潜在的歧义性,另一个Haskell编译器(Hugs)不允许您这样编写Combine。它有一个更正确的Haskell(没有很好地说明)规则的实现。

答案是使用一种重叠,其中一个实例严格来说更具体。你必须首先决定你想要哪种方式,以防出现歧义。我将选择以参数为前缀的函数:

{-# LANGUAGE UndecidableInstances, TypeFamilies #-}
instance {-# OVERLAPPING #-} (r ~ b)
=> Combine (a->b) a r  where ...
instance {-# OVERLAPPABLE #-} (Combine2 t1 t2 r)
=> Combine t1 t2 r  where
(<^>) = revApp
class Combine2 t1 t2 r  | t1 t2 -> r  where
revApp :: t1 -> t2 -> r
instance (b ~ r) => Combine2 a (a->b) r  where
revApp x f = f x

请注意,CombineOVERLAPPABLE实例有裸露的tyvars,这是一个catch-all,所以它总是可匹配的。编译器所要做的就是决定某个想要的约束是否是OVERLAPPING实例的形式。

OVERLAPPABLE实例上的Combine2约束不小于头,因此需要UndecidableInstances。还要注意,延迟到Combine2意味着,如果编译器仍然无法解决问题,则可能会收到令人困惑的错误消息。

谈到bare tyvars/"总是匹配的",我使用了一个额外的技巧来让编译器非常努力地改进类型:在实例的头部有一个barer,带有Equality类型改进约束(b ~ r) =>。要使用~,即使您没有编写任何类型族,也需要打开TypeFamilies

CTF方法也是类似的。您需要Output上的一个包罗万象的等式,它调用一个辅助类型函数。同样,您需要UndecidableInstances

最新更新