Idris 的早期实现：让依赖类型进入日常编程

在苏格兰圣安德鲁斯大学工作的埃德温·布雷迪，开发 Idris 时面对的是一个具体问题：如果类型可以包含数值，程序员便能写出更精确的约束，但这种能力如何用于需要读文件、接收输入和调用外部程序的工作？早期包说明把 Idris 称为具有完整依赖类型的实验语言，并明确提到它与 Epigram、Agda 的联系。

它希望保留 Haskell、OCaml 使用者熟悉的函数式编程风格。函数、递归和模式匹配仍然是组织程序的手段；新增的表达能力则让类型不只描述“这是一个列表”，还可以描述“这是一个长度为某个数的序列”。开发者希望类型检查器承担更多检查工作，而实际程序仍能使用基本数据、文件操作及并发等设施。

参考：[1] [2]

Hackage 的历史记录显示，布雷迪在2009年12月上传了 Idris 0.1.3。该页面提供源代码压缩包，包内的 idris.cabal 标明版本0.1.3、作者和 Alpha 稳定性。这个记录为早期实现提供了一个可以明确定位的公开分发阶段；它不等于语言全部研究工作的起点。

发行包同时包含编译器的 Haskell 模块、命令行程序入口和 Idris 编写的库文件。依赖项包括 Ivor 与 Epic。读者获得的因此不只是语言设想或语法介绍，而是带有实现、库和构建说明的软件包。它使用当时的工具与依赖版本，理解这份材料也须保留这个技术环境，不能拿后来版本的安装方式替代。

参考：[1]

包中的 vect.idr 给出了一个直接例子。Vect 的类型参数除元素类型以外，还带有自然数长度；空向量的长度为零，在已有向量前加一个元素，就把长度从 k 变为 S k。这里的 S 表示自然数的后继，配套的 nat.idr 定义了自然数和加法。

拼接函数 vapp 接收长度分别为 n、m 的两个向量，返回类型写成长度为 plus n m 的向量。程序分为空向量和非空向量两种情况，沿第一个向量递归构造结果。这样，拼接后长度如何变化已经进入函数接口，而不只是留在注释里。

同一文件里的 vlookup 把索引写成 Fin k，把待查向量写成 Vect A k。索引与容器共享长度参数，为表达合法位置提供了类型层面的联系。这些实例说明了依赖类型如何把数据之间的关系交给检查器；它们不保证整个程序不会发生任何错误。

参考：[1]

io.idr 则把研究带到与外部世界交互的部分。它列出输出字符串、读取字符串、创建锁和外部函数调用等命令，并用 Response 按命令确定返回类型：输出字符串返回单位值，读取字符串返回字符串。相应的 putStr、getStr 和文件操作封装，使这些动作能被程序组合起来。

这一设计把需要表达的约束延伸到操作接口，但外部函数仍然有自己的约定与风险。源码在允许 C 函数构造 Idris 数据的地方专门提示需要谨慎。类型接口和真实运行环境必须一起理解，不能把接口上的精确描述当作对外部代码的全面证明。

布雷迪在2010年5月的社群报告中说明，Idris 通过 C 代码编译，并使用 Boehm–Demers–Weiser 垃圾收集器；它也带有交互式证明能力。这个同时期说明把发行包与其运行路线联系起来，而没有借用后来实现的垃圾收集方式。

参考：[1] [2]

2010年的报告仍把项目列为活跃的实验语言，强调编程而不仅是证明，并提到用于验证网络协议的库正在开发。网络、文件和并发既是项目的应用方向，也需要具体库与运行时逐步落实，不能仅凭目标清单就断言所有设施已经成熟。

把2009年的发行包与2010年的开发者报告放在一起，可以看见 Idris 早期工作的实际轮廓：长度相关的数据类型说明它如何表达约束，输入输出库说明它如何接触外部世界，编译路线则说明这些程序如何走向执行。后续 Idris 的重构和版本演变属于下一阶段，应与这份早期实现分别叙述。

参考：[1] [2]