In
type theory, 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
preconditions when used as
function arguments or
postconditions 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, 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 the ...
. 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,
TypeScript and
Scala.
See also
*
Liquid Haskell
*
Dependent types
References
Type theory
Type systems
{{type-theory-stub