寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式合一」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式合一结构比较」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「抽象语法树」之「总集」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「命名环境术」之书。
寻观「编译器核心」之「编译数据」之「操作符」之「操作符数据结构」之书。
寻观「拓展库」之「顺序标识符」之「顺序标识符」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「类型检查基础」之书。

「函数应用接地信息」即「表达式」合（「或可有」于「表达式」）也。 「：含局部变量的类型、可直接读取的 ground 类型：」
「函数应用类型骨架」即「匹配合一上下文」合（「列」于「字符串」）合（「列」于「表达式」）合「表达式」也。 「：上下文、按声明顺序的隐式变量名、显式参数类型、返回类型：」
「函数应用参数组」即（「列」于「表达式」）合（「列」于「表达式」）合（「列」于（「参数形式」合「表达式」））也。 「：已给隐式参数、当前函数的全部显式参数、剩余调用脊：」

「收集函数调用头脊」乃化「表达式」而「表达式」合（「列」于（「参数形式」合「表达式」））也。
「收集函数调用头脊」者会「式」而
  鉴「式」而
    有（「式节点」于「函数调用」于（「缀」于「头」于「参数节点们」））则
      「头」与（（「态射」）于「参数节点们」于（会「参数节点式」而
        鉴「参数节点式」而
          有（「式节点」于（「参数节点」于「形」）于（（「列」【「参数」】）））则「形」与「参数」
          或有「其他」则「发生事故」于『函数调用脊必须是单参数节点』
        ））
    或有「其他」则「式」与「罄」
也。

「读取函数应用实参类型」乃化「命名环境」而化「表达式」而「或可有」于「表达式」也。
「读取函数应用实参类型」者会「境」而会「参数」而
  鉴「参数」而
    有（「式节点」于（「源码范围标注节点」于「忽略范围」）于（（「列」【「源码参数」】）））则
      「读取函数应用实参类型」于「境」于「源码参数」
    或有（「自由变量」于「名」）则（鉴（「解析单个名称及物」于「境」于「名」）而
      有（「可有」于（「参数类」与「忽略参数物」））则「可有」于「参数类」
      或有「可无」则「可无」 「：模式中的新绑定尚不在环境中：」
    ）
    或有（「式节点」于（「文件定义引用节点」于「文件名」于「定义名」于「忽略序数」）于「罄」）则（鉴（「文件定义引用类及物」于
          「境」于「文件名」于「定义名」
      ）而
      有（「参数类」与「忽略参数物」）则「可有」于「参数类」
    ）
    或有「其他参数」则「可无」
也。

「函数应用期望类自由名」乃化（「或可有」于「表达式」）而「列」于「字符串」也。
「函数应用期望类自由名」者会「可能期望类」而
  鉴「可能期望类」而
    有「可无」则「罄」
    或有（「可有」于「期望类」）则「读取式自由变量」于「期望类」
也。

「实例化函数应用隐式参数」乃化（「列」于「字符串」）而化「匹配合一上下文」而化「表达式」而「字符串」合「表达式」合
  「匹配合一上下文」也。
「实例化函数应用隐式参数」者会「已用名」而会「上下文」而会「绑定值域」而
  鉴「绑定值域」而
    有（「绑定」于「忽略原名」于「下式」）
    则（虑「全已用名」者（「附加」授以「字符串」）于「已用名」
      于（「读取式自由变量」于「下式」）而
        递归虑「新局部名」其化「有」而「字符串」者会「无」而
              虑「候选名」者「下个字符序数」于『__函数应用隐式参数__』而若（「存在吗」授以「字符串」）
                于（会「已有名」而「串相等」于「候选名」于「已有名」）于「全已用名」则
                  「新局部名」于「元」
              否则
                「候选名」
            而
            虑「名」者「新局部名」于「元」而
            虑「值域」者「解构替换绑定名非重复」于「一」于「名」于「下式」而
            虑「后上下文」者「匹配合一上下文添加变量」于「上下文」于「名」而「名」
          与「值域」与「后上下文」
    ）
    或有「其他值域」则「发生事故」于『隐式派值域必须是绑定』
也。

「读取函数应用类型骨架」乃化（「列」于「字符串」）而化「表达式」而「函数应用类型骨架」也。
「读取函数应用类型骨架」者会「初已用名」而会「头类」而
  虑「初上下文」者「空串典」授以（「或可有」于「表达式」）而
  虑「完成」者（化「匹配合一上下文」而化（「列」于「字符串」）而化「表达式」而「函数应用类型骨架」也
      会「上下文」而会「隐式名们」而会「显式函数类」而
        鉴（「拆分多参数函数类型」于「显式函数类」）而
          有（「可有」于（「参数类型们」与「返回类型」））则「上下文」与「隐式名们」与「参数类型们」与
    「返回类型」
          或有「可无」则「上下文」与「隐式名们」与「罄」与「显式函数类」
  ）而
  鉴「头类」而
    有（「式节点」于（「隐式派类型节点」于「参数个数」）于（（「列」【「绑定值域」】）））
    则（递归虑「读取隐式参数们」
      其
      化「整数」而化（「列」于「字符串」）而化「匹配合一上下文」而化（「列」于「字符串」）而化「表达式」而
        「函数应用类型骨架」者
          会「剩余个数」而会「已用名」而会「上下文」而会「反隐式名们」而会「当前绑定值域」而
            若（「等」于「剩余个数」于「零」）
            则
              「完成」于「上下文」于（「反转」于「反隐式名们」）于「当前绑定值域」
            否则
              （鉴（「实例化函数应用隐式参数」于「已用名」于「上下文」于「当前绑定值域」）而
                有（「隐式名」与「后绑定值域」与「后上下文」）则
                  「读取隐式参数们」于（「减」于「剩余个数」于「一」）
                    于（「缀」于「隐式名」于「已用名」）
                    于「后上下文」于（「缀」于「隐式名」于「反隐式名们」）于「后绑定值域」
              ）
            而
            「读取隐式参数们」于
                      「参数个数」于
                      「初已用名」于
                      「初上下文」于「罄」于
                      「绑定值域」
    ）
    或有（「式节点」于「箭头类型节点」于「忽略类型们」）则「完成」于「初上下文」于「罄」于「头类」
    或有「其他类」则「完成」于「初上下文」于「罄」于「其他类」
也。

「拆分函数应用参数组」乃化「整数」而化「整数」而化「爻」而化（「列」于（「参数形式」合「表达式」））而「函数应用参数组」
也。
「拆分函数应用参数组」者会「隐式参数个数」而会「显式参数个数」而会「要求饱和」而会「脊」而
  递归虑「读取显式参数们」其化「整数」而化（「列」于「表达式」）而化（「列」于「表达式」）而化（「列」
      于（「参数形式」合「表达式」））而「函数应用参数组」者
        会「剩余个数」而会「隐式参数们」而会「反显式参数们」而会「剩余脊」而
          若（「等」于「剩余个数」于「零」）
          则
            「隐式参数们」与（「反转」于「反显式参数们」）与「剩余脊」
          否则
            （鉴「剩余脊」而
              有（「缀」于（「显式」与「参数」）于「后脊」）则
                「读取显式参数们」于（「减」于「剩余个数」于「一」）于「隐式参数们」
                于（「缀」于「参数」于「反显式参数们」）于
                「后脊」
              或有「罄」则
                若「要求饱和」
                则
                  「发生事故」于『函数应用缺少显式参数，不允许部分应用』
                否则
                  「隐式参数们」与（「反转」于「反显式参数们」）与「罄」
              或有（「缀」于（「隐式」与「忽略参数」）于「忽略后脊」）则「发生事故」于
                『显式函数参数之间不可以出现隐式调用参数』
            ）
      而
      递归虑「读取隐式参数们」其化「整数」而化（「列」于「表达式」）而化（「列」于（「参数形式」合「表达式」））而
        「函数应用参数组」者
          会「剩余个数」而会「反隐式参数们」而会「剩余脊」而
            若（「等」于「剩余个数」于「零」）
            则
              「读取显式参数们」于「显式参数个数」于（「反转」于「反隐式参数们」）于「罄」于「剩余脊」
            否则
              （鉴「剩余脊」而
                有（「缀」于（「隐式」与「参数」）于「后脊」）则
                  「读取隐式参数们」于（「减」于「剩余个数」于「一」）
                  于（「缀」于「参数」于「反隐式参数们」）于
                  「后脊」
                或有「其他脊」则「读取显式参数们」于「显式参数个数」
                  于（「反转」于「反隐式参数们」）于「罄」于
                    「剩余脊」
              ）
          而
          「读取隐式参数们」于「隐式参数个数」于「罄」于「脊」
也。

「尝试接地函数应用类型」乃化「匹配合一上下文」而化「表达式」而化「表达式」而「匹配合一上下文」也。
「尝试接地函数应用类型」者会「上下文」而会「含变量类」而会「ground类」而
  鉴「ground类」而
    有（「式节点」于（「隐式派类型节点」于「忽略参数个数」）于（（「列」【「忽略值域」】）））则「上下文」 「：直接读取的多态类型仍需实例化，不能作为 ground 类型：」
    或有「其他ground类」则「尝试匹配合一」于「上下文」于「含变量类」于「ground类」
也。

「接地函数应用隐式参数」乃化「匹配合一上下文」而化（「列」于「函数应用接地信息」）而「匹配合一上下文」也。
「接地函数应用隐式参数」者会「初上下文」而会「接地信息们」而
  若（「等」于（（「长度」授以「字符串」）于（（「串典所有键」授以（「或可有」于「表达式」））于「初上下文」））于
    「零」
  ）
  则
    「初上下文」
  否则
    （虑「最终上下文」者（「从左折叠」授以「函数应用接地信息」授以「匹配合一上下文」）
      于（会「接地信息」而会
        「上下文」而
        鉴「接地信息」而
          有（「含变量类」与「可无」）则「上下文」
          或有（「含变量类」与（「可有」于「ground类」））则「尝试接地函数应用类型」于「上下文」于「含变量类」
            于「ground类」
      ）于「初上下文」于「接地信息们」而
      虑「未解名」者「匹配合一上下文未解名」于「最终上下文」而
      若（「等」于（「长度」于「未解名」）于「零」）
      则
        「最终上下文」
      否则
        「发生事故」于『函数应用的隐式参数无法完全确定：』附（「间合」于『，』于「未解名」）附
        『；匹配合一上下文：』附（「匹配合一上下文表示」于「最终上下文」））
也。

「写入函数应用已给隐式参数」乃化「匹配合一上下文」而化（「列」于「字符串」）而化（「列」于「表达式」）而
  「匹配合一上下文」合（「列」于「字符串」）也。
「写入函数应用已给隐式参数」者会「上下文」而会「剩余隐式名们」而会「剩余已给参数们」而
  鉴「剩余已给参数们」而
    有「罄」则「上下文」与「剩余隐式名们」
    或有（「缀」于「参数」于「后参数们」）则（鉴「剩余隐式名们」而
      有（「缀」于「隐式名」于「后隐式名们」）
      则（虑「后上下文」者（「串典更新」授以（「或可有」于「表达式」））于
        「上下文」于「隐式名」于（「可有」于「参数」）而
          「写入函数应用已给隐式参数」于「后上下文」于「后隐式名们」于
            「后参数们」
      ）
      或有「罄」则「发生事故」于『函数应用提供了过多隐式参数』
    ）
也。

「求解函数应用隐式参数」乃
    化「命名环境」而化「函数应用类型骨架」而化（「列」于「表达式」 「：用户已给隐式参数：」
    ）而
    化（「列」于「表达式」 「：当前函数的全部显式参数：」
    ）而化（「或可有」于「表达式」）而
      「列」于「表达式」 「：只返回自动插入的隐式类型实参：」
也。
「求解函数应用隐式参数」者会「境」而会「骨架」而会「已给隐式参数们」而会「显式参数们」而会「可能期望类」而
  鉴「骨架」而有（「初上下文」与「隐式名们」与「参数类型们」与「返回类型」）
  则（虑「上下文及缺省名们」者
        「写入函数应用已给隐式参数」于
        「初上下文」于「隐式名们」于
        「已给隐式参数们」而递归虑「读取显式接地信息们」其化（「列」于「表达式」）而化（「列」于「表达式」）而（「列」于
            「函数应用接地信息」
        ）者会
    「剩余参数类型们」而会
    「剩余显式参数们」而鉴
    「剩余参数类型们」与「剩余显式参数们」
    而
      有「罄」与「罄」则（「罄」授以「函数应用接地信息」）
      或有（「缀」于「参数类型」于「后参数类型们」）与（「缀」于「参数」于「后显式参数们」）则「缀」
        于（「参数类型」与（「读取函数应用实参类型」于「境」于「参数」））
        于（「读取显式接地信息们」于「后参数类型们」于「后显式参数们」）
      或有「其他」则「发生事故」于
        『函数应用骨架与显式实参数量不同：参数类型个数=』附（「整数表示」于（「长度」于「剩余参数类型们」））附
          『，实参个数=』附（「整数表示」于（「长度」于「剩余显式参数们」））
                                而
                                虑「显式接地信息们」者（鉴「显式参数们」而
                                  有「罄」则（「罄」授以「函数应用接地信息」） 「：裸多态函数由整个期望函数类型接地，没有显式实参信息：」
                                  或有「非空显式参数们」则「读取显式接地信息们」于
                                      「参数类型们」于「显式参数们」
                                ）而
                                虑「全部接地信息」者（「附加」授以「函数应用接地信息」）于
        「显式接地信息们」于（（「列」【（「返回类型」与「可能期望类」）】））而
                                虑「最终上下文」者「接地函数应用隐式参数」
          于（「上下文及缺省名们」中「零」）于「全部接地信息」
                                而
                                （「态射」授以「字符串」授以「表达式」）
          于（「上下文及缺省名们」中「一」）
        于（会「隐式名」而（「获取可有内容」授以「表达式」）
          于（（「串典读取」授以（「或可有」于「表达式」））于「最终上下文」于「隐式名」）））
也。

「添加当前函数应用组参数」乃化「爻」而化「表达式」而化「参数形式」而化「表达式」而「表达式」也。
「添加当前函数应用组参数」者会「已经开始」而会「函数」而会「形」而会「参数」而
  若「已经开始」
  则
    「添加函数调用参数」于「函数」于「形」于「参数」
  否则
    「函数调用式」于「函数」于（（「列」【（「参数节点式」于「形」于（（「列」【「参数」】）））】））也。

「检查函数应用参数组」乃化「命名环境」而化「表达式」而化「表达式」而化（「列」于「表达式」）而化（「列」于「表达式」）而
  化（「列」于「表达式」）而「表达式」合「表达式」也。
「检查函数应用参数组」者会「境」而会「头类」而会「头物」而会「已给隐式参数们」而会「显式参数们」而会「缺省隐式参数们」而
  虑「全部隐式参数们」者（「附加」授以「表达式」）于「已给隐式参数们」于「缺省隐式参数们」而
  递归虑「检查隐式参数们」其化「表达式」而化「表达式」而化（「列」于「表达式」）而化「爻」而「表达式」合「表达式」合
    「爻」者
      会「当前类」而会「当前物」而会「剩余参数们」而会「已经开始」而
        鉴「剩余参数们」而
          有「罄」则「当前类」与「当前物」与「已经开始」
          或有（「缀」于「参数」于「后参数们」）
          则（虑「后参数」者（「读引用」于「进行类型类型检查引用」）于「境」于
            「参数」而
              虑「后类」者「应用首隐式类型参数」于「当前类」于「后参数」而
              虑「后物」者「添加当前函数应用组参数」于「已经开始」于「当前物」于
                「隐式」于「后参数」而「检查隐式参数们」于「后类」于「后物」于
                「后参数们」于「阳」
          ）
      而
      鉴（「检查隐式参数们」于「头类」于「头物」于「全部隐式参数们」于「阴」）而
          有（「显式函数类」与「隐式后物」与「已经开始」）则（鉴「显式参数们」而
            有「罄」则「显式函数类」与「隐式后物」
            或有「非空显式参数们」则（鉴（「拆分多参数函数类型」于「显式函数类」）而
              有（「可有」于（「参数类型们」与「返回类型」））
              则（虑「无」者（若（「等」于（「长度」于「参数类型们」）于（「长度」于「显式参数们」））则
                    「元」
              否则
                「发生事故」于『函数应用显式参数数量与函数类型不一致』
                ）而
                  递归虑「检查显式参数们」其化「表达式」而化「爻」而化（「列」于「表达式」）而化（「列」于「表达式」）而
                    「表达式」者会「当前物」而
                      会「已有参数」而会「剩余参数们」而会「剩余类型们」而鉴
                      「剩余参数们」与「剩余类型们」而
                        有「罄」与「罄」则「当前物」
                        或有（「缀」于「参数」于「后参数们」）与（「缀」于「定义域」于「后类型们」）
                        则（虑「后参数」者（「读引用」于「进行对象类型检查引用」）于
                          「境」于「参数」于「定义域」而
                            虑「后物」者「添加当前函数应用组参数」于「已有参数」于
                            「当前物」于「显式」于「后参数」而「检查显式参数们」于
                            「后物」于「阳」于「后参数们」于「后类型们」
                        ）
                        或有「其他」则「发生事故」于
                          『函数应用显式参数与参数类型没有一一对应』而
                      虑「后物」者「检查显式参数们」于「隐式后物」于
                          「已经开始」于「显式参数们」于「参数类型们」而
                      「返回类型」与「后物」
              ）
              或有「可无」则「发生事故」于『函数调用的当前类型不是显式函数类型：』附（「表达式表示」于「显式函数类」）））
也。

「进行已知头函数应用」乃化「命名环境」而化「表达式」而化「表达式」而化（「列」于（「参数形式」合「表达式」））而化（「或可有」于
    「表达式」
）而「表达式」合「表达式」也。
「进行已知头函数应用」者会「境」而会「头类」而会「头物」而会「脊」而会「可能期望类」而
  虑「要求饱和」者（鉴「脊」而
  有「罄」则「阴」
  或有「非空脊」则「阳」）而
  虑「初已用名」者（「附加」授以「字符串」）于（「读取式自由变量」于「头物」）
    于（（「附加」授以「字符串」）于（「函数应用期望类自由名」于「可能期望类」）于（「命名环境获取所有名称」于「境」））
  而
  鉴（「读取函数应用类型骨架」于「初已用名」于「头类」）而有（「上下文」与「隐式名们」与「参数类型们」与「返回类型」）
  则
    若（「且」于「要求饱和」于（「且」于（「等」于（「长度」于「隐式名们」）于「零」）
          于（「等」于（「长度」于「参数类型们」）于「零」）））
    则
      「发生事故」于『函数调用的当前结果不是函数：』附（「表达式表示」于「头类」）
    否则
      （鉴（「拆分函数应用参数组」于（「长度」于「隐式名们」）于（「长度」于「参数类型们」）于「要求饱和」于「脊」）
        而
        有（「已给隐式参数们」与「显式参数们」与「剩余脊」）
        则（虑「当前可能期望类」者（鉴「剩余脊」而
          有「罄」则「可能期望类」
          或有「非空剩余脊」则「可无」授以「表达式」）而
            虑「接地返回类型」者（鉴「显式参数们」而
              有「罄」则（鉴「参数类型们」而
                有「罄」则「返回类型」
                或有「非空参数类型们」则「多参数函数类型」于「参数类型们」于
                  「返回类型」
              ）
              或有「非空显式参数们」则「返回类型」
            ）而
            虑「接地骨架」者「上下文」与「隐式名们」与「参数类型们」与
          「接地返回类型」而
            虑「缺省隐式参数们」者「求解函数应用隐式参数」于「境」于
            「接地骨架」于「已给隐式参数们」于「显式参数们」于
            「当前可能期望类」而
            虑「当前结果」者「检查函数应用参数组」于「境」于「头类」于
            「头物」于「已给隐式参数们」于「显式参数们」于
            「缺省隐式参数们」而鉴「剩余脊」而
              有「罄」则「当前结果」
              或有「非空剩余脊」则「进行已知头函数应用」于「境」
                于（「当前结果」中「零」）
                于（「当前结果」中「一」）于「剩余脊」于「可能期望类」
        ））
也。

「进行函数应用头脊类型合成」乃化「命名环境」而化「表达式」而「表达式」合「表达式」也。
「进行函数应用头脊类型合成」者会「境」而会「物」而
  虑「头及脊」者「收集函数调用头脊」于「物」而
  虑「头类及物」者（「读引用」于「进行对象类型合成引用」）于「境」
    于（「头及脊」中「零」）而
  「进行已知头函数应用」于「境」于（「头类及物」中「零」）于（「头类及物」中「一」）
    于（「头及脊」中「一」）于（「可无」授以「表达式」）
也。

「进行函数应用头脊类型检查」乃化「命名环境」而化「表达式」而化「表达式」而「表达式」也。
「进行函数应用头脊类型检查」者会「境」而会「物」而会「期望类」而
  虑「头及脊」者「收集函数调用头脊」于「物」而
  虑「头类及物」者（「读引用」于「进行对象类型合成引用」）于「境」
    于（「头及脊」中「零」）而
  虑「结果类及物」者「进行已知头函数应用」于「境」于（「头类及物」中「零」）
    于（「头类及物」中「一」）于（「头及脊」中「一」）于（「可有」于「期望类」）而
  虑「无」者「断言类型相等」于（「结果类及物」中「零」）于「期望类」而
  「结果类及物」中「一」
也。
