HOME

TheInfoList



OR:

In
type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a found ...
, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express
precondition In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification. If a precondition is violated, the effect of th ...
s when used as
function argument In computer programming, a parameter or a formal argument is a special kind of variable used in a subroutine to refer to one of the pieces of data provided as input to the subroutine. These pieces of data are the values of the arguments (often ...
s or
postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions ...
s when used as
return type In computer programming, the return type (or result type) defines and constrains the data type of the value returned from a subroutine or method. In many programming languages (especially statically-typed programming languages such as C, C++ ...
s: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as f: \mathbb \rarr \. Refinement types are thus related to
behavioral subtyping In object-oriented programming, behavioral subtyping is the principle that subclasses should satisfy the expectations of clients accessing subclass objects through references of superclass type, not just as regards syntactic safety (such as the abse ...
.


History

The concept of refinement types was first introduced in Freeman and Pfenning's 1991 ''Refinement types for ML'', which presents a type system for a subset of
Standard ML Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of th ...
. The type system "preserves the decidability of ML's type inference" whilst still "allowing more errors to be detected at compile-time". In more recent times, refinement type systems have been developed for languages such as
Haskell Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
,
TypeScript TypeScript is a free and open source programming language developed and maintained by Microsoft. It is a strict syntactical superset of JavaScript and adds optional static typing to the language. It is designed for the development of large appl ...
and Scala.


See also

* Liquid Haskell *
Dependent types In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...


References

Type theory Type systems {{type-theory-stub