写点什么

Idris 趋近发布 1.0 版

  • 2016 年 12 月 29 日
  • 本文字数:901 字

    阅读完需:约 3 分钟

据 Idris 开发团队披露,基于依赖类型的Idris 语言即将完成0.99 版本,该版本可被看成是1.0 版的Alpha 版本。Idris 1.0 版有望于2017 年2 月左右发布。

Idris 是一种纯函数式编程语言,目标在于注重语言通用性及满足系统编程所需效率的同时,让更多的编程人员使用基于类型的程序验证技术。

Idris 的主要理念是依赖类型。正如函数表述了值之间依赖性,依赖类型旨在表示类型与值之间的依赖性。举个例子,我们可以定义一类返回值为一个列表的函数,要求列表中的元素值依次递减,只有满足了该属性,才会去编译该函数所采用的任何具体实现。对于可被 Idris 所表示的软件属性,其它的例子还包括数组范围验证以及分布式或并发系统中的协议正确性,譬如确保所有程序遵循特定的协议访问文件句柄。下面所示的代码段使用 Idris 定义了 Vect 向量的依赖类型,并向 vapp 函数中添加了两个向量:

复制代码
infixr 5 ::;
data Vect : Set -> Nat -> Set where
VNil : Vect a O
| (::) : a -> Vect a k -> Vect a (S k);
vapp : (Vect A n) -> (Vect A m) -> (Vect A (plus n m));
vapp VNil ys = ys;
vapp (x :: xs) ys = x :: vapp xs ys;

编译器可以检测到上面代码段中所涉及类型的误用。例如,下面的 vapp的实现就破坏了依赖性

复制代码
vapp : Vect a n -> Vect a m -> Vect a (plus n m);
vapp VNil ys = ys;
vapp (x :: xs) ys = x :: vapp xs xs; -- BROKEN

据 Idris 核心开发人员介绍,决定发布 1.0 版的主要原因是该语言正步入稳定。这并不意味着 Idris 已“可用于生产环境”,因为开发团队还不可能做到提供长期支持或是保证实现的质量。即使如此,作为一种探究如何使用依赖类型编程的研究工具而言,Idris 还是颇具价值的。

Coq 类似,Idris 也支持交互定理证明,其中包括了反向推理,但是在用于定理证明之前,Idris 意在首先成为一种通用的编程语言。Idris 程序将被编译为C 语言,其内存管理依赖于并使用了垃圾回收机制。

查看英文原文: Idris Getting Close to Version 1.0


感谢冬雨对本文的审校。

给InfoQ 中文站投稿或者参与内容翻译工作,请邮件至 editors@cn.infoq.com 。也欢迎大家通过新浪微博( @InfoQ @丁晓昀),微信(微信号: InfoQChina )关注我们。

2016 年 12 月 29 日 18:005620
用户头像

发布了 227 篇内容, 共 63.7 次阅读, 收获喜欢 26 次。

关注

评论

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

时间戳,这样用就对了

Simon

MySQL timestamp

获奖公布丨程序员的七夕骚话该怎么讲?留下你爱的表白~

InfoQ写作平台官方

写作平台 话题讨论 七夕 活动专区

Git 常用命令总结

迷羊

git

机器学习 | 卷积神经网络详解(二)——自己手写一个卷积神经网络

迈微AI研发社

Python 神经网络 学习 卷积神经网络 CNN

一.操作系统概述

Winter

操作系统

机器学习算法之——逻辑回归(Logistic Regression)原理详解及Python实现

迈微AI研发社

学习 算法 逻辑回归 正则化 梯度下降

浅谈备受开发者好评的.NET core敏捷开发工具,讲讲LEARUN工作流引擎

Philips

我一个普通程序员,光靠GitHub打赏就年入70万,要不你也试试

程序员生活志

必看的数据库使用规范

Simon

MySQL 技术规范

带你认识MySQL sys schema

Simon

MySQL

【杭州】阿里巴巴搜索推荐事业部开发岗位招聘

iSausage

Java 阿里巴巴 推荐 搜索

机器学习算法之——隐马尔可夫模型原理详解及Python实现

迈微AI研发社

Python 学习 算法 隐马尔可夫模型 HMM

给路灯按上“电话卡”,从此不仅只照明还给管理员“打电话”

华为云开发者社区

人工智能 物联网 物联网化 华为云 路灯

区块链最激动人心的未来是什么

CECBC

大数据 区块链技术

MySQL5.7应当注意的参数

Simon

MySQL 参数

大数据平台架构设计探究

vivo互联网技术

大数据 架构设计 数据平台

200 行代码就能骗人的首个聊天机器人

程序员生活志

编程 机器人

牧羊少年奇幻之旅

W

读书笔记 感悟

2020中国RPA指数测评报告|T研究

人称T客

区块链加未来3至5年可以预见 上链将成为常态

CECBC

区块链 金融 数字时代

vivo web service:亿万级规模web服务引擎架构

vivo互联网技术

架构 Web 浏览器

前端科普系列(1):前端简史

vivo互联网技术

大前端 Web

从零开始的深度学习实用教程 | PyTorch官方推荐

迈微AI研发社

人工智能 学习 算法 教程 PyTorch

三分钟看懂Python和Java的区别

程序员生活志

Java Python

拼多多员工小便池拉屎,网易智能马桶屏蔽信号,360、搜狐厕所被监控,互联网公司厕所那些事!

程序员生活志

互联网 职场

InnoDB 事务加锁分析

vivo互联网技术

MySQL 数据库 innodb

机器学习算法之——卷积神经网络(CNN)原理讲解

迈微AI研发社

神经网络 学习 算法 CNN

Linux-技术专题-buffer/cache理解

浩宇天尚

赋能云端管理 激发智能边缘 英特尔发布超能云终端解决方案

最新动态

Java基础知识篇(2020最新版)准备放进收藏夹吃灰的勿进

简爱W

Java

如何优雅的备份账号相关信息

Simon

MySQL

Idris趋近发布1.0版-InfoQ