Practical refinement-type checking
Rowan Davies, Frank Pfenning · 2005
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 perhaps more important 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 these benefits is to extend an existing statically-typed language so that each ordinary type is refined by a number of refinement-types, which allow many common program invariants 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. Previous work indicates that automatically inferring refinement-types is algorithmically impractical in general. However, if a programmer annotates their pr...