# 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 . Refinement types are thus related to behavioral subtyping.

## HistoryEdit

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]}, TypeScript^{[5]} and Scala.

## See alsoEdit

## ReferencesEdit

- ^
^{a}^{b}Freeman, T.; Pfenning, F. (1991). "Refinement types for ML" (PDF).*Proceedings of the ACM Conference on Programming Language Design and Implementation*. pp. 268–277. doi:10.1145/113445.113468. **^**Hayashi, S. (1993). "Logic of refinement types".*Proceedings of the Workshop on Types for Proofs and Programs*. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.**^**Denney, E. (1998). "Refinement types for specification".*Proceedings of the IFIP International Conference on Programming Concepts and Methods*.**125**. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.**^**Vazou, Niki.*Liquid Haskell: Refinement Types for Haskell*. The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).**^**Panagiotis, Vekris; Cosman, Benjamin; Jhala, Ranjit (2016). "Refinement types for TypeScript".*Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation*. pp. 310–325. arXiv:1604.02480. doi:10.1145/2908080.2908110.

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