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

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

这是多态包含的一个相当奇特的实例，如 described here ，与约束包含相互作用。

如果一个类型 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) , 其中 inst :: Num a ，但没有这样的 inst ，所以我们不能翻译。

因此，在 test 的正文中代码仍使用 n :: (Num a, Ord a) => a) 检查.但是，如果我们只返回“Hello”而不使用 n , 然后类似于前面的 f在这种情况下，我们得到一个包含 forall a. a -> String 的推断类型注释类型。然后通过替换每一次出现的 n，在翻译输出中实现包含。在 test 的正文中与 \_ -> n .但是自从 n不发生在正文中，翻译在这里不做任何事情。