依值之类

此篇记提案 00002 第五步之依值规则：类可依整数、爻、字符串及其列之值。与汉语稿相应。索引式之形与闭合之较，见整数类型索引、爻类型索引、字符串类型索引、列表类型索引。

依一：书法

「定长表」立化「整数」而化「元类型」而「元类型」也。
「新定长表」乃承「甲」而化「甲」而化「整数」者「长」而（「定长表」于「长」于「甲」）也。
「读定长表」乃承「整数」者「长」而承「甲」而
  化（「定长表」于「长」于「甲」）而化（「下标」于「长」）而「甲」
也。

化 A 者「x」而 B：A 为可依之内建值类（整数、爻、字符串，或元仍为此诸类之列），则造依值之箭，B 可及 x；B 不及 x，则为常箭。A 为元类型，则告“化〇者□而〇的定义域不能是元类型”，类参书为 承「甲」而 …。
承 A 者「x」而 B：A 为元类型，则为隐类参，同 承「x」而 B；否则为隐值参数，编后擦之。
有签之依值箭书为 化「签」为 A 者「x」而 B，签依位核之，绑名依换名较之。隐值参数不设签。
化 A 者「x」而化 B 而 C 仍为一组二参之箭，满参之规不易。

依二：类之成

依值箭与隐值参数之定义域，先依参数定义域验之（存其签），去签后须为可依之内建值类，否则告“依值参数的定义域须为整数、爻、字符串或它们的列表”。绑名以此类入境，乃验值域。值域中类构造器之索引实参，依诸索引篇验为索引式。

依三：施

显组含依值箭，则依值之位之实参先核签、依定义域验之，且须为索引式，否则告“类型中的整数参数须为索引式；其他实参先用虑绑定”之属。去源码之标后之验果，代入其后诸位之定义域与果类；后之推定、实参之验与果类，皆用代入后之类。
类型与模块类四第四步读单态之函满参之调之返类，亦先代依值实参。
隐类参与隐值参数可相间，逐一实为待求之名；授以 所给之隐值实参依定义域验其物。
推定仍为有序之配：待求之索引变量惟独见时求之（向量于维 对 向量于三 得维＝三）；含未解待求变量之复索引式（如 加左右）姑不较，待隐参代入后之终验。惟见于复式之隐参不可推，须以 授以 给之。
隐参不可定，则先重行诸接地之较而不吞其错，类有不合则告其不合。

依四：拉姆达

会「x」而 e 对依值箭验之：x 以定义域之类入境，依代 x 后之值域验 e。
对隐值参数验之：受「x」而 e 绑 x；以 会 起之拉姆达，先以不重之新名启隐值参数，乃验全拉姆达。二者皆裹为隐拉姆达，随隐参之擦而去。
遇 A 者「x」而 e 合成之时，体之类及 x 则合依值之箭，否则合常箭。
隐值参数惟用于类中。项层引之，由隐参之擦告“隐式参数擦除后绑定变量仍然存在”。待办事项：于类检之时先拦之。

依五：相等

整数索引：两侧至少一侧为整数加、减、乘或列投影（长度、乘积）之调，则两侧规为数学整数多项式而较之。变量与不透明之项为原子；长度、乘积 施于列变量段者亦为原子。较前先规标准库总集重导之别名。
列投影：长度 循字面段累计元数，乘积 循元之整数多项式相乘，空列之积为一。乘积 由标准库 数据结构/多态列。豫 供之。
结构之较，左侧已解之待求变量先代入。
待办事项：含变量之列、字符串、爻索引仍惟依结构较之；第N个 犹未接整数之规。

依六：模式

支之细化，外境中类为可依内建值之局部名，与类变量同可解：空列 之果 定长列于零 配 定长列于 n，则此支中 n＝0。
整数索引之合一先依结构；相冲则规两侧为多项式：相等则不细，两侧皆常而异则判不可达，余告“无法细化”。覆盖之验遇“无法细化”以可达处之，惟告缺例之警。
所期之类不能定之隐值参数，为支中存在之名，依其定义域声之。
依值模式匹配：所匹为变量而见于所期之类，则各支所期之类以其支之模式代之，索引随之而规，如 长度于（缀头尾） 规为一加 尾 之长。
已析为文件定义引用之裸构造器模式，同于依名所得之构造器：有隐参者行模式施函，否则行广义合一。
待办事项：境中余变量之类所见之所匹变量犹未代之；构造器之依值字段于模式中犹未以字段名代入后字段之类；规后一侧为独待求变量者犹未据之而绑。

依七：擦除与边界

隐值参数如隐类参擦之，显依值参数照常传之。签名之数与签名之类别去相间之隐前缀，依值之位依常显参计之。无体之声之数亦计依值之位。宿主之界：带索引之类依去索引后之形处之，构造器之隐值参数如类参由类实参代之；依值之箭与隐值参数之函，如常函、全称之函，不得过界。待办事项：果类带复索引（如 加 n 一）之构造器，仍以果类特化处之而见拒。

依八：验收之样

应用/豫言编译器/测试/语法/依值类型/ 收第八节例一（局部寄配之二表，及只开一格、次序颠倒二反例）、例二（向量拼接与点积，及维数不同反例）、例五（张量改形，及漏维反例），又有依值箭、签、旧式书法告错、索引细化、无法细化与依值模式匹配诸例。

检索所得