Haskell Rank1类型和括号-奇怪的行为

编程问答 2022-08-15

问题描述

打开RankNTypes（没有这些签名，因为它们不是Haskell 98，says the User Guide）和-fprint-explicit-foralls（因此这些签名将不被接受），因此我可以看到量化，请考虑：

foo :: b -> (Eq c => c)              -- inferred foo :: forall {c} {b}. Eq c => b -> c
foo x = undefined

bar :: b -> (Eq b => b)              -- inferred bar :: forall {b}. Eq b => b -> b
bar x = undefined

bar2 :: b -> (forall b. Eq b => b)   --          bar2 :: forall {b1} {b}. Eq b1 => b -> b1
bar2 x = undefined

到目前为止，还不错：这些都是等级1类型。 GHC（版本8.6.5）已将约束分流到签名的前面；为bar“公用”了同名b的范围； bar2的 not 的作用域是通用的，因为在给定的签​​名中有一个明确的forall，因此名称被屏蔽。

barbar :: b -> (Eq b => b) -> (Show b => b)  --  barbar :: forall {b}. Show b => b -> (Eq b => b) -> b
barbar x y = undefined

barbar2 :: b -> Eq b => b -> (Show b => b)   --  barbar2 :: forall {b}. (Eq b,Show b) => b -> b -> b
barbar2 x y = undefined

barbar的推断签名发生了什么？嵌套的-> (Eq b => b) ->不是H98。这是否意味着b不通用？否：

*Main> barbar 'c' True
<interactive>:36:12: error:
    * Couldn't match expected type `Char' with actual type `Bool'

barbar,barbar2是第1级，并且具有相同的有效签名-还是？

添加 ：（针对答案）

barbar4 :: b -> (Eq b => b -> (Show b => b)) --  barbar4 :: forall {b}. (Eq b,Show b) => b -> b -> b
barbar4 x y = undefined

barbar,barbar4是等效的吗？因此，Eq b =>中的barbar覆盖了右侧的所有内容。然后我可以看到那是等级1。嵌套在barbar2的给定签名中的结束符不仅仅是装饰。

解决方法

这两种类型是不同的。观察此GHCi会话。首先，我们定义您的功能。 我使用Num而不是Eq来更好地解释正在发生的事情。

> barbar :: b -> (Num b => b) -> (Show b => b) ; barbar _ _ = undefined
> :t barbar
barbar :: forall {b}. Show b => b -> (Num b => b) -> b

> barbar2 :: b -> Num b => b -> (Show b => b) ; barbar2 _ _ = undefined
> :t barbar2
barbar2 :: forall {b}. (Num b,Show b) => b -> b -> b

这并不奇怪。现在，我们应用两个不选择b ~ String的函数来选择Num。此类型检查：

> :t barbar "hello" 5
barbar "hello" 5 :: [Char]

这不是：

> :t barbar2 "hello" 5
    * No instance for (Num [Char]) arising from a use of `barbar2'
    * In the expression: barbar2 "hello" 5

为什么？在第一种情况下，barbar必须确保Num b：调用方可以利用该保证来构造参数。上方，由于提供了约束，5被转换为b（即String）。

在第二种情况下，barbar2的调用者必须确保Num b，所以我们不能选择b ~ String。

现在，人们可能想知道barbar如何为通用Num b提供b约束。确实，这是不可能的，因为存在非数字类型。但是，仅当我们实际使用barbar中的第二个参数时，才需要这样做。我们不满意，所以类型检查器很满意。

确实，如果我们尝试使用第二个参数，则会收到错误消息：

> barbar3 :: b -> (Num b => b) -> (Show b => b) ; barbar3 _ y = y
    * Could not deduce (Num b) arising from a use of `y'
,

b 是“普通的”，但Eq约束不是。通常，这不是有用的配置，但原则上是可行的。这是一个例子：

rhubarb :: b -> (Eq b => b) -> b
rhubarb x _ = x

> rhubarb id id 3 :: Int
3

请注意，第二个id参数的类型为Eq (Int -> Int) => Int -> Int，这是无稽之谈...但是没关系，因为该类型的严格性不如Int -> Int。只是因为Int -> Int 没有有一个Eq实例，所以rhubarb实际上不能以任何方式使用该参数。

haskellhaskellhigher-rank-types