大咖直播-鸿蒙原生开发与智能提效实战!>>> 了解详情
写点什么

依赖类型语言 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:007330
用户头像

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

关注

评论

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

记录第二天-Vue起步

默默的成长

前端 Vue 3 10月月更

三方库移植之NAPI开发[1]—Hello OpenHarmony NAPI

离北况归

OpenHarmony

笔记本电脑内卷之争:华硕4+4无忧保脱颖而出

极客天地

十问分布式数据库:技术趋势、选型及标准思考

OceanBase 数据库

还在为如何编写Web自动化测试用例而烦恼嘛?资深测试工程师手把手教你Selenium 测试用例编写

霍格沃兹测试开发学社

技术分享 | 接口测试价值与体系

霍格沃兹测试开发学社

VUE 初学者基础知识

默默的成长

Vue 前端 10月月更

技术分享 | 常见接口协议解析

霍格沃兹测试开发学社

技术分享 | 抓包分析 TCP 协议

霍格沃兹测试开发学社

一个值得深思的话题:Wi-Fi 7的诞生会不会取代 5G 网络?

wljslmz

5G 无线技术 10月月更 WiFi7

Java基础(三)| switch、循环及Random详解

timerring

Java random Switch 循环 10月月更

技术分享 | app自动化测试(Android)--显式等待机制

霍格沃兹测试开发学社

技术分享 | app自动化测试(Android)-- 属性获取与断言

霍格沃兹测试开发学社

Vue基础-插值表达式-数据驱动视图-指令系统

默默的成长

前端 Vue 3 10月月更

技术分享 | 使用postman发送请求

霍格沃兹测试开发学社

EasyCV DataHub 提供多领域视觉数据集下载,助力模型生产

阿里云大数据AI技术

深度学习 开源 模型 计算机上视觉

2022Q3消费级AR眼镜市场季度分析:国产品牌纷纷发力,市场全面启航

易观分析

科技 AR眼镜 季度报告

如何在 SAP BTP Java 应用里使用 SQLite 数据库

汪子熙

云原生 云平台 SAP 10月月更 btp

技术分享 | app自动化测试(Android)-- 参数化用例

霍格沃兹测试开发学社

启科量子开源量子编程框架 QuTrunk

启科量子开发者官方号

人工智能 开发工具 量子计算 量子技术 启科量子

Wave-2 802.11ac SoC for Routers, Gateways and Access Points//IPQ4019,IPQ4029,Wallys

wallys-wifi6

IPQ4019 ipq4029

StampedLock:一个并发编程中非常重要的票据锁

华为云开发者联盟

高并发 开发 华为云 企业号十月PK榜

6步搭建一个飞机大战游戏

华为云开发者联盟

云计算 软件开发 华为云 企业号十月PK榜

技术分享 | app自动化测试(Android)-- 特殊控件 Toast 识别

霍格沃兹测试开发学社

干货 | 接口自动化测试分层设计与实践总结

霍格沃兹测试开发学社

搜索中常见数据结构与算法探究(二)

京东科技开发者

数据结构 算法 时间复杂度 KMP 算法与数据结构

使用 Zpan 搭建低成本个人私有网盘,还不限速

华为云开发者联盟

云计算 华为云 网盘 企业号十月 PK 榜

十大 CI/CD 安全风险(三)

SEAL安全

DevOps CI/CD DevSecOps 软件供应链安全

技术分享 | app自动化测试(Android)-- Capability 使用进阶

霍格沃兹测试开发学社

测试人生 | 疫情之下工资翻了2倍多,这4个月学习比工作8年学到的还多

霍格沃兹测试开发学社

干货 | 测试专家(前阿里P8)聊测试职业发展常见瓶颈

霍格沃兹测试开发学社

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