Haskell 类型系统 (*) 的有趣特性之一是，有时您可以仅根据其类型签名准确地判断函数的作用（假设没有涉及unsafe IO黑魔法）。
例如，任何具有类型签名a -> a的函数都必须是恒等函数，任何类型的函数(a,b) -> a都等价于fst. 在某些情况下，您无法完全确定函数：类型有无数种不同的可能函数a -> Int，但它们都是常量——它们都忽略了第一个参数。
我觉得这个属性很吸引人，但我怀疑它只适用于“微不足道”的函数，例如idand const。我对么？
此外，我在这里的推理仅基于直觉 - 例如，在 中a -> a，我们“一无所知” a（与像 等受约束的函数相反Num a => a -> a），因此除了原样返回之外，“不能做任何事情”。有没有正式的方法来处理这些扣除？
* 我知道 Haskell 的类型系统是基于Hindley-Milner 类型系统的，但我对它还不够熟悉，无法对此做出任何假设
您所指的概念称为参数化。对类型的通用量化给出了参数多态性和“统一性”属性，直观上就是“我们对此一无所知”a的概念，forall a. a -> a因此除了将其原封不动地返回之外，“不能做任何事情”。均匀性属性所说的是类型f :: [a] -> [a]不依赖于 的类型a，或者更准确地说，一致地依赖于它：任何人对 的“做”的事情都[a]必须对 的所有选择都是“可行的” a。Wadler 用它来说明映射列表中的值然后排列列表等同于先排列后映射。
处理这些直觉的正式方法在例如 Philip Wadler 的自由定理中给出，涉及类型和关系之间的同构（实际上是部分等价关系 (per's) 的类别PER），这表明这种一致性是一个普遍的属性在类别中。
参数化的一个有趣结果是你可以“双向”：从一个类型到关于该类型的定理，从一个类型到该类型的居民。Wadler 的自由定理是前者的一个例子，而Djinn是一个定理证明者（一个类型的居民是该类型“定理”的“证明”），是后者的一个例子。