Refinement type
| Type systems |
|---|
| General concepts |
| Major categories |
|
| Minor categories |
| See also |
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 [math]\displaystyle{ 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,[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
- Liquid Haskell
- Dependent types
References
- ↑ 1.0 1.1 Freeman, T.; Pfenning, F. (1991). "Refinement types for ML". pp. 268–277. doi:10.1145/113445.113468. https://www.cs.cmu.edu/~fp/papers/pldi91.pdf.
- ↑ Hayashi, S. (1993). "Logic of refinement types". pp. 157–172. doi:10.1007/3-540-58085-9_74.
- ↑ Denney, E. (1998). "Refinement types for specification". 125. Chapman & Hall. pp. 148–166.
- ↑ Vazou, Niki. "Liquid Haskell: Refinement Types for Haskell". The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). https://popl18.sigplan.org/event/plmw-popl-2018-liquidhaskell-overview.
- ↑ Volkov, Nikita (2015). "Refinement types as a Haskell library". http://nikita-volkov.github.io/refined/.
- ↑ Panagiotis, Vekris; Cosman, Benjamin; Jhala, Ranjit (2016). "Refinement types for TypeScript". pp. 310–325. doi:10.1145/2908080.2908110.
- ↑ Lehmann, Nico; Geller, Adam T.; Vazou, Niki; Jhala, Ranjit (6 June 2023). "Flux: Liquid Types for Rust". Proceedings of the ACM on Programming Languages 7 (PLDI): 169:1533–169:1557. doi:10.1145/3591283. https://doi.org/10.1145/3591283.
 |  |
