Skip to main content
版本: Next

类型系统

本文档描述 KCL 的类型系统,包括:

  • 类型规则
  • 类型检查
  • 类型转换
  • 类型推导

类型规则

基础定义

断言

SS 的所有自由变量都定义在 Γ\Gamma

ΓS\Gamma \vdash S

Γ\Gamma 是一个变量的类型声明环境(well-formed environment),如:x1:T1x_1:T_1, ..., xn:Tnx_n:T_n

SS 的断言有三种形式:

环境断言 断言表示 Γ\Gamma 是良构类型 (well-formed type)

Γ\Gamma \vdash ◇

良构类型断言 在环境 Γ\Gamma 下,natnat 是类型表达式

Γnat\Gamma \vdash nat

类型判断断言 在环境 Γ\Gamma 下,EE 具有类型 TT

ΓE:T\Gamma \vdash E: T

推理规则

表示法

ΓS1,...,ΓSnΓS\frac{\Gamma \vdash S_1, ..., \Gamma \vdash S_n}{\Gamma \vdash S}

推理规则中的 uu, vv, ww 用于表示变量,ii, jj, kk 用于表示整数,aa, bb 用于表示浮点数,ss 用于表示字符串,cc 代表常量(整数、浮点数、字符串、布尔)的字面值, ff 用于表示函数, TT, SS, UU 用于表示类型。

环境规则

Env ⌀

\frac{}{⌀ \vdash ◇ }

类型定义

Type Bool

ΓΓboolean\frac{\Gamma \vdash ◇}{\Gamma \vdash boolean}

Type Int

ΓΓinteger\frac{\Gamma \vdash ◇}{\Gamma \vdash integer}

Type Float

ΓΓfloat\frac{\Gamma \vdash ◇}{\Gamma \vdash float}

Type String

ΓΓstring\frac{\Gamma \vdash ◇}{\Gamma \vdash string}

Type Literal

c{boolean,integer,float,string}Γliteralof(c)\frac{ c \in \{boolean, integer, float, string\}}{\Gamma \vdash literalof(c)}

Type List

ΓT TVoidΓlistof(T)\frac{\Gamma \vdash T \ T \neq Void}{\Gamma \vdash listof(T) }

Type Dict

ΓT1 ΓT2 T1Void  T2VoidΓdictof(Tk=T1,Tv=T2)\frac{\Gamma \vdash T_1 \ \Gamma \vdash T_2\ T_1 \neq Void \ \ T_2 \neq Void}{\Gamma \vdash dictof(T_k=T_1, T_v=T_2)}

Type Struct

ΓT1 ... ΓTn  TiVoid K1KnΓstructof(K1:T1,...,Kn:Tn)\frac{\Gamma \vdash T_{1} \ ... \ \Gamma \vdash T_{n} \ \ T_i \neq Void \ K_1 \neq K_n}{\Gamma \vdash structof(K_1 : T_{1}, ... , K_n : T_{n})}

Type Union

ΓT1 ... ΓTn  TiVoidΓunionof(T1,...,Tn)\frac{\Gamma \vdash T_1 \ ... \ \Gamma \vdash T_n \ \ T_i \neq Void}{\Gamma \vdash unionof(T_1, ..., T_n)}

Type None

ΓΓNone\frac{\Gamma \vdash ◇}{\Gamma \vdash None}

Type Undefined

ΓΓUndefined\frac{\Gamma \vdash ◇}{\Gamma \vdash Undefined}

Type Void

ΓΓVoid\frac{\Gamma \vdash ◇}{\Gamma \vdash Void}

Type Any

ΓΓAny\frac{\Gamma \vdash ◇}{\Gamma \vdash Any}

Type Nothing

ΓΓNothing\frac{\Gamma \vdash ◇}{\Gamma \vdash Nothing}

类型判断规则

Operand Expr

Exp Truth

ΓΓtrue:boolean\frac{\Gamma \vdash ◇}{\Gamma \vdash true: boolean}
ΓΓfalse:boolean\frac{\Gamma \vdash ◇}{\Gamma \vdash false: boolean}

Exp Int

ΓΓint:integer\frac{\Gamma \vdash ◇}{\Gamma \vdash int: integer}

Exp Flt

ΓΓflt:float\frac{\Gamma \vdash ◇}{\Gamma \vdash flt: float}

Exp Str

ΓΓstr:string\frac{\Gamma \vdash ◇}{\Gamma \vdash str: string}

Exp None

ΓΓnone:none\frac{\Gamma \vdash ◇}{\Gamma \vdash none: none}

Exp Undefined

ΓΓundefined:undefined\frac{\Gamma \vdash ◇}{\Gamma \vdash undefined: undefined}

Expr ListExp

ΓE1:T1 E2:T2 ... En:TnΓ[E1,E2,...,En]:listof sup(T1,T2,...,Tn)\frac{\Gamma \vdash E_1: T_1 \ E_2: T_2 \ ... \ E_n: T_n}{\Gamma \vdash [E_1, E_2, ..., E_n]: listof \ sup(T_1, T_2, ..., T_n)}

Expr ListComp

ΓE1:T1 Γv:T ΓE2:listof T ΓE3:booleanΓ[E1 for v in E2 if E3]:listof(T1)\frac{\Gamma \vdash E_1: T_1 \ \Gamma \vdash v: T \ \Gamma \vdash E_2: listof \ T \ \Gamma \vdash E_3: boolean}{\Gamma \vdash [E_1 \ for \ v \ in \ E_2 \ if \ E_3]: listof(T_1) }

Expr DictExp

ΓEk1:Tk1 ΓEv1:Tv1 ... ΓEkn:TkN ΓEvn:TvNΓ{Ek1:Ev1,...,Ekn:Evn}:dictof(Tk=sup(Tk1,Tk2,...Tkn), Tv=sup(Tv1,Tv2,...,Tvn))\frac{\Gamma \vdash E_{k1}: T_{k1} \ \Gamma \vdash E_{v1}: T_{v1} \ ... \ \Gamma \vdash E_{kn}: T_{kN} \ \Gamma \vdash E_{vn}: T_{vN}}{\Gamma \vdash \{E_{k1}: E_{v1}, ..., E_{{kn}}: E_{vn}\}: dictof(T_{k}=sup(T_{k1}, T_{k2}, ... T_{kn}), \ T_{v}=sup(T_{v1}, T_{v2}, ..., T_{vn}))}

Expr DictComp

ΓE1:Trki ΓE2:Trvi Γv1:Tk Γv2:Tv ΓE3:dictof(Tk, Tv) ΓE4:booleanΓ{E1:E2 for (v1,v2) in E3 if E4}:dictof(Tk=sup(Trk1,Trk2,...,Trkn),Tv=sup(Trv1,Trv2,...,Trvn))\frac{\Gamma \vdash E_1: T_{rki} \ \Gamma \vdash E_2: T_{rvi} \ \Gamma \vdash v_1: T_k \ \Gamma \vdash v_2: T_v \ \Gamma \vdash E_3: dictof(T_{k}, \ T_{v}) \ \Gamma \vdash E_4: boolean}{\Gamma \vdash \{E_1:E_2 \ for \ (v_1, v_2) \ in \ E_3 \ if \ E_4\}: dictof(T_{k}=sup(T_{rk1}, T_{rk2}, ..., T_{rkn}), T_{v}=sup(T_{rv1}, T_{rv2}, ..., T_{rvn})) }

Expr StructExpr

ΓE1:T1 ... ΓEn:Tn K1KnΓ{K1=E1,...,Kn=En}:structof(K1:T1,...,Kn:Tn)\frac{\Gamma \vdash E_{1}: T_{1} \ ... \ \Gamma \vdash E_{n}: T_{n} \ K_1 \neq K_n}{\Gamma \vdash \{K_{1} = E_{1}, ..., K_{{n}} = E_{n}\}: structof(K_1 : T_{1}, ... , K_n : T_{n})}

Literal 类型是基础类型的值类型,Union 类型是类型的组合类型,Void、Any、Nothing 是特殊的类型指代,本身没有直接的值表达式对应关系。

Primary Expr

Expr Index

ΓE:listof(T) ΓIndex:integerΓE[Index]:T\frac{\Gamma \vdash E: listof(T) \ \Gamma \vdash Index: integer}{\Gamma \vdash E[Index]: T}

Expr Call

ΓE1:T1T2 ΓE2:T1ΓE1 (E2):T2\frac{\Gamma \vdash E_1: T_1 \rightarrow T_2 \ \Gamma \vdash E_2: T_1}{\Gamma \vdash E_1 \ (E_2): T_2}

Expr List Selector

ΓE:listof(T) ΓIndex:integerΓE.[Index]:T\frac{\Gamma \vdash E: listof(T) \ \Gamma \vdash Index: integer}{\Gamma \vdash E.[Index]: T}

Expr Dict Selector

ΓE:dictof(Tk=T1,Tv=T2) ΓS1:string ... ΓSn:stringΓE.{S1,...,Sn}:dictof(Tk=T1,Tv=T2)\frac{\Gamma \vdash E: dictof(T_k = T_1, T_v=T_2) \ \Gamma \vdash S_1: string \ ... \ \Gamma \vdash S_n: string}{\Gamma \vdash E.\{S_1, ..., S_n\}: dictof(T_k = T_1, T_v=T_2)}

Expr Struct Selector

ΓE:structof(K1:T1,...,Kn:Tn) ΓKi:stringΓE.Ki:Ti\frac{\Gamma \vdash E: structof(K_1 : T_{1}, ... , K_n : T_{n}) \ \Gamma \vdash K_i: string}{\Gamma \vdash E.K_i: T_{i}}

Unary Expr

Expr +

ΓE:T   T{integer,float}Γ +E:T\frac{\Gamma \vdash E: T \ \ \ T \in \{integer, float\}}{\Gamma \vdash \ +E: T}

Expr -

ΓE:T   T{integer,float}Γ E:T\frac{\Gamma \vdash E: T \ \ \ T \in \{integer, float\}}{\Gamma \vdash \ -E: T}

Expr ~

ΓE:integerΓ  E:integer\frac{\Gamma \vdash E: integer}{\Gamma \vdash \ ~E: integer}

Expr not

ΓE:booleanΓ not E:boolean\frac{\Gamma \vdash E: boolean}{\Gamma \vdash \ not \ E: boolean}

Binary Expr

算数运算符

Expr op, op \in {-, /, %, **, //}

ΓE1:T   ΓE2:T   T{integer,float}ΓE1 op E2:T\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: T \ \ \ T \in \{integer, float\}}{\Gamma \vdash E_1 \ op \ E_2: T}

Expr +

ΓE1:T   ΓE2:T   T{integer,float,string,listof(T1)}ΓE1 + E2:T\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: T \ \ \ T \in \{integer, float, string, listof(T_1)\}}{\Gamma \vdash E_1 \ + \ E_2: T}

Expr *

ΓE1:T1   ΓE2:T2    (T1==T2{integer,float}) or (T1==interger and T2  {string,listof(T3)}) or (T2==interger and T1  {string,listof(T3)})ΓE1  E2:T\frac{\Gamma \vdash E_1: T_1 \ \ \ \Gamma \vdash E_2: T_2 \ \ \ \ (T_1==T_2 \in \{integer, float\}) \ or \ (T_1 == interger \ and \ T_2 \ \in \ \{string, listof(T_3)\}) \ or \ (T_2 == interger \ and \ T_1 \ \in \ \{string, listof(T_3)\})} {\Gamma \vdash E_1 \ * \ E_2: T}

示例

Expr %

ΓE1:interger   ΓE2:integerΓE1 % E2:interger\frac{\Gamma \vdash E_1: interger \ \ \ \Gamma \vdash E_2: integer}{\Gamma \vdash E_1 \ \% \ E_2: interger}

逻辑运算符

Expr op, op \in {or, and}

ΓE1:boolean   ΓE2:booleanΓE1 op E2:boolean\frac{\Gamma \vdash E_1: boolean \ \ \ \Gamma \vdash E_2: boolean}{\Gamma \vdash E_1 \ op \ E_2: boolean}

示例

Expr and

ΓE1:boolean   ΓE2:booleanΓE1 and E2:boolean\frac{\Gamma \vdash E_1: boolean \ \ \ \Gamma \vdash E_2: boolean}{\Gamma \vdash E_1 \ and \ E_2: boolean}

比较运算符

Expr op, op \in {==, !=, <, >, <=, >=}

ΓE1:T   ΓE2:TΓE1 op E2:boolean\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: T}{\Gamma \vdash E_1 \ op \ E_2: boolean}

示例

Expr >

ΓE1:boolean   ΓE2:booleanΓE1 > E2:boolean\frac{\Gamma \vdash E_1: boolean \ \ \ \Gamma \vdash E_2: boolean}{\Gamma \vdash E_1 \ > \ E_2: boolean}

位运算符

Expr op, op \in {&, ^, ~, <<, >>}

ΓE1:integer   ΓE2:integerΓE1 op E2:integer\frac{\Gamma \vdash E_1: integer \ \ \ \Gamma \vdash E_2: integer}{\Gamma \vdash E_1 \ op \ E_2: integer}

Expr |

ΓE1:T   ΓE2:T   T{integer,listof(T1),dictof(Tk,Tv),structof(K1=T1,...,Kn=Tn)}ΓE1  E2:T\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: T \ \ \ T \in \{integer, listof(T_1), dictof(T_k, T_v), structof(K_1=T_1, ..., K_n=T_n)\}}{\Gamma \vdash E_1 \ | \ E_2: T}

成员运算符

Expr op, op \in {in, not in}

ΓE1:string   ΓE2:T   T{dictof,structof}ΓE1 op E2:bool\frac{\Gamma \vdash E_1: string \ \ \ \Gamma \vdash E_2: T \ \ \ T \in \{dictof, structof\}}{\Gamma \vdash E_1 \ op \ E_2: bool}

Expr op, op \in {in, not in}

ΓE1:T   ΓE2:listof(S),TSΓE1 op E2:bool\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: listof(S), T \sqsubseteq S}{\Gamma \vdash E_1 \ op \ E_2: bool}

身份运算符

Expr op \in {is, is not}

ΓE1:T   ΓE2:TΓE1 op E2:bool\frac{\Gamma \vdash E_1: T \ \ \ \Gamma \vdash E_2: T}{\Gamma \vdash E_1 \ op \ E_2: bool}

IF Expr

Expr If

ΓE1:boolean   ΓE2:T   ΓE3:TΓif E1 then E2 else E3:T\frac{\Gamma \vdash E_1: boolean \ \ \ \Gamma \vdash E_2: T \ \ \ \Gamma \vdash E_3: T}{\Gamma \vdash if \ E_1 \ then \ E_2 \ else \ E_3: T}

Stmt

Stmt If

ΓE1:boolean   ΓS1:Void   ΓS2:VoidΓif E1 then S1 else S2:Void\frac{\Gamma \vdash E_1: boolean \ \ \ \Gamma \vdash S_1: Void \ \ \ \Gamma \vdash S_2: Void}{\Gamma \vdash if \ E_1 \ then \ S_1 \ else \ S_2: Void}

Stmt Assign

Γid:T0   ΓT1   ΓE:T2Γid:T1 = E:Void\frac{\Gamma \vdash id: T_0 \ \ \ \Gamma \vdash T_1 \ \ \ \Gamma \vdash E: T_2}{\Gamma \vdash id: T_1 \ = \ E : Void}

Type Alias

Γid:T0   ΓT1Γtype id = T1:Void\frac{\Gamma \vdash id: T_0 \ \ \ \Gamma \vdash T_1}{\Gamma \vdash type \ id \ = \ T_1 : Void}

Union

Union 规则

List Union

Γ listof(T)   Γ listof(S)Γ listof(unionof(T,S))\frac{\Gamma \vdash \ listof(T) \ \ \ \Gamma \vdash \ listof(S)}{\Gamma \vdash \ listof(unionof(T, S))}

Dict Union

Γ dictof(T1,T2)   Γ dictof(S1,S2)Γ dictof(unionof(T1,S1),unionof(T2,S2))\frac{\Gamma \vdash \ dictof(T_1, T_2) \ \ \ \Gamma \vdash \ dictof(S_1, S_2)}{\Gamma \vdash \ dictof(unionof(T_1, S_1), unionof(T_2, S_2))}

Struct Union

给定两个结构体 structof(K1:T1,...,Kn:Tn)structof(H1:S1,...,Hm:Sn)structof(K_{1}: T_{1}, ..., K_{n}: T_{n}),structof(H_{1}: S_{1}, ..., H_{m}: S_{n})

定义他们的 union 类型:

structof(J1:U1,...,Jp:Un)=structof(K1:T1,...,Kn:Tn)structof(H1:S1,...,Hm:Sn)structof(J_{1}: U_{1}, ..., J_{p}: U_{n}) = structof(K_{1}: T_{1}, ..., K_{n}: T_{n}) \bigcup structof(H_{1}: S_{1}, ..., H_{m}: S_{n})

例如:

structof()  structof(H1:T1,...,Hm:Tn)=structof(H1:T1,...,Hm:Tn)structof() \ \bigcup \ structof(H_{1}: T_{1}, ..., H_{m}: T_{n}) = structof(H_{1}: T_{1}, ..., H_{m}: T_{n})
structof(K1:T1,...,Kn:Tn)  structof(H1:S1,...,Hm:Sn)=structof(K1:T1)::(structof(K2:T2,...,Kn:Tn)  structof(H1:S1,...,Hm:Sn))structof(K_{1}: T_{1}, ..., K_{n}: T_{n}) \ \bigcup \ structof(H_{1}: S_{1}, ..., H_{m}: S_{n}) = structof(K_1: T_1) :: (structof(K_{2}: T_{2}, ..., K_{n}: T_{n}) \ \bigcup \ structof(H_{1}: S_{1}, ..., H_{m}: S_{n}))

其中把 "::" 表示把一个对偶加入到一个结构的操作,定义如下:

structof(K1:T1)::structof()=structof(K1:T1)structof(K_{1}: T_{1}) :: structof() = structof(K_{1}: T_{1})
structof(K1:T1)::structof(K1:T1,...,Kn:Tn)=structof(K1:union_op(T1,T1),...,Kn:Tn)structof(K_{1}: T_{1}) :: structof(K_{1}: T_{1}', ..., K_n: T_{n}) = structof(K_{1}: union\_op(T_{1}, T_{1}'), ..., K_{n}: T_{n})
structof(K1:T1)::structof(K2:T2,...,Kn:Tn)=structof(K2:T2)::structof(K1:T1)::structof(K3:T3,...,Kn:Tn)structof(K_{1}: T_{1}) :: structof(K_{2}: T_{2}, ..., K_n: T_{n}) = structof(K_{2}: T_2) :: structof(K_{1}: T_1) :: structof(K_{3}: T_3, ..., K_{n}: T_{n})

基于此,两个 Struct 的 union 定义为:

Γstructof(K1:T1,...,Kn:Tn) Γstructof(H1:S1,...,Hm:Sn) structof(J1:U1,...,Jp:Un)=structof(K1:T1,...,Kn:Tn)structof(H1:S1,...,Hm:Sn)Γstructof(J1:U1,...,Jp:Un))\frac{\Gamma \vdash structof(K_{1}: T_{1}, ..., K_{n}: T_{n}) \ \Gamma \vdash structof(H_{1}: S_{1}, ..., H_{m}: S_{n}) \ structof(J_{1}: U_{1}, ..., J_{p}: U_{n}) = structof(K_{1}: T_{1}, ..., K_{n}: T_{n}) \bigcup structof(H_{1}: S_{1}, ..., H_{m}: S_{n})}{\Gamma \vdash structof(J_{1}: U_{1}, ..., J_{p}: U_{n}))}

其中 union_op(T1,T2)union\_op(T_1, T_2) 表示对相同 KiK_i 的不同类型的判断操作:

  • T1T_1T2T_2 有偏序关系时, 如果 T1T2T_1 \sqsubseteq T_2 时,返回 T2T_2,否则返回 T1T_1,即取最小上界
  • T1T_1T2T_2 不存在偏序关系时,有三种可选的处理逻辑:
    • 结构体 union 失败,返回 type_error
    • 返回后者的类型,此处为 T2T_2
    • 返回类型 unionof(T1,T2)unionof(T_1, T_2)

此处需要根据实际需求选择适当的处理方式。

结构体继承可以看做一种特殊的 union,整体逻辑与 union 相似,但在 union_op(T1,T2)union\_op(T_1, T_2) 中对相同 KiK_i 的不同类型的判断操作如下:

  • T1T_1T2T_2 有偏序关系且 T1T2T_1 \sqsubseteq T_2 时,返回 T1T_1,即仅当 T1T_1T2T_2 的下界时以下界 T1T_1 为准
  • 否则返回 type_error

通过这样的继承设计可以实现分层的、自下而上逐层收缩的类型定义。

Operation

KCL 支持对结构体属性进行如 p op E 形式的操作。 即对给定结构体 A:structof(K1:T1,...,Kn:Tn)A: structof(K_{1}: T_{1}, ..., K_{n}: T_{n}), 对结构体中的路径 pE 的值进行指定的操作(如 union,assign,insert 等)。

定义如下更新操作:

ΓA:structof(K1:T1,...,Kn:Tn)  Γp(K1,...,Kn) Γe:Tkk1,...,kknA{p op e}:{K1:T1,...,Kn:Tn}{p:T}\frac{{\Gamma\vdash A: structof(K_{1}: T_{1}, ..., K_{n}: T_{n})}  {\Gamma\vdash p \in (K_{1}, ..., K_{n})} \ {\Gamma\vdash e:T}   k \neq k_1, ..., k \neq k_n} { A \{p \ op \ e\}:\{K_1:T_1, ..., K_n:T_n\}∪\{p:T\}}

即对路径 pp 进行操作本质上是对两个结构体的一种 union,对同名属性类型 union 时的规则根据情况而定。例如路径 pp 是一个可用作字段名的标识符 p=k1p=k_1,并且结构体 A 中字段名也是 k1k_1,它的类型为 T1T_1,并且表达式 ee 的类型也为 T1T_1 ,那么

ΓA:structof(K1:T1,...,Kn:Tn)  Γp=K1 Γe:T1kk1,...,kknA{p op e}:{K1:T1,...,Kn:Tn}\frac{{\Gamma\vdash A: structof(K_{1}: T_{1}, ..., K_{n}: T_{n})}  {\Gamma\vdash p = K_{1}} \ {\Gamma\vdash e:T_1}   k \neq k_1, ..., k \neq k_n} { A \{p \ op \ e\}:\{K_1:T_1, ..., K_n:T_n\}}

注意:

  • 此处表达式 ee 的类型 T1T_1 同原先同名属性 K1K_1 的具有相同的类型。可根据实际情况需要适当放松,如 ee 的类型 T1\sqsubseteq T_1 即可。
  • 对于多层结构体嵌套的操作,递归的使用以上规则即可。

类型偏序

基础类型

Type TType AnyType \ T \sqsubseteq Type \ Any
Type NothingType TType \ Nothing \sqsubseteq Type \ T
Type NothingType BoolType AnyType \ Nothing \sqsubseteq Type \ Bool \sqsubseteq Type \ Any
Type NothingType IntType AnyType \ Nothing \sqsubseteq Type \ Int \sqsubseteq Type \ Any
Type NothingType FloatType AnyType \ Nothing \sqsubseteq Type \ Float \sqsubseteq Type \ Any
Type IntType FloatType \ Int \sqsubseteq Type \ Float
Type NothingType StringType AnyType \ Nothing \sqsubseteq Type \ String \sqsubseteq Type \ Any
Type NothingType LiteralType AnyType \ Nothing \sqsubseteq Type \ Literal \sqsubseteq Type \ Any
Type NothingType ListType AnyType \ Nothing \sqsubseteq Type \ List \sqsubseteq Type \ Any
Type NothingType DictType AnyType \ Nothing \sqsubseteq Type \ Dict \sqsubseteq Type \ Any
Type NothingType StructType AnyType \ Nothing \sqsubseteq Type \ Struct \sqsubseteq Type \ Any
Type NothingType NoneType AnyType \ Nothing \sqsubseteq Type \ None \sqsubseteq Type \ Any
Type NothingType VoidType AnyType \ Nothing \sqsubseteq Type \ Void \sqsubseteq Type \ Any
Type NothingType AnyType \ Nothing \sqsubseteq Type \ Any

字面值类型

Type Literal(Bool)Type BoolType \ Literal(Bool) \sqsubseteq Type \ Bool
Type Literal(Int)Type IntType \ Literal(Int) \sqsubseteq Type \ Int
Type Literal(Float)Type FloatType \ Literal(Float) \sqsubseteq Type \ Float
Type Literal(String)Type StringType \ Literal(String) \sqsubseteq Type \ String

联合类型

Type XType Union(X,Y)Type \ X \sqsubseteq Type \ Union(X, Y)

自反

Type XType XType \ X \sqsubseteq Type \ X

示例

Type BoolType BoolType \ Bool \sqsubseteq Type \ Bool
Type IntType IntType \ Int \sqsubseteq Type \ Int
Type FloatType FloatType \ Float \sqsubseteq Type \ Float
Type StringType StringType \ String \sqsubseteq Type \ String
Type ListType ListType \ List \sqsubseteq Type \ List
Type DictType DictType \ Dict \sqsubseteq Type \ Dict
Type StructType StructType \ Struct \sqsubseteq Type \ Struct
Type NothingType NothingType \ Nothing \sqsubseteq Type \ Nothing
Type AnyType AnyType \ Any \sqsubseteq Type \ Any
Type Union(TypeInt,TypeBool)Type Union(TypeInt,TypeBool)Type \ Union(Type Int, Type Bool) \sqsubseteq Type \ Union(Type Int, Type Bool)

传递

Type XType Z if Type XType Y and Type Y Type ZType \ X \sqsubseteq Type \ Z \ if \ Type \ X \sqsubseteq Type \ Y \ and \ Type \ Y \sqsubseteq \ Type \ Z

包含

Type List(T1)Type List(T2) if T1T2Type \ List(T_1) \sqsubseteq Type \ List(T_2) \ if \ T_1 \sqsubseteq T_2
Type Dict(Tk1,Tv1)Type Dict(Tk2,Tv2) if Tk1Tk2 and Tv1Tv1Type \ Dict(T_{k1}, T_{v1}) \sqsubseteq Type \ Dict(T_{k2}, T_{v2}) \ if \ T_{k1} \sqsubseteq T_{k2} \ and \ T_{v1} \sqsubseteq T_{v1}
Type Structure(K1:Ta1,K2:Ta2,...,Kn:Tan)Type Structure(K1:Tb1,K2:Tb2,...,Kn:Tbn) if Ta1Tb1 and Ta2Tb2 and ... and TanTbnType \ Structure(K_1: T_{a1}, K_2: T_{a2}, ..., K_n: T_{an}) \sqsubseteq Type \ Structure(K_1: T_{b1}, K_2: T_{b2}, ..., K_n: T_{bn}) \ if \ T_{a1} \sqsubseteq T_{b1} \ and \ T_{a2} \sqsubseteq T_{b2} \ and \ ... \ and \ T_{an} \sqsubseteq T_{bn}

继承

Type Struct AType Struct B if A inherits BType \ Struct \ A \sqsubseteq Type \ Struct \ B \ if \ A \ inherits \ B

None

Type NoneType X,X{Type Nothing, Type Void}Type \ None \sqsubseteq Type \ X, X \notin \{Type \ Nothing, \ Type \ Void\}

Undefined

Type UndefinedType X,X{Type Nothing, Type Void}Type \ Undefined \sqsubseteq Type \ X, X \notin \{Type \ Nothing, \ Type \ Void\}

相等性

交换律

Type Union(X,Y)==Type Union(Y,X)Type \ Union(X, Y) == Type \ Union(Y, X)

示例

Type Union(Int,Bool)==Type Union(Bool,Int)Type \ Union(Int, Bool) == Type \ Union(Bool, Int)

结合律

Type Union(Union(X,Y),Z)==Type Union(X,Union(Y,Z))Type \ Union(Union(X, Y), Z) == Type \ Union(X, Union(Y, Z))

示例

Type Union(Union(Int,String),Bool)==Type Union(Int,Union(String,Bool))Type \ Union(Union(Int, String), Bool) == Type \ Union(Int, Union(String, Bool))

幂等性

Type Union(X,X)==Type XType \ Union(X, X) == Type \ X

示例

Type Union(Int,Int)==Type IntType \ Union(Int, Int) == Type \ Int

偏序推导

Type Union(X,Y)==Type Y if XYType \ Union(X, Y) == Type \ Y \ if \ X \sqsubseteq Y

示例

假设 Struct A 继承 Struct B

Type Union(A,B)==Type BType \ Union(A, B) == Type \ B

幂等性是偏序自反的一个特例

List

Type List(X)==Type List(Y) if X==YType \ List(X) == Type \ List(Y) \ if \ X == Y

Dict

Type Dict(Tk,Tv)==Type Dict(Sk,Sv) if Tk==Sk and Tv==SvType \ Dict(T_k, T_v) == Type \ Dict(S_k, S_v) \ if \ T_k == S_k \ and \ T_v == S_v

Struct

Type Struct(K1:T1,K2:T2,...,Kn:Tn)==Type Struct(K1:S1,K2:S2,...,Kn:Sn) if T1==S1 and ... and Tn==SnType \ Struct(K_1: T_{1}, K_2: T_{2}, ..., K_n: T_{n}) == Type \ Struct(K_1: S_{1}, K_2: S_{2}, ..., K_n: S_{n}) \ if \ T_{1} == S_{1} \ and \ ... \ and \ T_{n} == S_{n}

偏序检查

Type X==Type Y if Type XType Y and Type Y Type XType \ X == Type \ Y \ if \ Type \ X \sqsubseteq Type \ Y \ and \ Type \ Y \sqsubseteq \ Type \ X

基础方法

  • sup(t1: T, t2: T) -> T: 根据类型偏序计算两类型 t1, t2 的最小上界。需要动态创建 union type。
  • typeEqual(t1: T, t2: T) -> bool: 比较两类型 t1, t2 是否相等。
  • typeToString(t: T) -> string: 自顶向下递归解析并转化类型成对应的字符串类型。

Sup Function

  • 暂不考虑类型参数,条件类型等特性
  • 使用一个有序集合存储 UnionType 的所有类型
  • 使用一个全局的 Map 根据 UnionType 的名称存储产生的所有 UnionType
  • 根据偏序关系计算类型之间的包含关系
// The Sup function returns the minimum supremum of all types in an array of types
func Sup(types: T[]) -> T {
typeOf(types, removeSubTypes=true)
}

// Build a sup type from types [T1, T2, ... , Tn]
func typeOf(types: T[], removeSubTypes: bool = false) -> T {
assert isNotNullOrEmpty(types)
// 1. Initialize an ordered set to store the type array
typeSet: Set[T] = {}
// 2. Add the type array to the ordered set for sorting by the type id and de-duplication
addTypesToTypeSet(typeSet, types)
// 3. Remove sub types according to partial order relation rules e.g. sub schema types
if removeSubTypes {
removeSubTypes(typeSet)
}
if len(typeSet) == 1 {
// If the typeSet has only one type, return it
return typeSet[0]
}
// 4. Get or set the union type from the global union type map
id := getIdentifierFromTypeSet(typeSet)
unionType := globalUnionTypeMap.get(id)
if !unionType {
unionType = createUnionType(typeSet) // Build a new union type
globalUnionTypeMap.set(id, unionType)
}
return unionType
}

// Add many types into the type set
func addTypesToTypeSet(typeSet: Set[T], types: T[]) -> void {
for type in types {
addTypeToTypeSet(typeSet, type)
}
}

// Add one type into the type set
func addTypeToTypeSet(typeSet: Set[T], type: T) -> void {
if isUnion(type) {
return addTypesToTypeSet(typeSet, toUnionOf(type).types)
}
// Ignore the void type check
if !isVoid(type) {
// De-duplication according to the type of id
typeSet.add(type)
}
}

func removeSubTypes(types: Set[T]) -> void {
for source in types {
for target in types {
if !typeEqual(source, target) {
// If the two types have an inheritance relationship, the base class is retained, or if the two types have a partial order relationship according to the relation table.
if (isPartialOrderRelatedTo(source, target)) {
types.remove(source)
}
}
}
}
}

// isPartialOrderRelatedTo function Determine whether two types have a partial order relationship `source \sqsubseteq target`
// according to the partial order relationship table and rules
func isPartialOrderRelatedTo(source: T, target: T) -> bool {
assert isNotNullOrEmpty(source)
assert isNotNullOrEmpty(target)
if isNoneOrUndefined(source) and !isNothing(target) and !isVoid(target) {
return true
}
if isAny(target) {
return true
}
if typeEqual(source, target) {
return true
}
if isUnion(target) and source in target.types {
return true
}
// Literal Type
if (isStringLiteral(source) and isString(target)) or \
(isBooleanLiteral(source) and isBool(target)) or \
(isIntLiteral(source) and isInt(target)) or \
(isFloatLiteral(source) and isFloat(target)) {
return true
}
if isInt(source) and isFloat(target) {
return true
}
if isList(source) and isList(target) {
return isPartialOrderRelatedTo(toListOf(source).eleType, toListOf(target).eleType
}
if isDict(source) and isDict(target) {
return isPartialOrderRelatedTo(toDictOf(source).keyType, toDictOf(target).keyType) and isPartialOrderRelatedTo(toDictOf(source).valueType, toDictOf(target).valueType)
}
if isStruct(source) and isStruct(target) {
if isTypeDerivedFrom(source, target) {
return true
}
// Empty Object
if len(target.keys) == 0 {
return true
}
if any([key Not in source.keys for key in target.keys]) {
return false
}
for key, sourceType in (source.keys, source.types) {
targetType = getKeyType(target, key) ? getKeyType(target, key) : anyTypeOf()
if !isPartialOrderRelatedTo(sourceType, targetType) {
return false
}
}
return true
}
return false
}

类型检查

类型检查器

类型检查器通过语法制导翻译的方式,自顶向下遍历语法树,并根据上下文有关的定型规则来判定程序构造是否为良类型程序。

类型检查器依赖类型规则,类型环境 Γ\Gamma 的信息记入符号表。对类型表达式采用抽象语法,如 listof(T)。类型检查失败时产生 type_error,并根据语法上下文产生错误信息。

基础方法

  1. isUpperBound(t1, t2): supUnify(t1, t2) == t2
  2. supUnify(t1, t2):
  • 对于基础类型,根据偏序关系计算 sup(t1, t2)
  • 对于 list、 dict、 Struct, 递归地对其中元素的类型进行 supUnify
  • 不存在偏序关系时,返回 Nothing

检查逻辑

Operand Expr

Did:TD \to id: T

env.addtype(id.entry, T.type)

TbooleanT \to boolean

T.type = boolean

TintegerT \to integer

T.type = integer

TfloatT \to float

T.type = float

TstringT \to string

T.type = string

Tc, c{boolean,integer,float,string}T \to c, \ c \in \{boolean, integer, float, string\}

T.type = literalof(c)

TNoneT \to None

T.type = None

TUndefinedT \to Undefined

T.type = Undefined

T [T1]T \to \ [T_1]

T.type = listof (T1.type)

T{T1:T2}T \to { \{T_1: T_2\} }

T.type = dictof (T1.type: T2.type)

T{N1:T1,N2:T2,...,Nn:Tn}T \to { \{N_1: T_1, N2: T_2, ..., N_n: T_n\} }

T.type = structof (N1: T1.type, N2: T2.type, ..., Nn: Tn.type)

EidE \to id

E.type = env.lookup(id.entry)

E[E1,E2,...,En]E \to [E_1, E_2, ..., E_n]

func listExpr(E) {
supe = sup([e.type for e in E]])
E.type = listof(type)
}

E[E1 for E2 in E3 if E4]E \to [E_1 \ for \ E_2 \ in \ E_3 \ if \ E_4]

func listComp(E) {
if !typeEqual(E4.type, boolean) {
raise type_error
}
if !isUpperBound(listof(Any), E3.type) {
raise type_error(E)
}
if !isUpperBound(E3.type, E2.type) {
raise type_error(E)
}
E.type = listof(E1.type)
}

E{Ek1:Ev1,...,Ekn:Evn}E \to \{E_{k1}: E_{v1}, ..., E_{kn}: E_{vn}\}

func dictExpr(E) {
supk := sup([e.type for e in E.keys()]])
supv := sup([e.type for e in E.values()]])
E.type = dictof(supk, supv)
}

E{E1:E2 for (E3,E4) in E5 if E6}E \to \{E_1:E_2 \ for \ (E_3, E_4) \ in \ E_5 \ if \ E_6\}

func dictComp(E) {
if !typeEqual(E6.type, boolean) {
raise type_error(E)
}
if !isUpperBound(dictof(Any, Any), E5.type) {
raise type_error(E)
}
if !isUpperBound(E5.type, dictof(E3.type, E4.type)) {
raise type_error(E)
}
E.type = dictof(E1.type, E2.type)
}

E{Ek1:Ev1,...,Ekn:Evn}E \to \{E_{k1}: E_{v1}, ..., E_{kn}: E_{vn}\}

func dictExpr(E) {
supk := sup(Ek1, ..., Ekn)
supv = sup(Ev1, ..., Evn)
E.type = dictof(supk, supv)
}

E{N1=E1,...,Nn=En}E \to \{N_{1} = E_{1}, ..., N_{{n}} = E_{n}\}

func structExpr(E) {
Struct = structof()
for n, e in E {
Struct.add(n, e.type)
}
E.type = Struct
}

Primary Expr

EE1[E2]E \to E_1[E_2]

func sliceSuffix(E) {
if !isUpperBound(listof(Any), E.E1.type) {
raise type_error(E)
}
if typeEqual(E.E2.type, integer) {
raise type_error(E)
}
E.type = E.E1.type.eleType
}

EE1(E2)E \to E_1(E_2)

func callSuffix(E) {
if !typeEqual(E.E1.type, func) {
raise type_error(E)
}
if !isUpperBound(listof(E.E1.arguType), E.E2.type) {
raise type_error(E)
}
E.type = E.E1.returnType
}

Unary Expr

根据每条双目运算符的推理规则推导,以 '+' 为例

E+E1E \to + E_1

func Plus(E) {
if !typeEqual(E.E1.type, [integer, float]) {
raise type_error(E)
}
E.type = E.E1.type
}

Binary Expr

根据每条双目运算符的推理规则推导,以 '%' 为例

EE1 E \to E_1 \ % \ E_2

func Mod(E) {
if !(typeEqual(E.E1.type, [integer, float]) && typeEqual(E.E2.type, [integer, float])) {
raise type_error(E)
}
E.type = E.E1.type
}

IF Binary Expr

EifE1 then E2else E3E \to if E_1 \ then \ E_2 else \ E_3

func ifExpr(E) {
if !typeEqual(E.type, boolean) {
raise type_error(E)
}
if !typeEqual(E_2.type, E_3.type) {
raise type_error(E)
}
E.type = E_2.type
}

Stmt

Sif E then S1 else S2S \to if \ E \ then \ S_1 \ else \ S_2

func ifStmt(S) {
if !typeEqual(S.E.type, boolean) {
raise type_error(E)
}
if !typeEqual(S.S1.type, S.S2.type) {
raise type_error(E)
}
S.type = S.S1.type
}

Sid:T=ES \to id: T = E

Sid=TES \to id = T E

func assignStmt(S) {
tpe := env.lookup(id.entry)
if tpe != nil && tpe != S.T {
raise type_error(E)
}
if isUpperBound(tpe, E.type) {
raise type_error(E)
}
env.addtype(id.entry, T.type)
}

类型转换

基础定义

通过语法制导翻译的方式,根据运算符特征,对参与运算的值类型进行自动类型转换

转换规则

EE1 op E2,,op{+,,,/,%,,//}E \to E_1 \ op \ E_2, , op \in \{+, -, *, /, \%, **, //\}

func binOp(E) {
if E.E1.type == integer and E.E2.type == integer {
E.type = integer
} else if E.E1.type == integer and E.E2.type == float {
E.type = float
} else if E.E1.type == float and E.E2.type == integer {
E.type = float
} else if E.E1.type == float and E.E2.type == float {
E.type = float
}
}

类型推导

基础定义

  • 在类型信息不完全的情况下类型规则推导、重建类型
  • 自底向上推导并重建数程序中的数据结构类型,如基础类型,list, dict, Struct

基础方法

  1. typeOf(expr, subst): 输入为表达式和代换规则集合,返回 expr 的类型和新的代换规则集合
  2. unifier(t1, t2, subst, expr) 用 t1=t2 尝试代换,如果代换成功(未出现且无冲突),则将 t1=t2 加入 subst 并返回 subst。否则报错已出现或有冲突。

推导逻辑

Eid=E1E \to id = E_1

func assignExpr(E, subst) {
return unifier(E.id.type, E.E_1.type, subst, E)
}

unifier(t1,t2,subst,expr)substunifier(t1, t2, subst, expr) \rightarrow subst

func unifier(t1, t2, subst, expr) {
t1 = applySubstToTypeEquation(t1, subst)
t2 = applySubstToTypeEquation(t2, subst)

if t1 == t2 {
return subst
}

if isTypeVar(t1) {
if isNoOccur(t1, t2) {
addTypeEquationToSubst(subst, t1, t2)
return subst
} else {
raise occurrence_violation_error(t1, t2, expr)
}
}

if isTypeVar(t2) {
if isNoOccur(t2, t1) {
addTypeEquationToSubst(subst, t2, t1)
return subst
} else {
raise occurrence_violation_error(t2, t1, expr)
}
}

if isList(t1) and isList(t2) {
return unifier(toListOf(t1).eleType, toListOf(t2).eleType, subst, expr)
}
if isDict(t1) and isDict(t2) {
dict1of := toDictOf(t1)
dict2of := toDictOf(t2)
subst = unifier(dict1of.keyType, dict2of.keyType, subst, expr)
subst = unifier(dict1of.valueType, dict2of.valueType, subst, expr)
return subst
}
if isStruct(t1) and isStruct(t2) {
Struct1of := tostructof(t1)
Struct2of := tostructof(t2)
for key, _ in Struct1of {
subst = unifier(t1[key].type, t2[key].type, subst, expr)
}
return subst
}

raise unification_error(t1, t2, expr)
}

func applySubstToTypeEquation(t, subst) {
// walks through the type t, replacing each type variable by its binding in the substitution
σ. If a variable is Not bound in the substitution, then it is left unchanged.
if isBasicType(t) {
return t
}
if isList(t) {
return listOf(applySubstToTypeEquation(toListOf(t).eleType, subst))
}
if isDict(t) {
dictof := toDictOf(t)
kT := applySubstToTypeEquation(dictof.keyType, subst)
vT := applySubstToTypeEquation(dictof.valueType, subst)
return dictOf(kT, vT)
}
if isStruct(t) {
structof := tostructof(t)
s := structof()
for key, type in Struct1of {
kT := applySubstToTypeEquation(type, subst)
s.add(key, kT)
}
return s
}
if hasTypeVar(t) {
for tvar in t.vars {
if tvar in subst {
*tvar = subst[tvar]
}
}
}
return t
}

func addTypeEquationToSubst(subst, tvar, t) {
// takes the substitution σ and adds the equation tv = t to it
for _, t in subst {
for tvar in t.vars {
tmp := applyOneSubst(tsvar, tvar, t)
*tvar = tmp
}
}
subst.add(tvar, t)
}

func applyOneSubst(t0, tvar, t1) {
// substituting t1 for every occurrence of tv in t0.
if isBasicType(t0) {
return t0
}
if isList(t0) {
return listOf(applyOneSubst(toListOf(t).eleType, tvar, t1))
}
if isDict(t0) {
dictof := toDictOf(t)
kT := applyOneSubst(dictof.keyType, tvar, t1)
vT := applyOneSubst(dictof.valueType, tvar, t1)
return dictOf(kT, vT)
}
if isStruct(t0) {
structof := tostructof(t)
s := structof()
for key, type in Struct1of {
kT := applyOneSubst(type, tvar, t1)
s.add(key, kT)
}
return s
}
if t0 == tvar {
return t1
}
return t0
}

func isNoOccur(tvar, t) {
// No variable bound in the substitution occurs in any of the right-hand sides of the substitution.
if isBasicType(t) {
return true
}
if isList(t) {
return isNoOccur(tvar, toListOf(t).eleType)
}
if isDict(t) {
dictof := toDictOf(t)
return isNoOccur(tvar, dictof.keyType) and isNoOccur(tvar, dictof.valueType)
}
if isStruct(t) {
structof := tostructof(t)
noOccur := true
for _, type in structof {
noOccur = noOccur and isNoOccur(tvar, type)
}
return noOccur
}
return tvar != t
}

示例

正常推导

T : {
a = 1
b = "2"
c = a * 2
d = {
d0 = [a, c]
}
}

x: T = {
a = 10
}

Occurrence Violation Error

T = {
a = a
}

Type Unification Error

T : {
a = 1
}

T : {
a = "1"
}

Reference