haskell - let 如何与 Haskell 中更高级别的类型交互？

Question

我遇到了更高级别类型的令人困惑的情况。我想出了如何让它工作，但我不明白工作版本和非工作版本之间的区别。

使用这些背景定义:

{-# LANGUAGE RankNTypes #-}

data AugmentedRational = Exact Integer Rational -- Exact z q is q * pi^z
                       | Approximate (forall a.Floating a => a)

approximateValue :: Floating a => AugmentedRational -> a
approximateValue (Exact z q) = (pi ** (fromInteger z)) * (fromRational q)
approximateValue (Approximate x) = x

...这两个函数有什么区别。

版本A(我最初写的，不起作用)

-- lift a floating function to operate on augmented rationals, treating the function as approximate
approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f = Approximate . f . approximateValue

结果:

Cannot instantiate unification variable `b0'
with a type involving foralls: forall a. Floating a => a
  Perhaps you want ImpredicativeTypes
In the first argument of `(.)', namely `Approximate'
In the expression: Approximate . f . approximateValue

如果您遵循我不完全理解的命令式类型建议，错误消息将更改为:

No instance for (Floating (forall a. Floating a => a))
  arising from a use of `f'
In the first argument of `(.)', namely `f'
In the second argument of `(.)', namely `f . approximateValue'
In the expression: Approximate . f . approximateValue

版本 B，确实有效

{-# LANGUAGE NoMonomorphismRestriction #-} -- add this

approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f x = let fx = f $ approximateValue x
              in Approximate fx

其他非工作版本

-- this one is "perhaps you meant impredicative types"
approx f x = Approximate . f . approximateValue $ x
-- these ones give the no instance Floating (forall a.Floating a => a) message
approx f x = Approximate . f $ approximateValue x
approx f x = let x' = approximateValue x
              in Approximate . f $ x'

摘要

这是怎么回事？在我看来，这 5 个定义在语法上都是用不同的方式表达完全相同的事情。

编辑注释:删除了有关该类型是存在类型的错误声明。

Answer 1

(您的问题中没有任何内容使用存在类型。您拥有的是一个具有多态参数的构造函数 Approximate ，导致 Approximate 具有 2 级类型并领先更高级别类型和类型推断的问题。)

简短的回答是:无积分风格和更高级别的类型不能很好地结合在一起。如果涉及多态参数，请避免使用函数组合，并坚持使用普通函数应用程序或 $，一切都会好起来的。以可接受的方式编写approx的直接方法是:

approx :: (forall a . Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f ar = Approximate (f (approximateValue ar))

问题在于 GHC 无法正确支持“命令式”类型。这意味着:如果一个函数是多态的，它的类型变量可以用单态类型实例化，但不能用本身多态的类型实例化。为什么这与此相关？

让我们看看你写的内容:

approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f = Approximate . f . approximateValue

您在这里使用了函数组合 (.) 两次。函数组合的类型是这样的:

(.) :: (b -> c) -> (a -> b) -> a -> c
infixr 9 .

所以上面的定义被解析为

Approximate . (f . approximateValue)

但是

Approximate :: (forall a. Floating a => a) -> AugmentedRational

具有2级类型。因此，将 Approximate 的类型与 (.) 的第一个参数相匹配意味着:

b = forall a. Floating a => a
c = AugmentedRational

必须坚持。

这是 GHC 不允许的多态类型的 b 实例化。它建议将 ImpredicativeTypes 作为可能使其工作的语言扩展，但不幸的是，它是一个非常脆弱的语言扩展，并且通常不鼓励使用它。正如您所看到的，即使启用了 ImpredicativeTypes，GHC 通常仍然需要相当多的额外类型注释，因此如果没有额外的更改，您的程序将无法运行。

普通函数应用程序内置于 GHC 中，并在类型检查期间进行不同的处理。这就是为什么 approx 的更直接定义有效。使用 $ 也可以，但只是，因为 GHC 中实现了一个特殊的 hack，告诉类型检查器 $ 实际上与函数应用程序没有什么不同。