haskell – GHC何时可以推断出约束变量？

2023年6月7日 228次阅读

我得到类型推断错误,因为GHC不会推断约束变量.它看起来可以通过一阶统一来推断.在进一步调查中,我发现插入let-bindings会改变类型推断的行为.我想知道GHC在做什么.

这里的代码演示了这个问题.新类型ConstrainedF c代表多态函数,其类型参数受c约束.据我所知,GHC不会根据给予ConstrainedF的值来推断c.

{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, MonoLocalBinds #-}

import Data.Monoid
import GHC.Prim(Constraint)

newtype ConstrainedF c =
  ConstrainedF { runConstrainedF :: forall a. c a => [a] -> a}

applyConstrainedF :: forall c a. c a => ConstrainedF c -> [a] -> a
applyConstrainedF f xs = runConstrainedF f xs

-- GHC cannot infer the type parameter of ConstrainedF
foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) [[1], [2]]
--foo = applyConstrainedF (ConstrainedF mconcat :: ConstrainedF Monoid) [[1], [2]]

应该可以在应用程序ConstrainedF mconcat中推断类型：

> ConstrainedF有类型forall c. (forall a.c a => [a] – > a) – >约束条件c.
> mconcat有类型forall b. Monoid b => [b] – >湾
> forall b. Monoid b => [b] – > b与forall结合使用a. c a => [a] – > a通过赋值a：= b和c：= Monoid.

然而,GHC抱怨：

Could not deduce (Monoid a) arising from a use of `mconcat'
from the context (c0 a).

关于约束变量,我必须遵循哪些规则才能使GHC推断类型？

模糊类型错误的典型解决方案是添加代理值以约束模糊类型.当我尝试它时,这很挑剔.如果我只是添加一个额外的参数来约束c的类型,它可以工作：

data Cst1 (c :: * -> Constraint) = Cst1

monoid :: Cst1 Monoid
monoid = Cst1

applyConstrainedF :: forall c a. c a => ConstrainedF c -> Cst1 c -> [a] -> a
applyConstrainedF f _ xs = runConstrainedF f xs

foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) monoid [[1], [2]]

但是在foo中引入let绑定会混淆类型推断,并且它无法再与Monoid统一c.

foo_doesn't_work :: [Int]
foo_doesn't_work = let cf = ConstrainedF mconcat
                   in applyConstrainedF cf monoid [[1], [2]]

由于类型推断在这两个函数之一中得到正确的答案,这告诉我GHC将在某些情况下统一约束变量而不是其他情况.我不明白发生了什么.

最佳答案 这里的问题是子类型.在你的例子中,c也可以是(Monoid b,Eq b).

此外,您可以使用Data.Typeable来检查实例化的c.

或者,如果你要求用Monoid“统一”(c,d)(一对约束)怎么办？

问题第二部分的答案是 – 你猜对了！ – 让我们概括.

我知道你已经猜到了,因为你添加了一个MonoLocalBinds编译指示.但是,它并没有达到您的期望.你看,它只会停止真正本地绑定的泛化 – 依赖于函数参数或其他本地绑定的绑定.

例如.这工作：

foo_does_work :: () -> [Int]
foo_does_work x =
  let cf = const (ConstrainedF mconcat) x
  in applyConstrainedF cf monoid [[1], [2]]

有关详细信息,请参阅Let generalisation: Which bindings are affected?

点赞