为何Haskell 9.0线性类型未设置Zero而Idris 2包含该多重性取值？

Haskell 9.0 线性类型设计未加入Zero多重性的核心原因如下： #

• 最小可行产品的迭代策略
  GHC团队上线线性类型特性时遵循MVP原则，优先保障核心线性逻辑的稳定性：仅保留覆盖绝大多数主流使用场景的One（恰好使用一次）和Many（无使用限制）两种多重性，Zero多重性对应的无关性量化属于边缘特性，优先级较低，为了避免拖慢核心特性的上线节奏，暂不纳入第一版实现。
• 现有特性已覆盖等价需求
  Haskell此前已经存在大量和Zero多重性功能重叠的成熟特性：比如多态类型参数本身就不会在运行时留存、虚模式匹配、Proxy类型等都能实现「变量不在运行时使用」的需求，当时没有迫切的必要性再在多重性体系里重复实现相同能力，也避免和现有语义产生冲突。
• 降低实现与验证成本
  加入Zero多重性需要大幅修改GHC类型检查器的约束求解逻辑，还要处理和GADT、levity多态等现有扩展的复杂交互场景，验证所有边界case的正确性需要极高的研发成本，在第一版线性类型落地时团队没有足够精力完成相关工作，因此选择暂不支持。
• 使用场景相对小众
  Zero多重性的核心价值主要体现在依赖类型相关的编码场景中，而Haskell的依赖类型支持本身还处于迭代阶段，绝大多数线性类型的核心使用场景（资源安全管控、线性数据结构、无拷贝IO操作等）仅靠One和Many就可以完全覆盖，没有加入Zero的迫切需求。

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