Refinement type: Difference between revisions
Content deleted Content added
Akeosnhaoe (talk | contribs) Tags: Mobile edit Mobile web edit |
ThomasJMarko (talk | contribs) |
||
| Line 4: | Line 4: | ||
==History== |
==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>, [[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|booktitle=Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation|pages=310-325|year=2016|arxiv=1604.02480}}</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>, Flow<ref>{{cite web|url=https://flow.org/en/docs/lang/refinements/|title=Type Refinements|accessdate=21 Feb 2020}}</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|booktitle=Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation|pages=310-325|year=2016|arxiv=1604.02480}}</ref> and [[Scala (programming language)|Scala]]. |
||
==See also== |
==See also== |
||
Revision as of 03:44, 22 February 2020
| 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
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], Flow[5], TypeScript[6] and Scala.
See also
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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ 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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ 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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help) - ^ Vazou, Niki. Liquid Haskell: Refinement Types for Haskell. The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
- ^ "Type Refinements". Retrieved 21 Feb 2020.
- ^ 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.
{{cite conference}}: Unknown parameter|booktitle=ignored (|book-title=suggested) (help)
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |