Refinement type: Difference between revisions

Content deleted Content added

Inline

Revision as of 21:41, 27 October 2023

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 $f:\mathbb {N} \rightarrow \{n\in \mathbb {N} \,|\,n>5\}$ . 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.

References

^ ^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. Vol. 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).
^ 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.
^ 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.

\Gamma \!\vdash

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

[freeman-pfenning-1] 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.

[2] 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.

[3] 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.

[4] Vazou, Niki. Liquid Haskell: Refinement Types for Haskell. The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).

[5] Volkov, Nikita (2015). "Refinement types as a Haskell library".

[6] 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.

[7] 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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

@@ Line 4: / Line 4: @@
 ==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 for languages such as [[Haskell (programming language)|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 (programming language)|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}}</ref> and [[Scala (programming language)|Scala]].
+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 for languages such as [[Haskell (programming language)|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 (programming language)|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}}</ref> and [[Scala (programming language)|Scala]].
 ==See also==