{{Short description|Types constrained by a predicate}} {{Type systems}} In type theory, a '''refinement type'''<ref name="freeman-pfenning">{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|url=https://www.cs.cmu.edu/~fp/papers/pldi91.pdf|doi=10.1145/113445.113468 |title=Refinement types for ML|book-title=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=Logic of refinement types|citeseerx = 10.1.1.38.6346|doi=10.1007/3-540-58085-9_74|book-title=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|citeseerx = 10.1.1.22.4988|title=Refinement types for specification|book-title=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> 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>f: \mathbb{N} \rarr \{n \in \mathbb{N} \, | \, n > 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'',<ref name="freeman-pfenning" /> 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,<ref>{{cite conference|title=Liquid Haskell: Refinement Types for Haskell|conference=The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018)|url=https://popl18.sigplan.org/event/plmw-popl-2018-liquidhaskell-overview|last1=Vazou |first1=Niki}}</ref><ref>{{Cite web|last=Volkov|first=Nikita|date=2015|title=Refinement types as a Haskell library|url=http://nikita-volkov.github.io/refined/}}</ref> TypeScript,<ref>{{cite conference|first1=Vekris|last1=Panagiotis|first2=Benjamin|last2=Cosman|first3=Ranjit|last3=Jhala|title=Refinement types for TypeScript|doi=10.1145/2908080.2908110|book-title=Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation|pages=310–325|year=2016|arxiv=1604.02480}}</ref> Rust,<ref>{{cite journal |last1=Lehmann |first1=Nico |last2=Geller |first2=Adam T. |last3=Vazou |first3=Niki |last4=Jhala |first4=Ranjit |title=Flux: Liquid Types for Rust |journal=Proceedings of the ACM on Programming Languages |date=6 June 2023 |volume=7 |issue=PLDI |pages=169:1533–169:1557 |doi=10.1145/3591283 |url=https://doi.org/10.1145/3591283|doi-access=free }}</ref> and as libraries for real world usage in Scala.<ref>{{Cite web |last=Thomas |first=Frank |date=2025-09-08 |title=refined: simple refinement types for Scala |url=https://github.com/fthomas/refined |url-status=live |archive-url=https://web.archive.org/web/20250821215658/https://github.com/fthomas/refined |archive-date=2025-08-21 |access-date=2025-09-08 |website=GitHub}}</ref><ref>{{Cite web |last=Fromentin |first=Raphaël |date=2025-09-08 |title=Strong type constraints for Scala |url=https://github.com/Iltotore/iron |url-status=live |archive-url=https://web.archive.org/web/20250520175623/https://github.com/Iltotore/iron |archive-date=2025-05-20 |access-date=2025-09-08 |website=GitHub}}</ref>
==See also==
* Liquid Haskell * Dependent types
==References== {{reflist}}
Category:Type theory Category:Type systems
{{type-theory-stub}}