New functional language champions type-driven development

Functional programming has added a new language in its ranks with the recent 1.0 release of Idris.

The language is positioned as general purpose, with dependent types. «Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behavior can be specified precisely in the type,» documentation on the language said. Idris also leverages eager evaluation for compilation, in which an expression is evaluated right when it is bound to a variable.

Idris also features totality checking, coinductive types, an extensible syntax, a simple foreign function interface to C, and a Hugs-style interactive environment. Hugs 98 was a programming language based on Haskell 98; Idris is closely related to the Agda and Epigram functional languages.

Development of Idris has been led by Edwin Brady, a lecturer in computer science at the University of St. Andrews in the United Kingdom, who has even authored a book on the language, «Type Driven Development with Idris.» Despite its 1.0 designation, Idris at this stage remains primarily a research tool, arising out of research on dependent types. The compiler and runtime need to be improved, and bugs need to be fixed. Some important libraries may not be available, either.

Functional programming has been picking up steam in recent years. It has been praised for offering better-structured code and panned for making software less-efficient. Idris joins a growing list of functional or «functional first» languages, including Microsoft’s F#, Scala, and Clojure. Lambdascript was recently introduced to bridge functional programming to Python.