Idris 2 发布了 0.6.0 版本。更新内容包括 REPL 变更、语法变更、编译器变更、IDE 协议变更和标准库变更等。

Idris 是一个类似 Haskell 的纯函数编程语言，类型系统支持 dependent types。

• 依赖模式匹配的依赖类型系统
• 简单的 C 函数接口
• 编译器级别的编码支持
• where 语句，with 规则，简单的 case 表达式，模式匹配 let 和 lambda 绑定
• Dependent records with projection and update
• Type classes
• 类型驱动的重载方案
• do notation and idiom brackets
• 缩进语法
• 可扩充的语法
• Cumulative universes
• 整体验证
• 类似 Hugs 的交互环境

主要变化

• 引入新的基于 Scheme 的实验性 evaluator（只有在通过 Chez scheme 或 Racket 编译时才可以使用）。如需在 REPL 中访问此功能，使用:set eval scheme将 evaluator 模式设置为基于 Scheme 的 evaluator。
• 引入新选项evaltiming，用于计算 REPL 中的评估所需时间，通过:set evaltiming进行设置
• 将:lp/loadpackage重命名为:package
• 新增:import，其功能与:module相同
• 新增通过:help <replCmd>获取详细帮助的功能，例如:help :help或:help :let。这也适用于:?和:h别名

详情查看 Changelog。