Idris

定义

Idris 是一门以依赖类型（dependent types）为核心的静态类型纯函数式编程语言，由 Edwin Brady 主导开发。与偏重定理证明的 Agda、Coq 不同，Idris 的定位是「面向通用编程的依赖类型语言」。

核心特性

在 Idris 中，类型是一等公民，类型可以依赖于值，例如可在类型层面表达「长度为 n 的向量」，让编译器静态排除越界等错误。语言支持代数数据类型、类型类式的接口机制、全函数性检查（totality checking）。Idris 2 基于定量类型理论（Quantitative Type Theory），可在类型中标注变量的使用次数，从而表达线性资源。

应用

Idris 主要用于教学、研究和探索类型驱动开发方法，Brady 所著《Type-Driven Development with Idris》系统阐述了这一实践。

意义

Idris 推动了依赖类型从证明助手走向日常编程的探索。