时间戳

首页 > 解决方案 > 在参数类型而不是函数类型中设置约束有什么作用？

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

问题描述

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

{-# 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) =>

标签： haskell

解决方案

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

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

但是，在核心语言中根本没有包含。表面语言中的每种包含情况都必须翻译成显式的 lambda 表达式和应用程序。此外，c => a简单地变成c -> a，并且约束函数的使用被转换为f :: c => a对 some的简单函数应用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它实际上是一个有两个参数的函数，一个有 typeNum 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不发生在正文中，翻译在这里没有做任何事情。

推荐阅读