最近在看某个Slide的时候里了解到了Refinement type这个玩意儿，今天拿来总结总结。
何为Refinement Type 言简意赅的讲：
Refinement Types = Types + Logical Predicates
即Refinement Type是由类型和谓词逻辑组合而成的，其中谓词逻辑可以对类型的值域进行约束。也就是说，我们可以在原有类型的基础上给它加个值的限定，并且可以在编译时检测是否符合谓词逻辑限定。
下面我们来玩一下Haskell和Scala中典型的Refinement Type库。
LiquidHaskell LiquidHaskell 是Haskell上一个基于Liquid Types的静态分析器，可以通过Refinement Type进行静态检查。安装的时候注意需要系统环境中有logic solvers(比如z3)。
下边我们来看看如何使用LiquidHaskell：
1
2
3
4
5
6
7
8
9
module RfT where
zero' :: Int
zero' = 0
zero'' :: Int
zero'' = 0
我们定义了两个函数zero'和zero''，这两个函数的值都是0。我们在每个函数的声明前都加了一行谓词逻辑的限定，语法类似于：
比如{-@ zero'' :: {v: Int | v > 5 } @-}代表zero''函数有一个类型为Int的参数，而且接受的值必须大于5，这就是谓词逻辑限定。我们运行一下看看结果：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
LiquidHaskell Copyright 2009 -15 Regents of the University of California . All Rights Reserved .
**** DONE : Parsed All Specifications ******************************************
**** DONE : Loaded Targets *****************************************************
**** DONE : Extracted Core using GHC *******************************************
**** DONE : generateConstraints ************************************************
Done solving.
Safe
**** DONE : solve **************************************************************
**** DONE : annotate ***********************************************************
**** Checked Binders : None *****************************************************
**** RESULT : UNSAFE ************************************************************
rft1.hs:10 :1 -6 : Error : Liquid Type Mismatch
Inferred type
VV : {VV : GHC .Types .Int | VV == (0 : int)}
not a subtype of Required type
VV : {VV : GHC .Types .Int | VV > 5 }
In Context
LiquidHaskell成功地检测出了错误 —— zero''函数不符合谓词逻辑限定。
下边再举个对函数参数和返回值进行refine的例子：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
divide :: Int -> Int -> Int
divide n d = n `div` d
f1 :: Int
f1 = divide 1 0
f2 :: Int
f2 = divide 1 1
abs' :: Int -> Int
abs' n | n > 0 = n
| otherwise = 0 - n
验证结果符合我们的期望：
1
2
3
4
5
6
7
8
9
10
11
12
13
rft1 .hs:19 :6 -15 : Error : Liquid Type Mismatch
19 | f1 = divide 1 0
^^^^^^^^^^
Inferred type
VV : {VV : GHC .Types .Int | VV == ?a}
not a subtype of Required type
VV : {VV : GHC .Types .Int | VV /= 0 }
In Context
?a := {?a : GHC .Types .Int | ?a == (0 : int)}
可以看到LiquidHaskell可以验证函数的先验条件和后验条件。
至于其中的实现原理，可以参考这篇论文：Liquid Types （数学推导太多，没看懂>_<）
refined(Scala) refined 是Scala中一个Refinement Type的实现（貌似也是借鉴的Haskell的库，连名字都抄过来了）。我们在REPL里玩玩，首先导入相关的包：
1
2
3
4
5
6
7
8
9
10
import eu.timepit.refined._
import eu.timepit.refined.api.Refined
import eu.timepit.refined.auto._
import eu.timepit.refined.numeric._
import eu.timepit.refined.boolean._
import eu.timepit.refined.char._
import eu.timepit.refined.collection._
import eu.timepit.refined.generic._
import eu.timepit.refined.string._
import shapeless.{ ::, HNil }
refined这个库直接在类型系统上进行限定，通过一个Refined[T, P]类型(aka T Refined P, T - 类型， P - 谓词逻辑)来表示，比如正整数可以表示为Int Refined Positive，非空字符串可以表示为String Refined NonEmpty。几个例子：1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
scala> val i1: Int Refined Positive = 5
i1: eu.timepit.refined.api.Refined [Int ,eu.timepit.refined.numeric.Positive ] = 5
scala> val i2: Int Refined Positive = -5
<console>:21 : error: Predicate failed: (-5 > 0 ).
val i2: Int Refined Positive = -5
scala> val i3: String Refined NonEmpty = ""
<console>:37 : error: Predicate isEmpty() did not fail.
val i3: String Refined NonEmpty = ""
^
scala> val u1: String Refined Url = "htp://example.com"
<console>:37 : error: Url predicate failed: unknown protocol: htp
val u1: String Refined Url = "htp://example.com"
^
可以看到refined内置不少Predicate，也可以自己自定义Predicate。
References
