类型系统 | Refinement Type

最近在看某个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'' :: {v: Int | v >= 0 && v < 24 } @-}
zero' :: Int
zero' = 0
{-@ zero'' :: {v: Int | v > 5 } @-}
zero'' :: Int
zero'' = 0

我们定义了两个函数zero'zero'',这两个函数的值都是0。我们在每个函数的声明前都加了一行谓词逻辑的限定,语法类似于:

1
{-@ f :: {x: T | predicate } @-}

比如{-@ zero'' :: {v: Int | v > 5 } @-}代表zero''函数有一个类型为Int的参数,而且接受的值必须大于5,这就是谓词逻辑限定。我们运行一下看看结果:

1
$ liquid --diff rft1.hs
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
{- Preconditions -}
{-@ divide :: Int -> {v: Int | v != 0 } -> Int @-}
divide :: Int -> Int -> Int
divide n d = n `div` d
f1 :: Int
f1 = divide 1 0
f2 :: Int
f2 = divide 1 1
{- Postconditions -}
{-@ abs' :: Int -> {v: Int | v >= 0 } @-}
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

文章目录
  1. 1. 何为Refinement Type
  2. 2. LiquidHaskell
  3. 3. refined(Scala)
  4. 4. References