主要观点：作者偶尔在 Fediverse 上开玩笑提及维基百科关于支持依赖类型的编程语言列表，Ada 作为一种 1983 年的语言出现在其中，之后常有人询问 Ada 的依赖类型，作者决定写文解释。Ada 的依赖类型是类型依赖于具体值，其设计哲学避免动态分配，通过第二非调用栈解决函数返回值问题，关键动机是避免动态分配。Ada 的类型系统在 1983 年就很超前，注重建模类型意图，数组可使用任意整数类型作索引，还引入了判别式、类型谓词等概念实现更灵活的依赖类型。同时探讨了“学术语言”和“商业语言”（如 SPARK 和 Ada）之间的奇怪相互作用，Ada 的很多类型系统概念虽与类型理论相关，但可能并非直接从理论而来。

关键信息：

• 维基百科列表中 Ada 与复杂功能语言等并列。
• Ada 避免动态分配及第二栈解决方案。
• Ada 类型系统特点及相关示例，如不同类型定义、数组类型等。
• 判别式及类型谓词在依赖类型中的应用。
• “学术语言”与“商业语言”的相互作用及 Ada 的特殊性。

重要细节：

• 举例说明 Ada 中依赖类型的应用，如根据函数参数创建数组。
• 提到 Ada 2012 引入更强大的依赖类型及设计合同系统。
• 解释不同类型谓词的作用及适用场景。
• 说明 Ada 类型系统中表示子句等相关细节。