5 多态函数

在编程语言和类型论中，多态（英语：polymorphism）指为不同数据类型的实体提供统一的接口，或使用一个单一的符号来表示多个不同的类型。

如何编写求表长的通用程序？

——用 ML 语言，不必管表中元素的类型。

func length(lptr) = 
    if is_null(lptr) return 0;
    else return length(tail(lptr)) + 1;
// is_null 测试表是否为空
// tail 返回表尾指针

参数化多态

• 多态函数：允许函数参数的类型有多种不同的情况，函数体中语句的执行能适应参数为不同类型的情况
• 多态算符：Ad-hoc 多态，例如数组索引、函数指针、取地址符 & 等都是多态算符

类型变量

• length 的类型可以写成 $\forall$$\alpha$$.\text{list}($$\alpha$$)\to integer$
• 引入类型变量便于讨论未知类型，比如在不要求声明先于使用的语言中：

func deref(p): // 此时不知道 p 的类型 -- 设为 β
    return p↑  // 此时由↑知道 β = pointer(α)，是指向某个 α 类型的指针类型
               // deref 的类型是 ∀α. pointer(α) → α

多态函数类型系统

一个含多态函数的语言

• P → D; E
• D → D; D | id : Q
• Q → $\forall$ type-variable. Q | T // 多态函数
• T → T '→' T | T × T | unary-constructor(T) | basic-type | type-variable | (T) // 引入类型变量
• E → E(E) | E, E | id

basic-type 表示像 boolean 和 integer 这样的基本类型

unary-constructor 表示一元构造符，它允许写出像 pointer(integer) 和 list(integer) 形式的类型

增加一些推理规则

引入类型变量、笛卡儿积类型和多态函数后增加的推理规则

环境规则

现在可以把类型变量 $\alpha$ 加入到定型环境中，而不仅仅是变量到类型的映射

$\displaystyle(Env\ Var)\quad\frac{\Gamma\vdash\diamondsuit,\ \alpha\not\in dom(\Gamma)}{\Gamma,\alpha\vdash\diamondsuit}$

语法规则

$\displaystyle(Type\ Var)\quad\frac{\Gamma_1,\alpha,\Gamma_2\vdash\diamondsuit}{\Gamma_1,\alpha,\Gamma_2\vdash\alpha}$

从环境中得到一个类型变量

$\displaystyle(Type\ Product)\quad\frac{\Gamma\vdash T_1,\Gamma\vdash T_2}{\Gamma\vdash T_1\times T_2}$

说明笛卡尔积类型的语法

$\displaystyle(Type\ Parenthesis)\quad\frac{\Gamma\vdash T}{\Gamma\vdash (T)}$

说明类型表达式外加括号仍然是类型表达式

$\displaystyle(Type\ Forall)\quad\frac{\Gamma,\alpha\vdash T}{\Gamma\vdash \forall\alpha.T}$

说明加上全称量词后形成多态类型

定型规则

$\displaystyle(Exp\ Pair)\quad\frac{\Gamma\vdash E_1:T_1,\Gamma\vdash E_2:T_2}{\Gamma\vdash E_1,E_2:T_1\times T_2}$

说明笛卡尔积类型的定型规则

$\displaystyle(Exp\ FunCall)\quad\frac{\Gamma\vdash E_1:T_1\to T_2,\ \ \ \ \Gamma\vdash E_2:T_3}{\Gamma\vdash E_1(E_2):S(T_2)}$（$S$ 是 $T_1$ 和 $T_3$ 的最一般的合一代换）

说明多态函数调用的定型规则

$\displaystyle(Exp\ Id\ Fresh)\quad\frac{\Gamma\vdash \forall \alpha.T,\ \ \ \Gamma,\alpha_i\vdash\diamondsuit}{\Gamma,\alpha_i\vdash [\alpha_i/\alpha]T}$（类型变量换名，$\alpha_i$ 不在 $\Gamma$ 中）

多态类型的函数标识符在使用时要去掉全称量词，用一个新的类型变量代替约束变量

记号 $[\alpha_i/\alpha]T$ 表示 $T$ 中自由出现的 $\alpha$ 用 $\alpha_i$ 代换后的结果

代换和实例

代换：用 类型表达式中的类型变量 所代表的 类型表达式 替换之

subst (t : type_exp, Sv : type_var → type_exp) : type_exp

Sv 是一个代换，其规定了类型表达式与类型表达式之间的映射，如果没有规定，代换的结果为恒等映射

type_exp subst(t: type_exp) { // 这里省略了Sv，下面递归调用都使用相同的 Sv
    if (t是基本类型)
        return t;
    else if (t是类型变量)
        return S(t);
    else if (t是t1→t2)
        return subst(t1) → subst(t2);
}

实例：用 $S(t)$ 表示 subst 用于 t 后所得的类型表达式，这个结果叫做 $t$ 的实例

例子

$s<t$ 表示 s 是 t 的实例，$\alpha,\beta$ 是类型变量

• $pointer(integer)<pointer(\alpha)$
• $integer→integer<\alpha→\alpha$
• $pointer(\alpha)<\beta$
• $\alpha<\beta$

下面左边的类型表达式不是右边的实例

左边	右边	原因
integer	real	代换不能用于基本类型
integer → real	$\alpha→\alpha$	$\alpha$ 的代换不一致
integer → $\alpha$	$\alpha→\alpha$	$\alpha$ 的所有出现都应该代换

合一

如果存在某个代换 $S$ 使得 $S(t_1)=S(t_2)$，则称类型表达式 $t_1,t_2$ 能够合一

最一般的合一代换满足

• $S(t_1)=S(t_2)$
• 对任何其他满足 $S'(t_1)=S'(t_2)$ 的代换 $S'$，代换 $S'(t_1)$ 都是 $S(t_1)$ 的实例

例子

• $t_1=pointer(list(\alpha))\quad t_2=pointer(\beta)$
• $S:\alpha\to\alpha,\beta\to list(\alpha)$，则 $S(t_1)=S(t_2)=pointer(list(\alpha))$
• $S':\alpha\to integer,\beta\to list(integer)$，则 $S'(t_1)=S'(t_2)=pointer(list(integer))$
• 这里 $S$ 是最一般的合一代换

多态函数类型检查

多态函数和普通函数在类型检查上的区别

同一多态函数的不同出现不要求变元/参数有相同类型

• 比如 $deref(deref(p))$ 中两层 deref 作用的是不同的类型

必须把类型相同的概念推广到类型合一

• 比如类型为 $s\to s'$ 的 $E_1$ 作用于类型为 $t$ 的 $E_2$，不是简单地确定 s 和 t 是否相同，而要看二者是否合一

要记录类型表达式合一的结果

• 比如 $s\to s'$，如果指派某个变量 $\alpha$ 为类型 $t$，在今后的检查过程中都要保证 $\alpha$ 被指派为类型 $t$

检查多态函数的翻译方案

• E → E~1~(E~2~)

p = mkLeaf(new_type_var); // 因为不知道返回值是什么类型，以类型变量p代替
unify(E1.type, mkNode('→',E2.type,p));  // 将E1的类型与E2→p类型合一
E.type = p; // 检查成功

• E → E~1~, E~2~

E.type = mkNode('×',E1.type,E2.type);

• E → id

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

• $fresh(t)$：把 t 所指的类型表达式中的约束变量用新的变量代替，返回指向替换后的类型表达式的指针
• $unify(m, n)$：合一 m 和 n 所指向的类型表达式，并且记住代换（副作用），也就是记住合一采用的代换

例子1

以语句 deref ( deref ( q ) ) 为例，已知 q 是 pointer ( pointer (int) ) 类型

表达式 ：类型	记录代换
q : pointer ( pointer ( int ) )
deref~i~ : pointer ( α~i~ ) → α~i~
deref~i~ ( q ) : pointer ( int )	α~i~ = pointer ( int )
deref~o~ : pointer ( α~o~ ) → α~o~
deref~o~(deref~i~ (q)) : int	α~o~ = int

例子2

func length(lptr) = 
    if null(lptr) then 0
    else length(tl(lptr)) + 1;

求表长的函数的检查

类型声明

• $length:\beta$
• $lptr:\gamma$
• $if:\forall\alpha.boolean\times\alpha\times\alpha→\alpha$
• $null:\forall\alpha.list(\alpha)\to boolean$
• $tl:\forall\alpha.list(\alpha)→list(\alpha)$
• $0:integer\quad 1:integer$
• $match:\forall \alpha.\alpha\times\alpha→\alpha$

match (
    length(lptr), if(null(lptr), 0, length(tl(ptr))+1)
)

行	定型断言	记录代换	规则
1	$length:\beta$		Exp Id
2	$lptr:\gamma$		Exp Id
3	$length(lptr):\delta$	$\beta=\gamma→\delta$	Exp FunCall
4	$lptr:\gamma$		2
5	$null:list(\alpha_n)\to boolean$		Exp Id, Type Fresh
6	$null(lptr):boolean$	$\gamma=list(\alpha_n)$	Exp FunCall
7	$0 : integer$		Exp Num
8	$lptr:list(\alpha_n)$		2
9	$tl:list(\alpha_t)\to list(\alpha_t)$		Exp Id, Type Fresh
10	$tl(lptr):list(\alpha_n)$	$\alpha_t=\alpha_n$	Exp FunCall
11	$length:list(\alpha_n)→\delta$		1
12	$length(tl(lptr)):\delta$		Exp FunCall
13	$1:integer$		Exp Num
14	$+:integer\times integer\to integer$		Exp Id
15	$length(tl(lptr))+1:integer$	$\delta=integer$	Exp FunCall
16	$if:boolean\times \alpha_i\times\alpha_i\to \alpha_i$		Exp Id, Type Fresh
17	$if (...):integer$	$\alpha_i=integer$	Exp FunCall
18	$match:\alpha_m\times\alpha_m→\alpha_m$		Exp Id, Type Fresh
19	$match(...):integer$	$\alpha_m=integer$	Exp FunCall

length 函数的类型是：$\forall\alpha.list(\alpha)\to integer$

函数和算符重载

例如：加法算符 + 可用于不同类型，“+” 是多个函数的名字，而不是一个多态函数的名字

重载的消除：在重载符号的引用点，其含义能确定到唯一

本文阅读量