什么是编程语言中的不变量，为什么它很重要？

Question

谁能解释一下编程语言中的不变量是什么以及它们为什么重要？

Answer 1

什么是不变量

任何字段中的不变量 - 是值（通常是数字），如果这些不变量不相同，则允许您区分“对象”。

例如，如果你有一个数学术语说

(x+3)²+1

并且您想转换该术语，一个不变量将替换为随机数x，我的 rng 选择了x=0- 所以不变量将是

(0+3)²+1 = 9+1 = 10

那么如果我错误地转换了这个词

x²+6x+3 + 1 = x² + 6x +4

再次测试x = 0我看到0²+0+4 = 4哪个不同，10因此我知道一定有错误。但如果另一方面我把这个词变成了

x²+3x+9 +1 = x²+3x+10

不变量 forx=0将10再次出现 - 所以我们看到

它们为什么有用？

• 不同的不变量 => 不同的对象
• 相同的不变量 => 可能是相同的对象

例子： equational reasoning

为什么这在（函数式）编程中变得有趣 - 在这种情况下你会听到的一个表达是equational reasoning，这意味着如果你可以将算法/函数/术语转换为另一个算法/函数/术语而不会失去相等性，那么这就是我上面所做的过程。这对于像haskell这样的语言来说通常是正确的，因为限制了不变性，没有副作用等。而在oo中这通常不是真的。等式推理允许您缩小出现错误的区域，因此调试/错误查找相对更容易完成。

例子： property based testing

另一个常见不变量的领域是基于属性的测试：这里的标准示例 this reverse :: [a] -> [a]，即（链接）列表上的反向函数，具有 的属性reverse . reverse == id，即反转两次与什么都不做是一样的。如果您将其放入 Quickcheck 测试中 - 测试生成器会生成任意列表并检查此属性 - 如果其中一个（可能）数千个测试失败，您知道在哪里改进您的代码。

例子： Compiler optimizations

某些属性也可用于优化您的代码，例如，如果对于所有函数fmap f . fmap g == fmap (f . g)，左侧遍历数据结构两次，而右侧只遍历一次，则编译器可以替换它们并使您的代码速度提高两倍.