类型、名称与模块

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

类一：类型与形成

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

七内建皆可成类；元类型亦可成类，不设宇宙层。环境中认作元类型之名可为类；透明别名展开，普通值不可因其名而成类。箭头各域与结果皆验，右箭头展平，域中箭头不展；全称以元类型绑定类参而验体；元组逐项验，名随项存。依值之箭（化 A 者「x」而 B，A 为可依之内建值类）与隐值参数（承 A 者「x」而 B）之成，见依值类型依二。

类型应用首须名义构造器，沿 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，皆验为类型；既无隐亦无显而犹调用，拒之。

预读实参之类，惟读六形及其位置包装：自由变量取境中之类，文件定义引用取定义之类，有标之式 A 也 e 取 A 验为类者，e 待正式检查；第四形为单态之函之满参之调 g 于 x1 … 于 xk，须兼三条：g 去位置包装后为局部变量或文件定义引用；g 之类为单态之函（非全称多态）；诸参皆显，k 正合 g 之函类之显参之数。具则取 g 之返类；诸 xi 仍不于此轮合成，推定仍为一遍有序之匹配（「坐待」于（宿主导入 于 …） 赖此推其类参）。第五形为构造之书 「头」【…】（标签函数类型签七）：首去位置包装后为局部变量或文件定义引用、其类为单态之函，则取首之返类（构造之书依签补齐诸参，其果恒为首之返类）；诸项亦不于此轮合成（数据之文 「列」【「软件」【…】，…】 赖此推列之元素之类，提案〇〇〇二八）。第六形为组值 「组值」【「字段」者 值 也，…】（元组构造之节，议四一八）：依诸项合其组类，与正检之作用域合同法，得如 「组类」【「名」乃 文 也，…】 之类；不可合则仍不供 ground 之类（常文与数据之文 「列」【「组值」【…】，…】 无期之类时，赖此自首项推列之元素之类，后项依之而验）。惟于组值之字面本身合之，不及余式。首为多态之函、带 以、偏应用、首为匿名之函或他式之调，仍不供 ground 之类。字面、投影、余复杂应用、无标函数，不在此轮递归合成作 ground；若先已绑定为名，则可读其类，亦可就地书为（类 也 实参）。按实参次序匹配 Ai，再以 R 匹配 E；有后脊则本轮不用终 E。裸函数以全显式函数类代 R 匹配。已读类型仍全称则不作 ground。

未解尚存则拒，报列未定之隐参、函数隐参之名与诸显参之类，并示可标实参之类（实参 属 类），或以「以」依次给之；合一映射之全录，惟详调时书之。此为有序匹配，非全局反复搜索。尽解后，施所有类型实参，逐个正式检查显参对替换 Ai，补调用树。余脊非空继续用结果类；尽则返回，检查模式末须等 E。

故数字字面之多态调用或须以、或须结果期望，先令成名亦可改可推性。要之，隐参之推有三源：变量、定义引用、有标之式、单态之函之饱和调用四种显参之类，及所期之果类；余参欲供其类，书为（类 也 实参）。连化为一组，少授非合法；高阶参数可为函数，不等于偏应用。

依值之箭之实参验与代、隐值参数之实与推，见依值类型依三。

类五：模式

提案 00002 第四步：标准库 数据结构/多态列。豫 之「列」「罄」「缀」，乃内建列（《《内建类型：列》》、《《内建列：罄》》、《《内建列：缀》》）之别名。常结构之较与支内合一，仍规旧列类首（主“豫言”、包名“标准库”、包内此模）为内建列身份，以供旧存与旧接口；物类逐项较之。内建罄、缀仍用旧构造器签与字段之形。

合成所鉴 T，各支独立扩境。构造器开隐参使结果匹配 T，载荷逐项验；新名绑定 T，已识构造名不作新名。数、串、爻常量须合 T；元组须明确元组同数，命名者名须逐项同；列糖已展。模式应用必以构造器为首，不逆任意函数；首为函数则类检报“模式里不能调用函数「名」：模式只能由构造器、字面量与新名组成”，支体仍检。

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

整数索引之细、“无法细化”与依值模式匹配，见依值类型依六。

提案 00002 之分支细化开发规

宿主之界暂拒终果特化之构造器：终果类参必为互异全称之变，不含常量、复合类与重复之变。验此类诸构造器，拒之辞曰“结果类型特化的构造器不能过宿主边界”。待办之事：实作特化构造器之宿主边界转换。

模式之约必不能合，则其支不可达；编译器于支之源码位置警“不可达的匹配分支”，略其体之类检。模中构造器所属之类非所鉴之类者，编译器于模处告误“模式的构造器「名」不属于被鉴值的类型「类」”（带文件与行列），其体仍验，验毕乃并告。合成果类取首可达支；无可达支且无期望类，则不能合成。--no-warnings 止警之输出，仍略不可达支。模中之裸名（构造器而外）一立为新系而蔽其外（议题 212、222）；全局之函、本卷之类名、外层之系与模式之变皆然，内建构造器之名与常值仍依表达式验之。模中之施以函数为首、重绑模式名、强定存在参等寻常之误仍报；以函数为首者，筛可达之支时即报。模之位见正名自他卷所展之类型式者，编译器告定讯，书其卷、行列与源行：其源为裸名，则曰“模式变量「名」与类型「名」同名，换个名字”；源中书 以（…），则曰“模式里不能写类型实参，去掉 以（…）”；源文不可为裸名而模之项为元组、箭或隐式前缀之类，则曰“模式里不能写类型表达式：…”；余则循旧告“不是支持的模式匹配项：…”。前二辞末示模式惟构造、字面与新名可为（议题 #419）。

期望之类明定而诸支皆不可达，仍先求所鉴之式，继抛可捕获之“模式匹配错误，缺少分支”异常。

此段录正验之开发规，施行之状及证见施行记。全 GADT、存在之类及不可达支之验未毕。

构造器所返之类与分析对象之类行双向一阶合一；外境中类为元类型之局部变量，可于本支求解，求解必验其名自现。所得代换施于支之期望返类、局部绑定之类及支体之类参、标注。诸支各立状态，正常返与异常退皆复原状，余支仍用原境。

匹配有明定期望类，乃许此细化。合成匹配仍由首支合返类而检后继诸支；任一支细化外层类变，则告“需类型标注”。后继支由首支所得之类，乃合成算法内部之果，不得据此许细化。局部匹配可用类型判断明期望，如 （「文」也（鉴……））。

存在之类之开发路，先由构造器结果推隐参。结果不能定之参为本支新刚类，字段与随包之函依此类检之；合成支之结果类不得含此新名，否则告“存在类型逃出模式匹配分支”。显式模式类参唯核结果已定之类，不得强定存在之参，亦不得凭其指定而细化泛型构造器之外层索引。跨参组未定之存在参，仍在实现验收之域。

存在之类于隐式模式参中一绑，使检查后支之语法树闭合；复用仍取同一类名。模式转换去其隐绑，运行时构造器字段之次如故。

跨参组之构造器模式，由终构造结果求隐参；读后全称另取新名，将见于终果之有用后继索引纳入推定，唯补今调用组之隐参。后组实绑定仍守同一终索引之约，隐藏类之绑定及逃逸之限遍及全支。

类六：无体之声与宿主之界

无体之声者，签名之后无同名之义之 乃 声，惟许见于词法与语法语四所列之文。语法分析合其体：逐参受之之嵌函，至内为一次内原语之调，实参依次为诸层之参。类型检查依声类检之，并按声明类别改其至内之调：

• 宿主导入（。接口。豫）：依诸参之类与所期之果类算边界签名（形与 Wasm 类之应见网页汇编接口网五），附于内名之末，去类为“有”之实参。算形先展透明之类；整数、小数、爻、字符串、有径应；元组、命名元组依项；列于甲为列；字节串、字节缓冲为串；有构造器之类依其声次列诸支，以类之实参代构造器之类参；接口之文无构造器之类为资；果类 异步返回 于 甲（标准库 语言核心/异步原语。豫）记为异〔甲之形〕，惟许为果之最外。函数之类、全称之类、类变量、列外之递归类、动态分类值，及非接口之文无构造器之类（如引用类），皆报“不能过宿主边界”。
• 内建之声（。内建。豫）：声名须在编译器之原语表，否则报“不在原语表里的内建名”。签名依粗形校之：整数、小数、爻、字符串（字节串、字节缓冲同属串）、有记为整、小、爻、串、元，余类记为任；去元参后，参数与原语表同数，表书“任”之位配诸粗形，余位须同，否则报“内建签名不符”。校通则易为原语之内名（豫言_ 加声名），代码生成就地生令或调运行时。参之次依内原语。
• 底层内建之声（。底层内建。豫）：内名为 底层_ 加声名（声名以“声明”起者易为 声明： 加其余，如「声明存」易为 声明：内存），须在底层后端之原语表（底层定型。豫）、车道原语表或殊处之单，否则报“不在底层原语表里的内建名”。签名依粗形校之：整数与爻记为整，小数记为双，底层库数值类型之长整数、单精度、向量记为长、单、向，字符串记为串，有记为元，余类（类变之属）记为任；去元参后，在原语表者参数须同数，址参配整或长，任配诸类，果之元配整，余位须同，否则报“内建签名与底层原语表不符”。殊处之原语唯校其名。
• 底层导入（。底层接口。豫）：模块名为接口文件之名（去其后缀），字段名为声名，改为 导入：模块：字段：参数：结果；参果书型字之串（整数与爻为整，长整数、单精度、小数、向量为长、单、双、向；无则书零），去类为“有”之实参，果为“有”者无果；他类则报“底层导入的参数与结果只能是整数、爻、长整数、单精度、小数、向量或有”。其义见《底层模式》七。

• 应用接口（。应用接口。豫）：改为“应用接口：包名：函数名：全签名”，全签名并书类为“有”之参（代码生成以此知实现之何参为“有”），实参仍惟留非“有”者。入口定同名顶层之函则编为导出，入口未实而见调则抛可承之异，见网页汇编接口网五。待办之事：未核入口定义之类与应用接口所声之类同否，今恃接口检查器于实现文件之式核之。

标准库之语言原语，皆声于 库/豫章/本原/本术。内建。豫；宿主之务声于 库/豫章/东道。接口。豫 与 宿主带列。接口。豫（导入模块“标准库”）；标准库之公函改调之，公名与参次不易。底层库之原语声于 库/底层库/本术。底层内建。豫，底层库诸模之公函改调之。

名一：作用域

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

鉴 之模中，裸名与构造同者（含构造之值别名）为构造之模；余裸名一立为新系而蔽其外，与本卷之类名、顶层之函、常值同名者亦然（议题 212、222）。既蔽，支体中同名之引归内新系，递归之呼亦取内者（议题 434）。他卷所展之类名居模之位，则依“模之项为类型式”告定讯，模式之变另取一名即可（议题 #419）。

空间者，寻 所立之静态名域，惟居 之 投影之左，不可为参、为返、为类或为数据。空间之名 于名称期消为所指文件中之定义引用，不运行查字段。打开文件新者前加，故后观先查；顶层定义却附于已有绑定末，重复时先项可先中，文件投影亦取首名。不可一概谓所有名称后者胜。须存其不同次序。

名二：导入与包

路径以包名、登记之子包名与包内模块名成之。包根为 名字。包。豫 所在；依赖与子包之登记（「包含在」「包含包」）明列。首段必为本包自身或其直依之名，是为始包；自次段起，段为当前所指包登记之子，则入其子而续，否则余段为所指包内之模块：子先于模块。路径止于包（单名，或止于子）则依其默认导入而展（详下），不聚目录；多段自所指包之根逐级。模块之文先求 模块名。豫，无则次求接口之文 模块名。接口。豫、模块名。应用接口。豫 与内建之声 模块名。内建。豫，又次求着色之源 模块名。着色器。豫（导之得构时所生之模）。着色之文（。着色器。豫、。着色器。接口。豫）之所导，惟求 模块名。着色器。豫 与 模块名。着色器。接口。豫，见着色语言着二。底层之文（名含「。底层」）之所导，惟求 模块名。底层。豫、模块名。底层接口。豫 与 模块名。底层内建。豫；高级之文导此三种底层之模则报错，诸缀尽见文件后缀。未登记之嵌套包仍为界，不可经父路径越之；登记之子，可经父路径引之。源用 。豫，兼容输入亦识 .yuyan。

导入之操作有三：寻载目标之文，而立末段名之静态空间；观纳已导之文所有名于未限定查找，所观之文须已由寻或寻观导之；寻观兼二者。依赖图含所需接口，自导与环导拒，不加载半接口规避。

默认导入者，库包述中「类型」所必书之「默认导入」也：其值为列，可为空列（空列示此包之导必明书模径）。目者，以“/”分段之包内模径（不含缀），或登记之子名；子先于模，子目则递归展其子自身之默认导入；诸目所展之叶模，不许导出同名之义。展为多叶模，则寻以末段绑一空间，对应诸叶模（包名之名 逐叶模求之），观依目之序逐一开之，寻观兼二者；所绑之空间惟末段之一，欲得某目自身之空间者，显寻其模。字段之书与检，见豫构包系统“默认导入”。

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

名三：构造与定序

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

文件接口存类型、值、构造各项。透明存体，值存类与引用，构造存类与身份。编译产物只可装配，不足验新源码。

最终定义列定全局：常源文之顶层为书作常初值之数据，试、脚本、金样别有程序之体（见执行与编译行一）；多态类型擦除可为空占位，不可压序。匿名名有内部计数，换旧对象须携接口清单，不命他方猜之。