BT

New Early adopter or innovator? InfoQ has been working on some new features for you. Learn more

Idris Getting Close to Version 1.0

| by Sergio De Simone Follow 4 Followers on Dec 19, 2016. Estimated reading time: 2 minutes |

Dependent types-based language Idris will soon reach version 0.99, which can be viewed as an alpha release of 1.0, according to the Idris team. Idris 1.0 is expected sometime around February 2017.

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.

The main idea behind Idris is that of dependent types, which aim to express dependencies between types and values, just like functions are a way to express dependencies between values. For example, we could define a sort function as returning a list where each element is smaller than the next, so that any implementation of that function will only compile if that property is proved true. Other examples of properties of software that could be expressed through Idris are array bounds verification and protocol correctness in distributed or concurrent systems, such as ensuring that all programs follow a specific protocol when accessing a file handle. This is how you can define a Vect type in Idris and a app function to append two such vectors:


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;

In the above code, the compiler is able to detect any misuse of the involved types, such as in the following broken implementation of 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

The main factor behind the decision to release 1.0 is the language getting stabler, say Idris core developers. This will not mean, though, that the language can be considered be “production ready”, mostly due to the impossibility for the development team to support it in the long term or guarantee the quality of its implementation. Still, Idris retains a lot of its value as a research tool to explore programming using dependent types.

Similarly to Coq, Idris supports interactive theorem-proving, including back reasoning, but aims to be a general-purpose programming language before a theorem prover. Idris compiles to C and relies and uses garbage collection for memory management.

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