haskell - 通过函数的类型确定函数的效果

Question

Haskell 类型系统 (*) 的一个有趣特性是，有时您可以仅根据其类型签名来准确知道该函数的功能(假设没有不安全 IO) 涉及黑魔法)。

例如，任何具有类型签名 a -> a 的函数都必须是恒等函数，并且任何类型为 (a,b) -> a 的函数都是相当于fst。在某些情况下，您无法完全确定该函数:a -> Int 类型有无数个不同的可能函数，但它们都是常量 - 它们都忽略第一个参数。

我发现这个属性很有趣，但我怀疑它只适用于“琐碎”的函数，例如id和const。我说得对吗？

此外，我在这里的推理仅基于直觉 - 例如，在 a -> a 中，我们对 a “一无所知”(与约束函数相反)就像 Num a => a -> a) 所以除了不改变地返回之外“不能做任何事情”。有没有正式的方法来处理此类扣除？

_{* 我知道 Haskell 的类型系统基于 Hindley–Milner 类型系统，但我对它还不够熟悉，无法对它做出任何假设}

Answer 1

您所指的概念被称为 parametricity 。对类型的通用量化给出了参数多态性和“一致性”属性，直观上就是“我们对此一无所知”的概念a在forall a. a -> a所以除了原封不动地返回它之外，“不能做任何事情”。均匀性属性所说的是类型 f :: [a] -> [a]不依赖于 a 的类型，或者更准确地说，一致依赖于它:任何人对 [a] 所做的任何事情。 a 的所有选择必须是“可行的” 。 Wadler 使用它来表明映射列表中的值然后排列列表相当于先排列然后映射。

处理这些直觉的正式方法在例如:Philip Wadler 的 Theorems for Free 并且涉及类型和关系之间的同构(实际上是部分等价关系(p.e.r.'s)的类别PER)，这表明这种一致性是该类别中的普遍属性。 p>

参数化的一个有趣结果是，您可以“双向”:从类型到有关该类型的定理，以及从类型到该类型的居民。瓦德勒的自由定理是前者的一个例子，Djinn ，一个定理证明者(某种类型的居民是该类型“定理”的“证明”)，是后者的一个例子。