Dependent Haskell与Idris的区别及依赖类型领域技术差异咨询

• 现有生态无需迁移即可复用依赖类型能力：无需将现有项目整体切换到新语言，Haskell生态沉淀十余年的Web框架、并发原语、科学计算库、生产级部署工具链都可以直接和依赖类型特性结合，比如可以直接为pandoc、lens这类生态核心组件添加更细粒度的类型校验，不需要重写任何已有逻辑。
• 降低现有Haskell开发者的学习成本：不需要重新学习新的语法体系、标准库和工具链，在已经熟悉的Haskell语法、cabal/stack工作流基础上就可以逐步引入依赖类型实践，学习路径完全衔接。
• 统一零散的类型级编程特性：将目前散落在TypeFamilies、GADTs、DataKinds、singletons等GHC扩展中的类型级编程能力整合为统一的依赖类型体系，消除不同扩展组合带来的语法奇异性和使用门槛。
• 为工业场景提供更低成本的正确性保障：在金融、高可用分布式系统等Haskell已经有成熟落地的领域，可以直接用依赖类型做协议正确性校验、边界条件静态检查，不需要引入额外的形式化验证工具链。

• 经过验证的工业级生态沉淀：Haskell有十多年的生产环境落地经验，从数据库驱动到性能分析工具都已经经过大规模场景验证，依赖类型特性可以直接落地到生产项目中，而Idris目前主要应用于研究和实验场景。
• 原生兼容惰性求值语义：Dependent Haskell的所有依赖类型特性都是基于Haskell原生的惰性求值语义设计的，不需要修改现有代码的求值逻辑即可使用，对已经基于惰性求值做架构设计的项目完全兼容。
• 丰富的类型级编程实践沉淀：Haskell社区已经有近十年的类型级编程实践积累，大量设计模式、最佳实践都可以直接平移到Dependent Haskell的开发中，不需要从零摸索适配方案。
• 成熟的性能优化体系：GHC的优化流水线已经发展了二十多年，Dependent Haskell的实现会和现有优化逻辑完全兼容，依赖类型代码可以获得和普通Haskell代码同等级的运行性能，而Idris的性能优化还处于早期发展阶段。

Dependent Haskell的核心基础是带依赖类型扩展的System Fω，而Idris的核心基础是定量类型理论（Quantitative Type Theory, QTT），二者的核心差异主要体现在三个层面：

• 擦除逻辑差异：System Fω的类型擦除基于种类层级区分，默认所有类型级内容在运行时都会被完全擦除，Dependent Haskell的设计中依赖类型的项默认也会在运行时擦除，需要显式标注才会保留到运行时；而QTT通过资源用量标记（0、1、ω）定义项的擦除属性，0用量的项会被擦除，1用量对应线性类型，ω对应无限制的普通项，擦除逻辑更统一但对开发者的标注要求更高。
• 求值策略差异：System Fω原生适配非严格（惰性）求值，Dependent Haskell的设计保留了Haskell的惰性求值语义，类型检查和项的求值完全分离，不会因为类型检查引入额外的运行时开销；而Idris默认是严格求值，依赖类型检查和项的求值逻辑耦合更紧密，要实现惰性求值需要显式标注。
• 兼容性设计差异：Dependent Haskell的核心设计原则是完全向后兼容现有Haskell代码，所以在依赖类型实现上做了针对性妥协，比如保留了Haskell的非完全性支持（允许无限递归、非终止项出现在类型检查阶段并做特殊处理），不会强制要求所有项都是总函数；而Idris从设计之初就是原生支持依赖类型的语言，默认要求类型检查阶段的项都是总函数以保证类型检查的终止性，使用非总函数需要显式标注。

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