Idris 2 v0.4.0 发布,类 Haskell 的纯函数编程语言
Idris 2 v0.4.0 发布。此版本主要变化包括语法变更、编译器变更、REPL/IDE 模式变更、库的变更,以及 API 变更等。
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 的交互环境
语法变化
- 带
"""分隔符的多行字符串 (#1097) - 使用
with关键字后强制严格缩进 (#1107) - 参数块 (parameter block) 的语法已更新。它现在允许声明隐式参数并为参数提供多重性,旧语法仍可用于兼容性目的,但将来会被删除
- 添加对 SnocList 语法的支持:
[< 1, 2, 3]desugars intoLin :< 1 :< 2 :< 3,以及高亮显示
编译器变化
- 添加更多优化和转换,特别是在 case 块、列表型的类型和枚举上,因此生成的代码通常会稍微快一点
- 添加
--profile标志,如果后端支持,则会生成配置文件数据。目前由 Chez 和 Racket 后端支持 - 添加了一个环境变量
IDRIS2_PACKAGE_PATH用于扩展查找包的位置 - 实验性标志 (
-Xcheck-hashes) 用于检查散列而不是文件系统时间以确定是否应重新编译文件,这将助于 CI/CD 缓存