Refinement type

Type systems
General concepts
Type safety
Major categories
Static vs. dynamic Manifest vs. inferred Nominal vs. structural Duck typing
Minor categories
Dependent Flow-sensitive Gradual Intersection Latent Refinement Substructural Unique
See also
Strong and weak typing

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 [math]f: \mathbb{N} \rarr \{n \in \mathbb{N} \, | \, n \gt 5\}[/math]. 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. 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, Flow, TypeScript and Scala.

See also

• Liquid Haskell
• Dependent types