Refinement type

From HandWiki
Jump to: navigation, search

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 [math]f: \mathbb{N} \rarr \{n \in \mathbb{N} \, | \, n \gt 5\}[/math]. Refinement types are thus related to behavioral subtyping.


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], Flow[6], TypeScript[7] and Scala.

See also


  1. 1.0 1.1 Freeman, T.; Pfenning, F. (1991). "Refinement types for ML". 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. 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. 125. Chapman & Hall. pp. 148–166. 
  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. "Type Refinements". Retrieved 21 Feb 2020. 
  7. 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. 

Hostmonster hHosting Tier.Net hosting HandWiki ads