Refinement type
| Type systems |
|---|
| General concepts |
| Major categories |
|
| Minor categories |
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.
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]References
[edit]- ^ 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.268-277&rft.date=1991&rft_id=info:doi/10.1145/113445.113468&rft.aulast=Freeman&rft.aufirst=T.&rft.au=Pfenning,+F.&rft_id=https://www.cs.cmu.edu/~fp/papers/pldi91.pdf&rfr_id=info:sid/en.wikipedia.org:Refinement+type" class="Z3988">
- ^ 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.157-172&rft.date=1993&rft_id=https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.6346#id-name=CiteSeerX&rft_id=info:doi/10.1007/3-540-58085-9_74&rft.aulast=Hayashi&rft.aufirst=S.&rfr_id=info:sid/en.wikipedia.org:Refinement+type" class="Z3988">
- ^ Denney, E. (1998). "Refinement types for specification". Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.148-166&rft.pub=Chapman+&+Hall&rft.date=1998&rft_id=https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.4988#id-name=CiteSeerX&rft.aulast=Denney&rft.aufirst=E.&rfr_id=info:sid/en.wikipedia.org:Refinement+type" class="Z3988">
- ^ Vazou, Niki. Liquid Haskell: Refinement Types for Haskell. The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
- ^ Volkov, Nikita (2015). "Refinement types as a Haskell library".
- ^ 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.310-325&rft.date=2016&rft_id=info:arxiv/1604.02480&rft_id=info:doi/10.1145/2908080.2908110&rft.aulast=Panagiotis&rft.aufirst=Vekris&rft.au=Cosman,+Benjamin&rft.au=Jhala,+Ranjit&rfr_id=info:sid/en.wikipedia.org:Refinement+type" class="Z3988">
- ^ 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.
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
