依赖类型签名与独立证明两种实现方式的差异问题

两种实现方式并非只有使用体验上的差异，存在几方面核心本质区别：

• 约束的强制力和绑定关系完全不同
  把属性直接写进依赖类型签名的方案里，性质是函数、数据类型本身不可分割的一部分。以长度索引列表的(++)为例，你在编写函数实现时，类型检查器会直接校验输出值必须符合Vect (m + n) a的约束，只要实现能通过类型检查，就天然满足“拼接后长度为两列表长度之和”的性质，不存在“函数实现正确但不符合性质”“性质证明和函数实现不匹配”的可能。如果后续修改函数实现，只要改动破坏了长度性质，类型检查会直接报错，不会出现“实现改了但证明没同步更新”的不一致问题。所有调用该函数的下游代码，不需要额外引入任何证明，拿到返回值就可以直接使用长度相关的性质。
  而普通List加单独证明的方案中，函数实现和性质证明是完全分离的两个实体：你编写(++)实现时，类型系统不会对长度行为做任何校验，哪怕你写出“无论输入什么都返回空列表”的错误实现，在类型层面也是合法的，只是后续你没法写出对应的appendAddsLength证明而已。同时下游代码调用List版的(++)时，默认拿不到任何长度相关的保证，如果需要用到长度性质，必须手动把对应的证明引入到调用位置，编译器不会自动帮你关联这个性质。如果后续修改了(++)的实现但忘了更新对应证明，就会出现证明和实际行为不一致的问题，而这类问题不会在函数本身的类型检查阶段被捕获。

• 不变量的维护成本和覆盖范围完全不同
  内嵌依赖类型的方案中，长度不变量是刻在数据结构定义里的：只要你操作的是Vect，不管是写拼接、拆分、映射、压缩哪种操作，类型系统都会自动要求你维护长度索引的正确性，不需要你为每个操作单独编写长度相关的证明，多个函数组合时，长度性质会自动沿着调用链传递，不需要额外做证明的拼装。
  而外部证明的方案中，不变量没有和数据结构绑定，你每写一个操作List的函数，都需要单独为它编写对应的长度性质证明；当你把多个函数组合成新的逻辑时，还需要手动把各个函数的证明拼装、变换，才能得到新逻辑对应的性质，随着代码规模变大，证明的维护成本会非线性上涨。

• 错误的暴露时机完全不同
  内嵌依赖类型的方案里，只要你违反了约定的性质，不管是函数实现写错了，还是调用函数时搞错了长度约束，错误会在你编写代码的阶段直接被类型检查器捕获，根本不会进入后续的测试、运行环节。
  而外部证明的方案中，如果你写完函数实现后忘了写证明、或者证明写得有疏漏，函数本身依然可以正常编译、被调用，性质的缺失不会直接阻断函数的使用，只有当你后续需要用到相关性质、或者做形式化验证的时候才会发现问题。

从纯理论的表达能力来看，在支持全谱依赖类型的语言中这两种方案是等价的：你完全可以通过外部证明模拟出内嵌类型的所有效果，反过来也可以把带外部证明的List封装成带长度索引的Vect类型。但两者在工程层面的强制力、维护成本、错误捕获机制上的差异是本质性的，和使用是否方便的工效学问题无关。

内容的提问来源于stack exchange，提问作者joel