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.
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,[4][5] TypeScript,[6] Rust[7] and Scala.
This programming language theory or type theory-related article is a stub.