简介
编辑在类型理论中，细化类型是一个被赋予了谓词的类型，该谓词被认为对细化类型的任何元素都是成立的。
细化类型在作为函数参数使用时可以表达前提条件，在作为返回类型使用时可以表达后置条件：例如，一个接受自然数并返回大于5的自然数的函数的类型可以写为.因此，细化类型与行为子类型化相关。
细化类型的历史
编辑细化类型的概念首次在Freeman和Pfenning的1991年《ML的细化类型》中提出，它为标准ML的一个子集提出了一个类型系统。
该类型系统保留了ML的类型推理的可解码性，同时仍然允许在编译时检测到更多的错误。
在最近，细化类型系统已经为Haskell、TypeScript和Scala等语言开发。
内容由匿名用户提供，本内容不代表vibaike.com立场，内容投诉举报请联系vibaike.com客服。如若转载，请注明出处：https://vibaike.com/170804/