在论文中，协变和逆变规则在处理函数类型时至关重要。协变适用于函数的返回类型，而逆变适用于参数类型。
在 (∀b. [b] → [b]) → Bool < (∀a. a → a) → Bool 中，对于输入类型，类型以逆变方式比较，这意味着更通用的类型必须位于右侧。这里，类型 a → a 比 [b] → [b] 更通用，从而使不等式成立。然而，在 [b] → Int < a → Int 的情况下，参数类型以逆变方式比较。为了使逆变成立，左侧参数必须比右侧更具体。由于 a 可以是任何类型并且 [b] 是特定类型（b 的列表），因此不等式成立但实际上不应该如此，例如，您不能使用 a -> Int 类型注释长度函数。
在我看来，正确的关系应该是 a → Int < [b] → Int，这是通过将 a 与 [b] 匹配来实现的。
我一直在阅读一些关于类型推断的论文，特别是关于函数的协变和逆变规则。我理解逆变规则的来源，但我不明白为什么它不适用于 [b] → Int < a → Int 这样的示例。
有人可以解释为什么逆变规则在这里不适用，或者我是否误解了一些基本的东西？
5
最佳答案
1
如果您问我如何重新排列列表（∀b. [b] → [b]），我可以为您提供恒等函数（∀a. a → a），因为它是最简单的列表重新排列器。
example1 :: forall b. [b] -> [b]
example1 = id @[b]
如果你想要一个关于恒等函数 ((∀a. a → a) → Bool) 的谓词——它实际上并不比常量布尔值好——那么我可以给你一个关于列表重排器的谓词 ((∀b. [b] → [b]) → Bool)，因为我知道你只会在恒等函数上调用它。
example2 :: (forall a. a -> a) -> Bool
example2 = reverses
reverses :: (forall b. [b] -> [b]) -> Bool
reverses f = f @Int [1, 2, 3] == [3, 2, 1]
如果您想要一个从任何类型的单个值列表计算整数的函数（∀b。[b] → Int），我可以给您一个不使用其参数的函数，只返回一个常量整数（∀a。a → Int）。
example3 :: forall b. [b] -> Int
example3 = const @[b] @Int 789
如果您要求一个常数函数，我不能给您length，因为它确实检查它的参数。
nonexample4 :: forall a. a -> Int
nonexample4 = length -- error
但是如果你要求的是一个从任何元素类型的列表源[]((∀b. [b]) → Int) 计算整数的函数，那么这些列表唯一可以是空列表，因此与不同length，这和常量整数函数一样好。
example5 :: (forall b. [b]) -> Int
example5 xs = 456
where
noInts = xs @Int
noChars = xs @Char
noVoids = xs @Void
example4 :: forall a. a -> Int
example4 = example5
此外，如果你要求一个函数从我想要的任何东西的神奇泉源中生成一个整数 ((∀a. a) → Int)，那么我可以随心所欲地玩假装游戏，但我知道那口井是干的——你永远不会用除了底部以外的任何东西来真正调用它。
example6 :: (forall a. a) -> Int
example6 magic = anyInt + ord anyChar
where
anyInt = magic @Int
anyChar = magic @Char
anyVoid = magic @Void -- oh no
因此最终方差不仅取决于函数箭头，还取决于量词：
- (∀a. a → Int) < (∀b. [b] → Int) 但是
- ((∀b. [b]) → Int) < ((∀a. a) → Int)
|
–
–
myfun::a -> Int myfun _ = 5myfun 也可以用 [b] -> Int 注释。并且以下也可以编译：myfun::[b] -> Int myfun _ = 5但是例如长度函数具有类型 [b] -> Int，但您不能用 a -> Int 注释它，所以它是 [b] -> Int < a -> Int 的反例，尽管如果您按照此规则执行通常的逆变方式，那么您应该有一个 < [b] 成立（任何可以用 a 类型输入的东西也可以用 [b] 类型输入）。–
–
–
|