所以就看你理解不理解这个predicate了——一般情况下，是一个返回Bool的函数。
哦，忘了谢邀了。不过你在我写作文的时候邀请我回答问题，我不谢邀（逃）。
给类型带上refinement，就可以表达一些indexed inductive data family能表达的东西，而且更简洁，更直观。比如，如果是有indexed inductive data family的编程语言，比如Idris，要写一个安全的除法，类型签名应该形如：
which其实挺丑的你没发现吗，因为你要多传入一个参数作为证明。构造证明是比较麻烦的。
当然，看了我的文章的人可能会提出这种依赖函数的做法：
但这里返回类型就发生了变化，这导致输入不确定的时候输出类型也不能确定，which不好。
所以，我们可以给b加上refinement：
下面这部分是我重写的，写第一遍的时候写的东西都忘差不多了，只补回了一小部分……我提交回答后知乎自动删除了我2/3的内容。不支持Edge浏览器和Windows输入法的事情应该在我登陆的时候提醒啊。不能只支持你们测试人员使用的环境，然后随意声称我们支持一些你们听说过的别的环境，对吧。 @知乎小管家 @知一声
这样，我们就拥有了上面两种写法的好处：
有了这个东西，任何能表达成Bool表达式的性质都可以用这种很直观的方式表达了。比如，归纳定义的自然数的加法交换律所使用的第一个引理：
然后，平凡可判定的情况，原本我们使用Refl，现在我们啥都不需要写，直接把这个unit返回回来就是：
归纳的情况，我们需要rewrite。在refinement type中，直接调用这些函数，就可以把这种约束引入上下文中。这非常美妙：
很多在Idris中不直观的东西，使用refinement type表达就很直观了。
那么这么完美的东西有什么缺陷呢？
首先，它间接引入了一种子类型关系，而且是非常非常非常非常复杂的子类型关系——比如，x:int{x>0}是x:int{x>=0}的子类型。这个约束如果变得复杂一些，写程序将变得对程序员的心智要求极高。再加上，嗯，这个东西本来就有一些子类型关系，类型系统就变得更复杂了……
而且，这个东西的类型检查器非常难实现，需要对表达成Bool表达式的约束进行求解的能力。解决这种问题的工具叫SMT solver，我不是这方面的砖家所以就不乱BB了。我上面使用的代码的语法抄自F*，F*就是一个具有这种能力的编程语言——然而它的约束求解能力全部来自z3。
也就是说，掺杂了很多玄学在里面……
去掉refinement type，F*就是一个F#。而TypeScript显然和F#是类似的——TS和F#都是静态强类型的、拥有较为简单类型系统的编程语言。
于是，我们给TS的类型引入这个{}，然后把这些约束发给z3，让z3决定你的程序的正确性，不就Ok了吗（逃）（不要乱信，我很讨厌做这种没什么实际意义的事情的人，这只是开个玩笑而已）。
