One of the major benefits of statically-typed programming languages is that they significantly improve programmer productivity. An obvious reason for this is that they dramatically reduce the amount of time spent debugging by catching most common errors at compile time. A more fundamental reason is that programmers can use the types to guide understanding of the structure of a piece of code, both during the development of the code, and during code maintenance. One proposal for increasing the benefits of static typing is to extend and existing language so that each ordinary type is refined by a number of refinement types, which allow many common program properties to be expressed and checked. In the resulting system a part of a program which is assigned a particular type may also be assigned multiple refinements of that type.
展开▼
