In
type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
, 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 the ...
s when used as
function argument
In mathematics, an argument of a function is a value provided to obtain the function's result. It is also called an independent variable.
For example, the binary function f(x,y) = x^2 + y^2 has two arguments, x and y, in an ordered pair (x, y). T ...
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 w ...
s when used as
return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as
. Refinement types are thus related to
behavioral subtyping.
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 programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...
. 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 pioneered several programming language ...
,
TypeScript
TypeScript (abbreviated as TS) is a high-level programming language that adds static typing with optional type annotations to JavaScript. It is designed for developing large applications and transpiles to JavaScript. It is developed by Micr ...
,
Rust
Rust is an iron oxide, a usually reddish-brown oxide formed by the reaction of iron and oxygen in the catalytic presence of water or air moisture. Rust consists of hydrous iron(III) oxides (Fe2O3·nH2O) and iron(III) oxide-hydroxide (FeO(OH) ...
and
Scala.
See also
*
Liquid Haskell
*
Dependent types
References
Type theory
Type systems
{{type-theory-stub