Refinement type
≈ 2 min read
Names in other languages
No names in other languages are held for this entry yet.
Article bodies are English and are not machine-translated. A name in another language is not a translation of the article.
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 f: \mathbb{N} \rarr \{n \in \mathbb{N} \, | \, n > 5\} . Refinement types are thus related to behavioral subtyping.
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 f: \mathbb{N} \rarr \{n \in \mathbb{N} \, | \, n > 5\} . 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 (primary in academia) for languages such as Haskell, TypeScript, Rust, and as libraries for real world usage in Scala. ==See also== Liquid Haskell Dependent types ==References==
Text derived from https://en.wikipedia.org/w/index.php?oldid=1322834676 under CC BY-SA 4.0; modifications have been made.