实例的约束推断

cro*_*eea 7 haskell ghc

考虑以下:

{-# LANGUAGE FlexibleContexts #-}
module Foo where

data D a = D a
class Foo b

instance (Num a) => Foo (D a)

f :: (Foo (D a)) => a -> a
f x = x+1
Run Code Online (Sandbox Code Playgroud)

GHC抱怨它无法推断Num a出来f.我希望从Foofor (非重叠)for的实例推断出这个约束D a.

我知道我可以使用GADT D并在Num a那里添加约束,但我希望不必为了D许多不必要的约束而污染构造函数.这种情况有没有希望发生,现在有可能吗?

Ørj*_*sen 7

我猜这会破坏重叠的实例,因此一般不推断.也就是说,你可以拥有

{-# LANGUAGE OverlappingInstances #-}
...
instance (Num a) => Foo (D a)

instance Foo (D Bool)
Run Code Online (Sandbox Code Playgroud)

然后你想要的推断肯定不会是合理的.

编辑:仔细观察文档,有可能

{-# LANGUAGE FlexibleContexts #-}
module Foo where

data D a = D a
class Foo b

instance (Num a) => Foo (D a)

f :: (Foo (D a)) => a -> a
f x = x+1
Run Code Online (Sandbox Code Playgroud)

然后在一个单独的文件中:

{-# LANGUAGE OverlappingInstances #-}
module Bar where

import Foo

instance Foo Bool

test = f True
Run Code Online (Sandbox Code Playgroud)

也就是说,文档意味着只有一个定义两个实例的模块需要有OverlappingInstances标志,所以如果Foo.f可以这样定义,你可以完全使另一个模块Bar中断类型安全.请注意,使用GHC的单独编译,f将在不知道模块的情况下完全编译Bar.

  • @Eric正如我编辑的例子所示,问题在于GHC对类的单独编译+开放世界假设原则上几乎不会对类的"所有实例"有所了解. (5认同)

Ben*_*Ben 5

箭头=>方向性的.这意味着如果 Num a持有则Foo (D a).这并不意味着如果Foo (D a)持有则Num a持有.

知道存在(并且永远不会)任何重叠的实例Foo (D a)应该意味着反向含义也是正确的,但是(a)GHC不知道这一点和(b)GHC的实例机制没有设置为使用这些知识.

要实际编译使用类型类的函数,GHC仅仅证明类型必须是类的实例是不够的.它必须实际提出一个特定的实例声明,提供成员函数的定义.我们需要一个建设性的证据,而不仅仅是存在证明.

要识别C类的实例,它可以重用一个将由正在编译的函数的调用者选择的实例,或者它必须具体地知道所涉及的类型以从可用的那些实例中选择单个实例.正在编译的函数只有在C具有约束条件时才会传递给C的实例.否则该函数必须足够单形,以至于它只能使用单个实例.

特别考虑你的例子,我们可以看到f有一个约束Foo (D a),所以我们可以依赖为我们提供的调用者.但来电者不打算给我们一个实例Num a.即使你假设我们从Num a约束中知道Foo (D a)某个地方一定有这样的实例,我们也不知道是什么,我们应该调用a哪个定义+?我们甚至不能调用另一个适用于任何Num a但在类外定义的函数,因为它们都将具有Num a约束,因此期望我们为它们识别实例.明知有无需实例实例仅仅是没有用的.

这一点并不明显,但实际上你要求GHC做的是对运行时a到达的类型进行运行时切换.这是不可能的,因为我们应该发出适用于任何类型的代码Num,甚至是尚不存在的类型,或者其实例尚不存在的代码.

一个类似的想法的工作是当你对一个约束而不是在实例.例如:

class Num a => Foo a 

f :: Foo a => a -> a
f x = x + 1
Run Code Online (Sandbox Code Playgroud)

但这只能起作用,因为我们知道所有 Foo实例都必须有一个相应的Num实例,因此所有多态函数的调用者都Foo a知道也选择一个Num实例.因此,即使不知道特定的a选择Num实例,f也知道它的调用者也将提供Num实例和Foo实例.

在你的情况下,班级 Foo一无所知Num.在其他示例中,Num甚至可能无法在定义类的模块可访问的代码Foo中定义.它是设置必须提供的必需信息的,用于调用类型类中的多态函数,并且这些多态函数必须能够在没有任何特定于某个实例的知识的情况下工作.

所以Num a => Foo (D a)实例不能存储Num实例 - 事实上,实例定义也是多态的a,因此即使有空间也无法选择要存储的特定实例!因此,即使f可能能够知道,有一个Num a从实例Foo (D a)(如果我们假定某些知识没有重叠都不能参与),它仍然需要Num a以要求其调用者选择的约束Num实例它用.