Jump to content

Refinement type

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Adam Williams (talk | contribs) at 19:01, 5 April 2019 (Add a history section). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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 describes a refinement type system for a subset of Standard ML. In more recent times, refinement type systems have been developed for languages such as Haskell[4], TypeScript[5] and Scala.

See also

References

  1. ^ 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)
  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. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
  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. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
  4. ^ Vazou, Niki. Liquid Haskell: Refinement Types for Haskell. The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
  5. ^ 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. doi:10.1145/2908080.2908110. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)