问题描述
依赖类型通常被宣传为一种方式，使您能够断言程序在规范中是正确的。因此，例如，要求您编写对列表进行分类的代码 - 您可以通过将sort的概念编码为类型来编写代码，并编写一个函数作为列表a - > SortedList a 。但是，您如何证明规范 SortedList 是正确的？难道不是这种情况：您的规格越复杂，您将该规格的编码作为类型编码的可能性就越不正确？这是静态的类型系统版本，
我可以诚实地给出的唯一答案是，更多复杂和笨重的规格，你越可能犯了一个错误。你可以在类型理论的形式化中编写一些东西，就像你可以将程序的描述形式化为一个可执行的函数一样。
希望是你的规范是简单的，小到可以通过检查来判断，而你的实现可能会更大。这有助于，一旦你有一些种子的想法正式化，你可以证明这些想法是正确的。从这个角度来看，您可以更轻松地机械地和可证实地从简单的部分中获取规范的一部分，并最终从您的规范中派生出实现，从而更有可能获得正确的实现。
但是，如何形式化某些东西可能并不清楚，这可能会导致您的想法转化为形式主义时出现错误 - 您可能会遇到这种情况。当你证明另外一个事实时，你认为你证明了一件事情，或者你可能发现自己正在进行类型理论研究，以便形式化一个想法。
Dependent types are often advertised as a way to enable you to assert that a program is correct up to a specification. So, for example, you are asked to write a code that sorts a list - you are able to prove that code is correct by encoding the notion of "sort" as a type, and writing a function such as List a -> SortedList a. But how do you prove that the specification, SortedList, is correct? Wouldn't it be the case that, the more complex your specification is, the more likely it would be that your encoding of that specification as a type is incorrect?
This is the static, type-system version of, How do you tell that your tests are correct?
The only answer I can honestly give is, yes, the more complex and unwieldy your specification, the more likely you are to have made a mistake. You can mess up in writing something in a type theoretic formalism just as well as you can in formalizing the description of your program as an executable function.
The hope is that your specification is simple and small enough to judge by examination, while your implementation of that might be far larger. It helps that, once you have some "seed" ideas formalized, you can show that the ideas derived from these are correct. From that point of view, the more readily you can mechanically and provably derive parts of your specification from simpler parts, and ultimately derive your implementation from your specification, the more likely you are to get a correct implementation.
But it can be unclear how to formalize something, which has the effect that either you might make a mistake in translating your ideas into the formalism – you might think you proved one thing, when actually you proved another – or you might find yourself doing type theory research in order to formalize an idea.
这篇关于依赖类型可以证明您的代码在规格上是正确的。但你如何证明规范是正确的？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！