类型、名称与模块

不可预设 HM、任意依赖类或自动柯里化；其接受之集及参数之组，或异本基线。

类一：类型与形成

Γ 为有序绑定及文件接口。类有内建、刚性变量、C(P,N,c,K) 名义构造器、构造应用、连续箭头 [A1,…,An,R]（n≥1）、全称 [a1,…,am].B（m≥1）、元组。P 文件身份，N 名，c 类型内号，K 声明类。

七内建皆可成类；元类型亦可成类，不设宇宙层。环境中认作元类型之名可为类；透明别名展开，普通值不可因其名而成类。箭头各域与结果皆验，右箭头展平，域中箭头不展；全称以元类型绑定类参而验体；元组逐项验。

类型应用首须名义构造器，沿 K 消参；显参域须元类型，实参须类；隐式位置惟授隐参。尽后 K 须元类型，否则未足。普通 λ、运行值、未解投影不得任作类型计算首；待定空缺不入正式形成。立可成名义类型，亦可立返回某类型之值构造器。异声明同形，非即相等。

类二：类等与匹配

先依接口展开透明类，不执行普通值函数体。内建同标签，刚名同名，箭头元组同数而逐项等，应用同首同参式而逐项等；全称同数，以同批新鲜刚名开体；名义构造器惟比 P 与 N，今分支忽略 c、K，不可另以编号或声明类加相等之限。

带类型抽象先共换绑定名；与非抽象相比时有局部 η 扩展：依参式以同一新名施非抽象而比。非任意 β 归约。对象子类型检查今惟类等，无普遍宽度子类、协变或动态兜底。

隐参另有 U，映局部待求名至未解或类型。左待求未解则记右项，已解则比旧解，余名刚性；结构递归。尝试失败保进入前映射，不带半成残解；终仍正式验实参。

类三：合成与检查

合成 Γ⊢e⇒A 得类及补后式，检查 Γ⊢e⇐A 得补后式。不能合成不许退动态执行。

首模式支不能合成，不任换支求类；条件之反向尝试另有其则。

类四：调用全法

输入头之 T、h，有序脊 S，可选期望 E。先开 T 前连续全称为新鲜待求名，避环境、实参、期望诸名；次拆显箭头 A1…An→R，非箭头则 n=0。

从 S 首读至多 m 个授以；显参始则依次取 n 个，间插隐参拒。原 S 非空须足，少则拒；原 S 空可取裸函数实例化。余脊留后轮。已给隐参填 U，皆验为类型；既无隐亦无显而犹调用，拒之。

预读实参之类只直读自由变量、文件定义引用及位置包装。字面、复杂应用、无标函数，不在此轮递归合成作 ground；若先已绑定为名，则可读其类。按实参次序匹配 Ai，再以 R 匹配 E；有后脊则本轮不用终 E。裸函数以全显式函数类代 R 匹配。已读类型仍全称则不作 ground。

未解尚存则拒；此为有序匹配，非全局反复搜索。尽解后，施所有类型实参，逐个正式检查显参对替换 Ai，补调用树。余脊非空继续用结果类；尽则返回，检查模式末须等 E。

故数字字面之多态调用或须授以、或须结果期望，先虑成名亦可改可推性。连化为一组，少授非合法；高阶参数可为函数，不等于偏应用。

类五：模式

合成所鉴 T，各支独立扩境。构造器开隐参使结果匹配 T，载荷逐项验；新名绑定 T，已识构造名不作新名。数、串、爻常量须合 T；元组须明确元组同数；列糖已展。模式应用必以构造器为首，不逆任意函数。

绑定仅本支可见。重复绑定、重复默认依基线失败处理，不自变成相等守卫。运行擦类后按标签、常量、字段判；缺支有运行报错，非皆静态穷尽。决策树可异，先后可达之行与默认限制不可异，未选支不行。

名一：作用域

局部绑定近者先。顶层依次解析体，而后添定义；自递归另加局部绑定，普通前向名不因后有定义而合法。当前绑定先于空间，空间先于打开文件。

名 N 若命中空间 N，且其内亦有定义 N，则取该定义，否则纯空间。之在名称期消，不运行查字段。打开文件新者前加，故后观先查；顶层定义却附于已有绑定末，重复时先项可先中，文件投影亦取首名。不可一概谓所有名称后者胜。须存其不同次序。

名二：导入与包

包根为 名字。包。豫 所在；依赖明列。单段查总集，不聚目录；多段自包根逐级；子包为界。源用 。豫，兼容输入亦识 .yuyan。

寻立末段名之空间，观纳未限定查找，诵重导内容；组合依寻观诵之次，不谓观自动寻。依赖图含所需接口，自导与环导拒，不加载半接口规避。

包定位非值 ABI，然输出 P 入符号。混链必须同 P，不擅换工作目录实址。可由定位层供绝对身份、源码及有序依赖，避免类型检查暗寻路径。

名三：构造与定序

同文件同最终返回类型头，此前构造数加一为新号，自一起。剥全称、箭头，再取应用头；异类型插声明不改此号。

文件接口存类型、空间、值、构造各项，重诵存原来源。透明存体，值存类与引用，构造存类与身份。对象文件只可链接，不足验新源码。

最终定义列定全局；多态类型擦除可为空占位，不可压序。匿名名有内部计数，换旧对象须携接口清单，不命他方猜之。