in type theory, a refinement type 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 formula_1. refinement types are thus related to behavioral subtyping.