Refinement type

In type theory, a refinement type^[1][2][3] 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 ${\displaystyle f:\mathbb {N} \rightarrow \{n\in \mathbb {N} \,|\,n>5\}}$. Refinement types are thus related to behavioral subtyping.

History[edit]

The concept of refinement types was first introduced in Freeman and Pfenning's 1991 Refinement types for ML,^[1] 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,^[4][5] TypeScript,^[6] Rust^[7] and Scala.

See also[edit]

• Liquid Haskell
• Dependent types

References[edit]

${\displaystyle \Gamma \!\vdash }$

This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it.

• v
• t
• e