如何与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，告诉类型检查器$实际上与函数应用程序没有什么不同。