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。