如何在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

如果您遵循我不完全理解的impredicative类型建议,则错误消息将更改为:

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具有rank-2类型并导致更高级别类型和类型推断的问题.)

简短的回答是:无点类型和更高级别的类型不能很好地结合在一起.如果涉及多态参数并且坚持使用普通函数应用程序$,则避免使用函数组合,或者一切都会好的.approx以一种被接受的方式写作的直接方式是这样的:

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

问题是GHC不能正确支持"impregicative"类型.这意味着:如果函数是多态的,则其类型变量可以使用单态类型进行实例化,但不能再次使用本身具有多态性的类型.为什么这里有关系？

让我们来看看你写的内容:

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

必须坚持.

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

正常功能应用程序内置于GHC中,并在类型检查期间进行不同处理.这就是为什么更直接地定义approx作品的原因.使用$也没关系,但只是因为在GHC中实现了一个特殊的hack,告诉类型检查器$与函数应用程序没有什么不同.