type.tex

%!TEX root = x.tex

\rSec0[typesystem]{类型系统}

\begin{bnf}{Type}
    NormalType \br
    ResultType
\end{bnf}

\begin{bnf}{NormalType}
    \terminal{(} Type \terminal{)} \br
    FundaType \br
    SpecialType \br
    CompType \br
    OpaqueType \br
    SomeType \br
    AnyType \br
    \terminal{typeof} \terminal{(} Expression \terminal{)} \br
    Type TypeQualifier
\end{bnf}

\begin{bnf}{TypeQualifier}
    \terminal{mut} \br
    \terminal{const}
\end{bnf}

$$ \mathcal{V} = \{ \langle v, T, Q \rangle \mid T \in \mathcal{T}, v \in T, Q \subset \mathcal{Q} \} $$

\pnum
\term{类型}是一个集合。\term{值}是类型、类型的成员和修饰符集合的元组。$T$称为值$v$的\term{类型}。

\rSec1[type.funda]{基本类型}
\indextext{类型!基本类型}

\begin{bnf}{FundaType}
    \terminal{void} \br
    \terminal{never} \br
    \terminal{bool} \br
    \terminal{int} \br
    \terminal{uint} \br
    \terminal{int} \terminal{<} Expression \terminal{>} \br
    \terminal{uint} \terminal{<} Expression \terminal{>} \br
    \terminal{float} \br
    \terminal{float} \terminal{<} Expression \terminal{>} \br
    \terminal{char} \br
    \terminal{string} \br
    SymbolType
\end{bnf}

$$\tcode{void} \coloneqq \{ \mathrm{void} \}$$

\pnum
\tcode{void}标识只有唯一一个值的类型。

$$\tcode{never} \coloneqq \{ \}$$

\pnum
\tcode{never}标识没有值的类型。

$$\tcode{bool} \coloneqq \{ \mathrm{false}, \mathrm{true} \}$$

\pnum
\tcode{bool}标识具有假（\tcode{false}）或真（\tcode{true}）两个值的类型。

\pnum
\tcode{true}的二进制表示为\tcode{0x01}，\tcode{false}为\tcode{0x00}。持有其他二进制表示的\tcode{bool}类型的值是未定义的。

\pnum
\tcode{bool}是有序的，其中\tcode{false}小于\tcode{true}。

$$\tcode{int}_{l,h} \coloneqq \{ x \in \mathcal{Z} \mid l \le x \le h \} $$

\pnum
$\tcode{int}_{l,h}$称作\term{整数类型}，其中$l$和$h$为待推导常数。在本规范中，如果$l = h$，则记作$\tcode{int}_l$。存在实现定义的常数$m$和$M$。$l$和$h$须满足
$$ l \ge m $$
$$ h \le M $$
$$ 0 \le h - l \le M $$

\tcode{uint}是$\tcode{int}_{l,h}$的别名，但满足$l\ge0$。

\pnum
\tcode{int<$w$>}是$\tcode{int}_{l,h}$的别名，但满足$l\ge-2^{w-1}$且$h\le2^{w-1}-1$。\tcode{uint<$w$>}是$\tcode{int}_{l,h}$的别名，但满足$l\ge0$且$h\le2^w-1$。其中$w$可以取8、16、32、64或128。它们称作\tcode{定长整数类型}，表示长度固定的整数。只能在定长整数类型上进行位运算。

$$ \tcode{float<}s\tcode{>}^\ast \subset \mathcal{R} $$
$$ \tcode{float<}s\tcode{>}^\dagger \subset \{ +\infty, -\infty, \mathrm{NaN}s \} $$
$$ \tcode{float<}s\tcode{>} \coloneqq \tcode{float<}s\tcode{>}^\ast \cup \tcode{float<}s\tcode{>}^\dagger $$

\pnum
\tcode{float<$s$>}称作\term{浮点类型}，其中$s$可以取实现定义的值（典型值为16、32、64或128）。
\tcode{float}为\tcode{float<64>}的别名。

\pnum
整数类型、定长整数类型和浮点类型称为\term{算术类型}。

$$\tcode{char} \coloneqq \left\{ \textnormal{Any Unicode scalar value} \right\}$$

\pnum
\tcode{char}表示一个Unicode标量值。值不在Unicode标量值范围内的\tcode{char}（例如，其值为代理项）是未定义的。

$$\tcode{string} \coloneqq \left\{ \textnormal{Any UTF-8 String} \right\} $$

\pnum
\tcode{string}表示任意长度的UTF-8字符串，包括空字符串。

\rSec2[type.symbol]{符号类型}
\indextext{类型!符号}

\begin{bnf}{SymbolType}
    SymbolLiteral \br
    \terminal{'(} UnqualID \terminal{)}
\end{bnf}

$$ \tcode{'}s \coloneqq \left\{ \langle \tcode{'}s, \tcode{'}s \rangle \right\} $$

$$ \tcode{Symbol} \coloneqq \bigcup_{\tcode{'}s} \left\{  \tcode{'}s \right\} $$

\pnum
符号字面量的类型与其值相同。\tcode{Symbol}是符号字面量的公共类型。参见~\ref{core.type}。

\rSec2[type.special]{特殊类型}
\indextext{类型!特殊类型}

\begin{bnf}{SpecialType}
    \terminal{self}
\end{bnf}

\pnum
\tcode{self}在特征或实现中代表当前类型。在此之外使用\tcode{self}是一个编译错误。

\rSec1[type.comp]{复合类型}
\indextext{类型!复合类型}

\begin{bnf}{CompType}
    Type \terminal{?} \br
    Type \terminal{[} \terminal{]} \br
    Type \terminal{[} Type \terminal{]} \br
    StructType \br
    FuncType \br
    UnionType \br
    Type \terminal{\&} \br
    FuncType \br
    OpaqueType
\end{bnf}

\rSec2[type.optional]{可空类型}
\indextext{类型!可空}

$$ T\tcode{?} \coloneqq \{ \langle t \rangle \mid t \in T \} \cup \{ \mathrm{nil} \} $$

\pnum
\tcode{$T$?}为\term{可空类型}。
\tcode{$T$?}要么包含一个$T$的值（使用\tcode{some}标识），要么不包含任何值（使用\tcode{nil}标识）。

\pnum
可空类型在核心库中对应\tcode{core::Optional}。参见~\ref{core.type}。

\rSec2[type.array]{数组类型}
\indextext{类型!数组}

$$ T\tcode{[]} \coloneqq \bigcup^\infty_{i=1} T^i $$

\pnum
\tcode{$T$[]}为\term{数组类型}，代表有限个类型$T$的值的序列。

\pnum
数组类型在核心库中对应\tcode{core::Array}。参见~\ref{core.type}。

\rSec2[type.dict]{字典类型}
\indextext{类型!字典}

$$ T\tcode{[}K\tcode{]} \coloneqq T^K $$

\pnum
\tcode{$T$[$K$]}为\term{字典类型}，代表键类型$K$到值类型$T$的映射。

\pnum
字典类型在核心库中对应\tcode{core::Dictionary}。参见~\ref{core.type}。

\rSec2[type.struct]{结构类型}
\indextext{类型!结构}

\begin{bnf}{StructType}
    \terminal{(} \terminal{)} \br
    \terminal{(} StructTypeList \terminal{,}\bnfq \terminal{)}
\end{bnf}

\begin{bnf}{StructTypeList}
    UnnamedStructType \br
    UnnamedStructType \terminal{,} NamedStructType \br
    NamedStructType
\end{bnf}

\begin{bnf}{UnnamedStructType}
    StructTypeQualifier\bnfs Type \br
    UnnamedStructType \terminal{,} StructTypeQualifier\bnfs Type
\end{bnf}

\begin{bnf}{NamedStructType}
    StructTypeQualifier\bnfs Identifier \terminal{:} Type InitialValue\bnfq \br
    NamedStructType \terminal{,} StructTypeQualifier\bnfs Identifier \terminal{:} Type InitialValue\bnfq
\end{bnf}

\begin{bnf}{StructTypeQualifier}
    \terminal{mut}
\end{bnf}

\begin{bnf}{TypeNotation}
    \terminal{:} Type
\end{bnf}

\begin{bnf}{InitialValue}
    \terminal{=} Expression
\end{bnf}

$$ \tcode{(} T_1 \tcode{,} \ldots \tcode{,} T_m \tcode{,} K_1 \tcode{:} U_1 \tcode{,} \ldots \tcode{,} K_n \tcode{:} U_n \tcode{)} \coloneqq \prod^m_{i=1} T_i \times \prod^n_{j=1} U_j $$
$$ \tcode{()} \coloneqq \tcode{void} $$

\pnum
\tcode{($T_1$, $\ldots$, $T_m$, $K_1$:$U_1$, $\ldots$, $K_n$:$U_n$)}称作\term{结构类型}。
结构类型包含顺序成员和命名成员，其中顺序成员可以使用索引访问，命名成员可以使用标识符访问。
如果结构类型不包含任何命名成员，则它称为\tcode{元组类型}。

\pnum
特别地，只有一个元素的元组需表示为\tcode{($T$,)}。没有元素的元组与\tcode{void}等价。

\pnum
命名成员可以具有默认值。具有默认值的成员在初始化的时候可以省略而使用默认值。

\rSec2[type.ref]{引用类型}
\indextext{类型!引用}

\pnum
引用类型是另一个值的引用。

\rSec2[type.func]{函数类型}
\indextext{类型!函数}

\begin{bnf}{FuncType}
    ParameterInType FuncTypeQual\bnfs ReturnType \br
    Type FuncTypeQual\bnfs ReturnType
\end{bnf}

\begin{bnf}{ParameterInType}
    \terminal{(} ParamListInType\bnfq \terminal{)}
\end{bnf}

\begin{bnf}{ParamListInType}
    ThisParamDeclInType \br
    ThisParamDeclInType \terminal{,} NamedParamListInType \br
    ThisParamDeclInType \terminal{,} UnnamedParamListInType \br
    ThisParamDeclInType \terminal{,} UnnamedParamListInType \terminal{,} NamedParamListInType \br
    UnnamedParamListInType \br
    UnnamedParamListInType \terminal{,} NamedParamListInType \br
    NamedParamListInType
\end{bnf}

\begin{bnf}{UnnamedParamListInType}
    UnnamedParamDeclInType \br
    UnnamedParamListInType \terminal{,} UnnamedParamDeclInType
\end{bnf}

\begin{bnf}{NamedParamListInType}
    NamedParamDeclInType \br
    NamedParamListInType \terminal{,} NamedParamDeclInType
\end{bnf}

\begin{bnf}{UnnamedParamDeclInType}
    ParamQual\bnfq Type \br
    ParamQual\bnfq Identifier \terminal{:} Type\bnfq
\end{bnf}

\begin{bnf}{NamedParamDeclInType}
    ParamQual\bnfq \terminal{(} Identifier \terminal{)} Type\bnfq \br
    ParamQual\bnfq \terminal{(} Identifier \terminal{)} Identifier \terminal{:} Type\bnfq
\end{bnf}

\begin{bnf}{ThisParamDeclInType}
    \terminal{this} \terminal{:} Type
\end{bnf}

\begin{bnf}{FuncTypeQual}
    ThrowQual \br
    \terminal{async} \br
    \terminal{unsafe} \br
    \terminal{mut} \br
    \terminal{once}
\end{bnf}

\pnum
\tcode{($T_1$, $\ldots$, $T_m$, $K_1$:$U_1$, $\ldots$, $K_n$:$U_n$) -> $R$}称作\term{函数类型}。函数类型标识能以函数方式调用的值。
如果函数只有一个顺序参数，则可以省略括号。

\pnum
函数类型可以包含显式指定类型的\tcode{this}参数。在这种情况下，函数可以在动态成员访问表达式中作为方法被调用。

\pnum
如果函数类型包含\tcode{once}修饰符，则它只能调用一次，随后值会被消耗，它实现了\tcode{core::ops::FunctorOnce}。
如果函数类型包含\tcode{mut}修饰符，则对它的调用将会更改其值，它实现了\tcode{core::ops::FunctorMut}。
如果函数类型不包含这两种修饰符，则对它的调用不会更改其值，它实现了\tcode{core::ops::Functor}。函数均具有此类函数类型。

\rSec1[type.opaque]{不透明类型}
\indextext{类型!不透明}

\begin{bnf}{OpaqueType}
    \terminal{class} Type
\end{bnf}

\pnum
不透明类型用于从现有的类型出发构造一个相同但不能混用的类型。类型$T$与其构造的不透明类型$U$之间不具有隐式转换，但可以显式转换。同一个类型构造的复数个不透明类型之间也不能混用。

\pnum
不透明类型会继承原类型的
\begin{itemize}
    \item 成员访问（顺序成员和命名成员），但这些成员的默认访问级别会更改为\tcode{private}；
    \item 固有实现；
    \item 所有特征实现（以及所有运算符）。
\end{itemize}

\enterexample
\begin{codeblock}

type T = class int;
type U = class int;

let i = 0;
let j: T = i; // 错误，\tcode{int}不能隐式转换为\tcode{class int}
let k: T = i as T; // 可以，显式转换
let m: U = j; // 错误，\tcode{T}和\tcode{U}之间没有隐式转换

\end{codeblock}
\exitexample

\rSec1[type.impl]{\tcode{impl}类型}
\indextext{类型!\tcode{impl}}

\begin{bnf}{SomeType}
    \terminal{impl} Type \br
    \terminal{impl} \terminal{_}
\end{bnf}

\pnum
\tcode{impl $T$}标识一个静态待推导类型，但保证该类型为$T$的子类型。
它可以出现在具有初始化值的绑定的类型中或函数返回值处。
\tcode{impl _}代表一个基础类型待推导的\tcode{impl}类型。

\pnum
\tcode{impl}还能用于简化泛型函数声明。参见~\ref{generic.impl}。

\enterexample
\begin{codeblock}

trait T { }
type A { }
type B { }

impl A : T { }
impl B : T { }

let x: impl T = A(); // \tcode{x}的类型是\tcode{A}
let mut y: impl T = B(); // \tcode{y}的类型是\tcode{B}

y = x; // 错误，\tcode{B}不能赋给\tcode{A}

\end{codeblock}
\exitexample

\rSec1[type.dyn]{\tcode{dyn}类型}
\indextext{类型!\tcode{dyn}}

\begin{bnf}{AnyType}
    \terminal{dyn} Type \br
    \terminal{dyn} \terminal{_} \br
    \terminal{dyn}
\end{bnf}

\pnum
\tcode{dyn $T$}对$T$的子类型进行包装，保证在运行时可以接受任何为$T$的子类型的值。
\tcode{dyn _}代表一个基础类型待推导的\tcode{dyn}类型。
\tcode{dyn}表示对任意类型的包装。

\enterexample
\begin{codeblock}

trait T { }
type A { }
type B { }

impl A : T { }
impl B : T { }

let x: dyn T = A { }; // \tcode{x}的类型是\tcode{dyn T}
let mut y: dyn T = B { }; // \tcode{y}的类型是\tcode{dyn T}

y = x; // 正确，\tcode{dyn T}之间可以互相赋值

\end{codeblock}
\exitexample

\rSec1[type.result]{结果类型}
\indextext{类型!结果类型}

\begin{bnf}{ResultType}
    NormalType \terminal{!!} NormalType
\end{bnf}

\pnum
结果类型\tcode{$T$ !! $E$}标识一个可能产生错误的值，其中$T$是正常的返回值类型，$E$是错误类型，且必须实现\tcode{ErrorCode}。

\rSec1[type.named]{具名类型}

\begin{bnf}{TypeName}
    \terminal{(} Type \terminal{)} \br
    EntityID \br
    FundaType \br
    SpecialType \br
    \terminal{typeof} \terminal{(} Expression \terminal{)}
\end{bnf}

\pnum
\term{类型名称}在特定的语法位置表示类型，以避免潜在的语法歧义。

\rSec1[subtype]{子类型}
\indextext{类型!子类型}

\pnum
类型$A$可能是类型$B$的\term{子类型}，记作$A \preceq B$。$A$可以在需要$B$的上下文中隐式转换到$B$。

\pnum
子类型关系具有自反性和传递性，即对任意类型$A$、$B$和$C$有$A \preceq A$和$A \preceq B \land B \preceq C \implies A \preceq C$成立。

\begin{equation*}
\begin{aligned}
    T \preceq　\tcode{void},& T \in \mathcal{T} \\
    \tcode{never} \preceq T,& T \in \mathcal{T}
\end{aligned}
\end{equation*}

\pnum
任何类型都是\tcode{void}的子类型。\tcode{never}是任何类型的子类型。

\begin{equation*}
\begin{aligned}
I_{l_1,h_1} &\preceq J_{l_2,h_2} \mathrel{\mathrm{if}} l_1 \geq l_2 \lor h_1 \leq h_2 \\
    \tcode{float<}s_1\tcode{>} &\preceq \tcode{float<}s_2\tcode{>} \mathrel{\mathrm{if}} s_1 \leq s_2 \\
I_{l,h} &\preceq \tcode{float<}s\tcode{>} \\
    I, J &\in \left\{ \tcode{int}, \tcode{uint}, \tcode{int<}w\tcode{>}, \tcode{uint<}w\tcode{>} \right\}
\end{aligned}
\end{equation*}

\pnum
范围更小的整数类型是范围更大的整数类型的子类型。长度更小的浮点类型是长度更大的浮点类型的子类型。

\pnum
整数类型是浮点类型的子类型。当整数被隐式转换为浮点数时，其值将被转换为最接近的浮点数。\enternote 虽然整数转换到浮点数可能无法保持值不变，但出于习惯仍然保持这个隐式转换。 \exitnote \enternote 浮点类型不能隐式转换到整数类型，但可以显式转换。 \exitnote

$$ \tcode{'}s \preceq \tcode{Symbol} $$

\pnum
所有符号字面量类型都是\tcode{Symbol}的子类型。

\pnum
\tcode{bool}没有语言内建的子类型约束。但是，其他类型的值可以在\tcode{if}表达式中当作条件使用，这通过实现\tcode{Condition}完成。

\begin{equation*}
\begin{aligned}
T &\preceq T\tcode{?} \\
T\tcode{[]} &\preceq U\tcode{[]} \mathrel{\mathrm{if}} T \preceq U \\
T\tcode{[}K\tcode{]} &\preceq U\tcode{[}L\tcode{]} \mathrel{\mathrm{if}} T \preceq U \mathrel{\mathrm{and}} K \preceq L \\
\end{aligned}
\end{equation*}

\pnum
任意类型是其对应可空类型的子类型。如果$T_i$是$U_i$的子类型，则\tcode{$T_0$[]}、\tcode{$T_0$[$T_1$]}、\tcode{($T_1$, $\ldots$, $T_n$)}分别是\tcode{$U_0$[]}、\tcode{$U_0$[$U_1$]}、\tcode{($U_1$, $\ldots$, $U_n$)}的子类型。\enternote 这意味着数组和字典的元素类型是协变的。 \exitnote

\pnum
对两个结构类型$T$和$U$而言，如果
\begin{itemize}
    \item $T$的顺序成员数量小于或等于$U$的；
    \item $T$的顺序成员是对应$U$顺序成员的子类型；
    \item $T$的命名成员是对应$U$命名成员的子类型，或具有默认值；
\end{itemize}
则$U$是$T$的子类型。

\pnum
对两个函数类型$T$和$U$而言，如果$U$的每个参数类型都是对应$T$的参数的子类型，且$T$的返回类型是$U$的返回类型的子类型，则$T$是$U$的子类型。\enternote 这意味着函数类型的参数类型是逆变的，返回类型是协变的。 \exitnote $T$可以拥有比$U$更多的顺序参数，或者$U$不包含的命名参数。

\pnum
类类型可以定义类型转换函数。每个这样的函数定义了一个子类型关系。

\pnum
对类型表达式而言，$T\mathbin{\tcode{\&}}U$是$T$和$U$的子类型；$T$和$U$是$T\mathbin{\tcode{|}}U$的子类型。

\rSec1[type.common]{公共类型}
\indextext{类型!公共类型}

\pnum
对两个类型$A$和$B$而言，存在一个唯一的类型$C$称为$A$和$B$的\term{公共类型}。$C$满足：

\begin{equation}
\begin{aligned}
    A &\preceq C \\
    B &\preceq C \\
    \forall D \in \mathcal{T}, A &\preceq D \land B \preceq D \Rightarrow C \preceq D
\end{aligned}
\end{equation}

记作 $C = A \otimes B$。公共类型满足交换律。

\pnum
如果$A \preceq B$，则$A \otimes B = B$。

\pnum
如果$A$和$B$之间没有子类型关系，则$A \otimes B = A \mathbin{\tcode{|}} B$。

\rSec1[qualifier]{修饰符}
\indextext{修饰符}

\pnum
值除了总是具有类型之外，还可能带有一个或数个修饰符。修饰符指示了值的其他属性。

\pnum
类型可以带有修饰符，指定该值需有特定的修饰符约束。

\rSec2[qual.mut]{\tcode{mut}}
\indextext{修饰符!\idxcode{mut}}

\pnum
\tcode{mut}表示该值是可变的。具有\tcode{mut}的值才能成为赋值操作符的左操作数。参见~\ref{expr.assign}。

\rSec2[qual.const]{\tcode{const}}
\indextext{修饰符!\idxcode{const}}

\pnum
\tcode{const}表示该值是一个常量值，于编译期间确定且不可变。部分语言功能只允许常量值。

\pnum
\tcode{const}绑定创建一个常量并插入当前作用域。该绑定的初始值必须是常量表达式。