如何手动推断实例 const :: a -> a -> a

Question

Haskell 类型变量是隐式量化的。关键字forall出现在 后::。

例如，const输入签名

const :: a -> b -> a

写为：

const :: forall a b. a -> b -> a

我的问题是：我如何有效地推断签名

const :: forall a. a -> a -> a

从这个定义来看。我尝试使用从一阶逻辑（例如普遍消除）中学到的概念，但无法从理论角度证明其合理性。

当然，这是有道理的，因为没有什么可以排除b与 相同a。

为什么我不能证明使用该推理规则是合理的？因为我不能对第二个量词使用消除，因为变量会发生冲突。我无法实例b化a.

Answer 1

考虑：

(1) const :: forall a b. a -> b -> a

(2) const :: forall a. a -> a -> a

你不能从（1）推断出（2）；如果可以的话，那就意味着const 总是有一个类型拟合forall a. a -> a -> a（并且在（1）中并不明显，因为我们还没有应用足够的推理步骤）。但我显然可以在诸如, where has type 之const类的情况下使用。const True 'a'constBool -> Char -> Bool

您可以做的是认识到 (2) 是(1) 的实例。与一般情况b不同，但是（正如您所说）没有什么可以阻止与任何一种特定用法相同的事物。因此，从使用的上下文中，您可以推断出特定用法具有类型。例如，这种情况发生在：a baconstforall a. a -> a -> a

silly :: forall a. a -> a
silly x = const x x

您还可以单独判断const :: forall a b. a -> b -> a，如果您选择实例化，则与您得到的b相同。我们总是将其作为一个选项，因为该类型承诺对所有可能的类型都有效，其中包括我们总是选择与 for 相同的事物的可能性子集。aconst :: forall a -> a -> abba

为此，我们只需将bs 替换为as（在我们实例化的量词范围内，但这里是整个表达式）。您对是否可以这样做表示怀疑，因为变量会发生冲突，但实例化一个变量与另一个变量相同是我们在这里所做的事情的重点。这与简单地重命名变量并通过给变量赋予本应不同的相同名称来意外更改表达式不同；在这里，我们故意选择在它们不明确时检查特殊情况。

但不存在从const :: forall a -> b -> a单独（没有任何使用它的上下文）到 的纯粹推理链const :: forall a. a -> a -> a，因为当你做出这种改变时，你正在削弱/专业化const；您选择将其限制为最通用类型的子类型。如果不添加您选择限制b为与 相同的附加信息，推理规则不会让您从 (1) 到 (2) a。（用 Haskelly 术语来说，这将是一个额外的a ~ b约束）