写点什么

依赖类型语言 Idris 发布 1.0 版本

  • 2017-04-13
  • 本文字数:764 字

    阅读完需:约 3 分钟

英国圣安德鲁大学讲师、Idris 创建者Edwin Brady写道,在达到 alpha 阶段几个月之后,Idris 1.0 发布。

1.0 版本发布,最关键的一点是其核心语言及基础库都被认为是稳定的,就是说,将来的 1.x 版本应该确保源代码向后兼容。自 alpha 版本以来, Idris 就一直致力于工具和库的支持,同时,该语言添加了新的编译指令和一个新的LinearTypes语言扩展,其中前者是为了让使用稳定性较差的特性成为可能。然而,据 Brady 介绍,还是有许许多多可以做贡献的地方,尤其是改进编译器和运行时效率,以及修复 200 多个当前正处于打开状态的Bug。

虽然Brady 认为,Idris 从根本上讲是一个研究工具,目前还不足以考虑在生产环境中应用,但由Brady 写作并于近期出版的_ Manning of Type-Driven Development with Idris _,其 GitHub 库贡献者数量的增加,以及最近的学术著作,都说明人们对于这门语言的兴趣一直在增长。这些可以看作是 Idris 社区开始形成的标志,虽然这样说还有点太早。InfoQ 请求 Brady 对此发表评论,他的回复如下:

看到人们对 Idris 越来越感兴趣当然不错!虽然还有大量的工作要做,但我们已经达到了 1.0 版本,我们现在已经有了一门可以作为构建基础的稳定语言。我当前的目标是改进内核的效率和健壮性。

我们仍然还有不少处于打开状态的问题,但是,其中有许多是关于工具和可用性,另外还有许多特性请求。如果有人想参与,则可以从那些带有“Low Hanging Fruit”标签的开始。如果任何人有任何问题,Idris 社区都会尽量提供帮助。

Idris 是一门纯粹的函数式程序设计语言,旨在为更多的程序员提供基于类型的程序验证技术,同时,还能继续专注于成为一门通用语言,并且足够高效,可以用于系统编程。想要学习 Idris 的读者,可以阅读这个教程。此外,务必要阅读有关依赖类型编程的利弊

查看英文原文 Dependent-types Language Idris Reaches 1.0

2017-04-13 19:007310
用户头像

发布了 1008 篇内容, 共 439.9 次阅读, 收获喜欢 346 次。

关注

评论

发布
暂无评论
发现更多内容

放弃Cursor,我依然选择了Claude断供后的Windsurf

王翊仰

如何利用YashanDB实现数据分片与负载均衡

数据库砖家

如何利用YashanDB数据库加强数据分析能力

数据库砖家

Post-Training on PAI :Ray on PAI,云上一键提交强化学习

阿里云大数据AI技术

人工智能 数据库 模型训练 模型 模型推理

如何利用YashanDB进行高效数据归档管理

数据库砖家

如何利用YashanDB实现跨地域数据同步与灾备部署

数据库砖家

中烟创新自研【烟草行政许可文书制作系统】纳入“北京市人工智能赋能行业发展典型案例集”

中烟创新

如何利用YashanDB实现业务数据的高效管理?

数据库砖家

Golang基础笔记九之方法与接口

Hunter熊

golang 方法 接口 类型断言

一文读懂 Sigmoid 与 Hard Sigmoid 激活函数:从原理到量化部署

地平线开发者

自动驾驶 算法工具链 地平线征程6

01-自然壁纸实战教程-免费开放啦

万少

鸿蒙 HarmonyOS HarmonyOS NEXT

如何利用YashanDB构建智能决策支持系统?

数据库砖家

如何利用YashanDB实现实时数据处理

数据库砖家

如何利用YashanDB数据库实施数据治理

数据库砖家

从超级个体到超智能企业的一些思考

Abel(不忘初心) 钱小军

01-自然壁纸实战教程-免费开放啦

万少

HarmonyOS

如何利用YashanDB进行机器学习模型的构建

数据库砖家

如何利用YashanDB数据库进行数据监控

数据库砖家

聚焦全球数字经济大会 | 焱融存储推理加速方案成现场焦点

焱融科技

人工智能 数字经济 模型推理 KVCache

如何利用YashanDB进行高效的数据挖掘?

数据库砖家

如何利用YashanDB数据库实现分布式事务管理

数据库砖家

RAG评估矩阵全公开:如何科学衡量检索增强系统?

聚客AI学院

人工智能 向量数据库 RAG搭建 RAG应用 RAG 框架

跨平台动漫应用 Ani - 多平台支持的开源项目

qife122

kotlin 动漫

API 网关在iPaaS集成平台中的功能具体体现

谷云科技RestCloud

安全管理 API API网关 ipaas 网关管理

Coco AI 实战(一):Coco Server Linux 平台部署

极限实验室

CocoAI

剪映和Camtasia Studio哪个更好用 录制微课用什么剪辑简单方便 剪映和Camtasia Studio有什么区别

阿拉灯神丁

屏幕录制 录屏工具 视频编辑 Camtasia Studio2024 视频剪辑软件

哈尔滨等保测评:流程、要点

等保测评

Cookie Monster 的秘密配方:Pico CTF 登录机制中的隐藏旗帜

qife122

CTF Cookie分析

如何利用YashanDB构建企业级数据共享平台

数据库砖家

如何利用YashanDB数据库实现高可用性设计?

数据库砖家

Serverless JManus: 企业生产级通用智能体运行时

阿里巴巴云原生

阿里云 Serverless 云原生 函数计算

依赖类型语言Idris发布1.0版本_后端_Sergio De Simone_InfoQ精选文章