在参数类型而不是函数类型中放置约束有什么作用？

Question

我在函数参数的类型中放置了一个约束，而不是在函数的类型中。
我认为这会导致语法错误或向函数类型添加更多信息。
但看起来约束被完全忽略了。

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

test :: a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

main = print "Hello World"

这给出了以下类型错误：

Test3.hs:6:8: error:
    • No instance for (Num a) arising from a use of ‘n’
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            test :: forall a. a -> String
    • In the first argument of ‘(>)’, namely ‘n’
      In the expression: n > 10
      In the expression: if n > 10 then "Hello" else "World"
  |
6 |     if n > 10 then "Hello"
  |        ^

Test3.hs:6:8: error:
    • No instance for (Ord a) arising from a use of ‘>’
      Possible fix:
        add (Ord a) to the context of
          the type signature for:
            test :: forall a. a -> String
    • In the expression: n > 10
      In the expression: if n > 10 then "Hello" else "World"
      In an equation for ‘test’:
          test (n :: (Num a, Ord a) => a)
            = if n > 10 then "Hello" else "World"
  |
6 |     if n > 10 then "Hello"
  |  

在参数的类型中添加约束实际上有什么作用？

编辑：

为什么这需要RankNTypes扩展？
如果我删除(Num a, Ord a) =>约束，则不需要它。

Answer 1

这是多态包含的一个相当奇特的实例，如此处所述，与约束包含交互。

如果类型a包含b，则在表面语言中exp :: a暗示exp :: b。包含的一个特殊例子是f :: forall a. a -> a暗示f :: Int -> Int。此外，我们已经n :: Int暗示n :: c => Int了任何c约束。

然而，在核心语言中根本没有包含。表面语言中的每个包含情况都必须转换为显式的 lambda 表达式和应用程序。此外，c => a简单地变成c -> a，并且约束函数的使用被转换为f :: c => a对某些 的简单函数应用inst :: c。因此，f :: forall a. a -> a成为f @Int :: Int -> Int， 并 n :: Int成为\_ -> n :: c -> Int。

一个很少使用的情况是函数的逆变包含规则。以下是有效代码：

f :: (Int -> Int) -> Bool
f _ = True

g :: (forall a. a -> a) -> Bool
g = f

这被翻译成

f :: (Int -> Int) -> Bool
f = \_ -> True

g :: (forall a. a -> a) -> Bool
g = \x -> f (x @Int)

它与约束包含类似地工作：

f :: forall a. (Eq a => a) -> Bool
f _ = True

g :: forall a . a -> Bool
g = f

翻译成

f :: forall a. (Eq a -> a) -> Bool
f = \_ -> True

g :: forall a . a -> Bool
g = \x -> f (\_ -> x)

更接近原始问题，如果我们有

f (x :: Eq a => a) = True

作为顶级定义，它的推断类型是forall a. (Eq a => a) -> Bool. 然而，我们可以有任何类型的注释f被包含在推断类型中！所以我们可能有：

f :: forall a. a -> Bool
f (x :: Eq a => a) = True

GHC 仍然很高兴。原始代码

test :: a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

相当于下面稍微清晰一点的版本：

test :: forall a. a -> String
test (n :: (Num a, Ord a) => a) =
    if n > 10 then "Hello"
    else "World"

该类型的错误，你得到的是仅仅是因为n实在是有两个参数的函数，一个具有类型Num a和其他Ord a，而这两个参数是包含记录Num和Ord方法。但是，由于定义中的范围内没有此类实例，因此您不能将其n用作数字。翻译会转换n > 10为(>) inst (n inst) (10 inst), where inst :: Num a，但没有这样的inst，所以我们无法翻译。

因此，在test代码体中仍然使用n :: (Num a, Ord a) => a). 但是，如果我们只返回“Hello”而不使用n，那么与前f一种情况类似，我们会得到一个包含forall a. a -> String注释类型的推断类型。然后在翻译输出中通过用 替换n的主体中的每个出现来实现test包含\_ -> n。但是由于n没有出现在正文中，因此翻译在这里没有任何作用。