细化类型

在类型理论中，细化类型是一个被赋予了谓词的类型，该谓词被认为对细化类型的任何元素都是成立的。

细化类型在作为函数参数使用时可以表达前提条件，在作为返回类型使用时可以表达后置条件：例如，一个接受自然数并返回大于5的自然数的函数的类型可以写为.因此，细化类型与行为子类型化相关。

细化类型的概念首次在Freeman和Pfenning的1991年《ML的细化类型》中提出，它为标准ML的一个子集提出了一个类型系统。

该类型系统保留了ML的类型推理的可解码性，同时仍然允许在编译时检测到更多的错误。

在最近，细化类型系统已经为Haskell、TypeScript和Scala等语言开发。