Refinement types for ML
Tim Freeman, Frank Pfenning · ACM SIGPLAN Notices · 1991
T$'e describe a refinement of ML's type system allowing the specification of recursively defined subtypes of user-defined datatypes.The resulting system of rejirzemeni f,ypes preserves desirable properties of ML such as decidability of type inference, while at the same time allowing more errors to be detected at compile-time.The type system combines abstract interpretation with ideas from the intersection type discipline, but remains closely tied to ML in that refinement types are given only to programs which are already well-typed in ML.