与refinement type的区别是：类型的项定义上满足某种性质，因此可以根据这种性质对项进行划分，从而得到划分后的类型；refinement type把这种性质推广到后验的谓词，根据谓词进行filter

精化类型简介

例如：如果一个类型实现了int compare_3way，并且这个compare_3way满足strict total order，我们可以认为这个类型满足strict total order。 Mathematics behind Comparison #4: Three-Way Comparison

在满足strict total order后，我们可以认为这个类型的所有项可以根据它的端点进行分隔，分隔成不同的子集。 模式 - 使用 is 和 switch 表达式进行模式匹配。 - C# reference | Microsoft Learn

measurement switch { 
	< -40.0 => "Too low", 
	>= -40.0 and < 0 => "Low", 
	>= 0 and < 10.0 => "Acceptable", 
	>= 10.0 and < 20.0 => "High", 
	>= 20.0 => "Too high", 
	double.NaN => "Unknown", };

像这样被划分出来的项的类型是原来的类型的子类型？

代数结构的程序化描述

（不一定对：

假设我们把公理分成两部分：

• 一部分是定义元素如何构建
• 一部分是定义元素之间的联系 而元素如何构建的公理本身也蕴含一部分元素之间的联系关系

代数结构依公理而设。