类型推断不足导致编译失败,没有实例的歧义。

5

我对于这段代码为什么在有类型提示的情况下可以编译通过,但是没有类型提示时不能编译通过感到困惑。不应该存在任何实例模糊性(只存在一个实例)。

class Monad m => FcnDef β m | β -> m where
    def :: String -> β -- takes a name

instance Monad m => FcnDef (m α -> m α) m where
    def s body = body

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" ((return ()) :: m ())

另一方面,如果省略 :: m () 或所有类型声明,则编译会失败并显示以下错误:

No instance for (FcnDef (m0 () -> t0) m0)
  arising from a use of `def'

为了澄清,代码正在尝试创建一个多变量类型的def,这样就可以写例如:

def "dummy2" "input" $ \in -> return ()

编辑

这个问题比单态限制问题更加有趣。如果添加了这样的代码,那么会将实例解析为具体类型,即

dummyTest = def "dummy" (return ())
g :: IO ()
g = dummyTest

编译同样失败。


3
我还没有完全理解整个问题,但实例的数量不会有影响。实例推断是防御性的,考虑到可能出现的未来实例。看起来你的实例头两次使用了同一个变量。除非其他因素强制这些类型相同,否则它不会触发。 - pigworker
2个回答

7

外部类型签名的需求是由单态化限制引起的。

这一点的线索在于你定义的左侧。

dummyTest = ...

由于此定义没有任何参数,编译器将尝试使定义单态化。添加类型签名会覆盖此行为。

然而,正如您所指出的那样,这还不够。由于某种原因,编译器无法推断内部表达式的类型。为什么呢?让我们来玩一下类型推断引擎!

让我们从外部类型开始,尝试计算内部表达式的类型。

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())
def的类型是FcnDef β m => String -> β,但是我们将def应用到了两个参数上。这告诉我们,β必须是一个函数类型。让我们称之为x -> y
然后,我们可以很容易地推断出y必须等于m(),以满足外部类型。此外,return ()参数的类型是Monad m1 => m1 (),因此我们可以推断出我们要找的def类型必须具有类型FcnDef (m1() -> m()) m0 => def :: String -> m1() -> m()
接下来,我们将继续查找要使用的实例。唯一可用的实例不够通用,因为它要求m1m相同。因此,我们会发出像这样的错误消息:
Could not deduce (FcnDef (m1 () -> m ()) m0)
  arising from a use of `def'
from the context (Monad m)
  bound by the type signature for dummyTest :: Monad m => m ()
  at FcnDef.hs:10:1-51
Possible fix:
  add (FcnDef (m1 () -> m ()) m0) to the context of
    the type signature for dummyTest :: Monad m => m ()
  or add an instance declaration for (FcnDef (m1 () -> m ()) m0)
In the expression: def "dummy" ((return ()))
In an equation for `dummyTest':
    dummyTest = def "dummy" ((return ()))

这里需要注意的关键是,某个特定实例恰好存在并不会影响我们在尝试推断类型时所做的选择。
因此,我们要么手动使用作用域类型变量来指定这个约束,要么可以将其编码到类型类中。
class Monad m => FcnDef β m | β -> m where
    def :: String -> β -> β

instance Monad m => FcnDef (m α) m where
    def s body = body

-- dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())

现在类型推断引擎可以轻松确定return的单子必须与结果中的单子相同,并且使用NoMonomorphismRestriction,我们还可以删除外部类型签名。
当然,我不100%确定你想要达到什么目的,所以你需要判断这是否符合你尝试做的事情的上下文。

3
正如@pigworker在评论中所指出的:
实例推断在考虑可能的未来实例时是具有防御性的。看起来你的实例头两次使用了相同的变量。除非有其他东西强制这些类型相同,否则它不会触发。
这确实是关键问题,虽然@hammar的添加额外参数的方法可能是最普遍有用的解决方案,但在这种情况下,我们可以做一个观察,然后扭曲实例选择机制的一种弱点以获得好处。首先,请注意我们不能像这样编写两个实例:
instance Monad m => FcnDef (m α -> m α) m where -- etc...
instance Monad m => FcnDef (m1 α -> m2 b) m3 where -- etc...

为什么不能这样做?有点反常,因为它们有太多的重叠。第二种情况中不同的类型变量当然可以合理地实例化为相同的类型,从而匹配第一个实例;而且 OverlappingInstances 扩展在这里也不会真正帮上忙。
考虑到第一个实例在这种情况下是我们想要的,并且由于重叠意味着我们无法添加第二个实例,我们可以欺骗 GHC。我们将首先编写实际的、通用的第二个实例,然后将一些内容插入到上下文中(只有之后才会检查!),强制统一类型。如果启用了 TypeFamilies,你可以在这里使用 ~ 并写入以下内容:
instance (m1 ~ m2, m2 ~ m3, a ~ b, Monad m) => FcnDef (m1 α -> m2 b) m3 where -- etc...

这里会发生的是,GHC将根据泛型实例(generic instance)选择,而不考虑类型,然后尝试统一它们以满足约束条件。如果它们无法统一,则会出现类型检查错误,这是预期和所需的结果。如果它们匹配,那么就万事大吉。但重要的是,与您的代码不同,如果它们可以统一但仍然存在歧义,那么这将导致它们被统一。
在大多数情况下,实例选择忽略上下文是真正痛苦的,但在这种情况下非常有用。

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接