类型检查和类型系统的限制是什么? [英] What are the limits of type checking and type systems?

问题描述

类型系统经常受到批评，因为它具有限制性，即限制编程语言并禁止程序员编写有趣的程序.

Type systems are often criticised, for being to restrictive, that is limiting programming languages and prohibiting programmers to write interesting programmes.

克里斯·史密斯 声明:

我们确信程序是正确的(在此类型检查器检查的属性中)，但反过来我们必须拒绝一些有趣的程序.

We get assurance that the program is correct (in the properties checked by this type checker), but in turn we must reject some interesting programs.

和

此外，有一个可靠的数学证明，任何感兴趣的类型检查器总是保守的.构建一个不会拒绝任何正确程序的类型检查器不仅困难；不可能.

Furthermore, there is an ironclad mathematical proof that a type checker of any interest at all is always conservative. Building a type checker that doesn't reject any correct programs isn't just difficult; it's impossible.

有人可以概述一下这可能是什么有趣的程序吗?哪里证明类型检查器必须保守?

Could someone please outline what kind interesting programmes this could be? Where is it proven that type checkers have to conservative?

更一般的:类型检查和类型系统的限制是什么?

And more general: What are the limits of type checking and type systems?

推荐答案

我认为第一个陈述在技术上是错误的，但在实践中是正确的.

I think the first statement is technically wrong, though correct in practice.

静态类型本质上与证明程序的属性相同，通过使用足够强大的逻辑，您可以证明所有有趣的程序都是正确的.

Static typing is essentially the same as proving properties of programs, and by using a sufficiently powerful logic you could prove that all interesting programs are correct.

问题在于，对于强大的逻辑，类型推断不再有效，您必须将证明作为程序的一部分提供，以便类型检查器可以完成其工作.一个具体的例子是高阶证明器，例如 Coq.Coq 使用了非常强大的逻辑，但是在 Coq 中完成任何事情也非常乏味，因为您必须提供非常详细的证明.

The problem is that for powerful logics type inference no longer works, and you have to provide the proofs as part of the program so that the type checker can do its job. A concrete example are higher order provers such as Coq. Coq uses an extremely powerful logic, but it is also extremely tedious to get anything done in Coq, because you have to provide proofs in great detail.

最麻烦的有趣程序是解释器，因为它们的行为完全取决于输入.本质上，您需要反思地证明对该输入进行类型检查的正确性.

The kind of interesting programs that will give you the most trouble will be interpreters, as their behavior depends entirely on an input. Essentially you will need to reflectively prove the correctness of type checking for that input.

至于第二个陈述，他可能指的是哥德尔不完备定理.它指出，对于任何给定的证明系统，都存在无法在证明系统中证明的算术(自然数的加法和乘法的逻辑)的真实陈述.转换为静态类型系统，您将拥有一个不会做任何坏事的程序，但静态类型系统无法证明这一点.

As for the second statement, he may be referring to Gödels incompleteness theorem. It states that for any given proof system there are true statements of arithmetic (the logic of addition and multiplication of natural numbers) that cannot be proved in the proof system. Translated to static type systems you would have a program that doesn't do anything bad but the static type system couldn't prove that.

这些反例是参照证明系统的定义构造的，本质上是把我不能被证明"翻译成算术，不是很有趣.恕我直言，类似构建的程序也不会有趣.

These counterexamples are constructed by referring back to the definition of the proof system, saying essentially "I cannot be proved" translated into arithmetic, which is not very interesting. IMHO a program constructed analogously wouldn't be interesting either.

这篇关于类型检查和类型系统的限制是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！