BT

Your opinion matters! Please fill in the InfoQ Survey!

Dependent-Types Language Idris Reaches 1.0

| by Sergio De Simone Follow 5 Followers on Apr 06, 2017. Estimated reading time: 1 minute |

A few months after reaching what could be considered alpha stage, Idris 1.0 is out, writes Idris creator Edwin Brady, Lecturer in Computer Science at the University of St Andrews, UK.

The key point in Idris, being now 1.0, is its core language along with the base libraries being considered stable, meaning that future 1.x versions of the language should guarantee backward source compatibility. Since the alpha release, Idris evolution has focused on tools and library support, while the language has gained new pragmas to enable less stable features, and a new LinearTypes language extension. Still, there is a lot of room for more contributions, says Brady, in particular to improve the compiler and runtime efficiency, as well as to fix the over 200 bugs that are currently open.

Although Brady believes that Idris is primarily a research tool and that it is currently under-stuffed to be considered production-ready, the interest in the language has been growing, as attested by the recent publication from Manning of Type-Driven Development with Idris authored by Brady himself, the rising number of contributors to the GitHub repo, and recent academical work. These could be the signs of an incipient Idris community, although it could still be too early to say. In conversation with InfoQ, Brady has remarked the following:

It's certainly nice to see a growing interest in Idris! There's still
lots of work to do, but it's good that we have a stable language to
build on now that we've reached 1.0. My immediate goals are to improve
efficiency and robustness of the core.

We still have quite a few open issues, but many of these are about
tooling and usability, and many others are feature requests. If anyone
wants to get involved, the ones tagged as "Low Hanging Fruit" are good
places to start, and the Idris community will try to help if anyone has
any questions.

Idris is a purely functional programming language that aims to make type-based program verification techniques available to a larger number of programmers, while retaining its focus on being general-purpose and efficient enough to be used for system programming as well. You can start learning about Idris by reading its tutorial. Also, make sure to read about the trade-offs of programming with dependent types.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT