Idris (programming language)
This article relies too much on references to primary sources. (August 2019) (Learn how and when to remove this template message)
|Designed by||Edwin Brady|
1.3.3 / May 24, 2020
|Filename extensions||.idr, .lidr|
|Agda, Clean, Coq, Epigram, F#, Haskell, ML, Rust|
Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell.
Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants.
The syntax of Idris shows many similarities with that of Haskell. A hello world program in Idris might look like this:
module Main main : IO () main = putStrLn "Hello, World!"
The only differences between this program and its Haskell equivalent are the single (instead of double) colon in the type signature of the main function, and the omission of the word "where" in the module declaration.
Inductive and parametric data types
data Tree a = Node (Tree a) (Tree a) | Leaf a
or in the more general GADT-like syntax:
data Tree : Type -> Type where Node : Tree a -> Tree a -> Tree a Leaf : a -> Tree a
With dependent types, it is possible for values to appear in the types; in effect, any value-level computation can be performed during typechecking. The following defines a type of lists whose lengths are known before the program runs, traditionally called vectors:
data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a
This type can be used as follows:
total append : Vect n a -> Vect m a -> Vect (n + m) a append Nil ys = ys append (x :: xs) ys = x :: append xs ys
The functions append a vector of m elements of type a to a vector of n elements of type a. Since the precise types of the input vectors depend on a value, it is possible to be certain at compile-time that the resulting vector will have exactly (n + m) elements of type a. The word "total" invokes the totality checker which will report an error if the function doesn't cover all possible cases or cannot be (automatically) proven not to enter an infinite loop.
Another common example is pairwise addition of two vectors that are parameterized over their length:
total pairAdd : Num a => Vect n a -> Vect n a -> Vect n a pairAdd Nil Nil = Nil pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
Num a signifies that the type a belongs to the type class Num. Note that this function still typechecks successfully as total, even though there is no case matching Nil in one vector and a number in the other. Since both vectors are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.
Proof assistant features
Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile-time. This makes Idris into a proof assistant.
There are two standard ways of interacting with proof assistants: by writing a series of tactic invocations (Coq style), or by interactively elaborating a proof term (Epigram/Agda style). Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.[vague]
Because Idris contains a proof assistant, Idris programs can be written to pass proofs around. If treated naïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms.
Idris 2 is a new self-hosted version of the language which deeply integrates a linear type system, based on quantitative type theory. It currently compiles to Scheme. The latest version is 0.2.0, released on May 25, 2020.
- Brady, Edwin (12 December 2007). "Index of /~eb/darcs/Idris". University of St Andrews School of Computer Science. Archived from the original on 2008-03-20.
- "Release 1.3.3". Retrieved 2020-05-25.
- "Uniqueness Types". Idris 1.3.1 Documentation. Retrieved 2019-09-26.
- "Idris, a language with dependent types". Retrieved 2014-10-26.
- "Elaborator Reflection — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- "Code Generation Targets — Idris 1.1.1 documentation". docs.idris-lang.org.
- "Frequently Asked Questions". Retrieved 2015-07-19.
- "Syntax Guide — Idris 1.3.2 documentation". Retrieved 27 April 2020.
- "Erasure By Usage Analysis — Idris 1.1.1 documentation". idris.readthedocs.org.
- "Benchmark results". ziman.functor.sk.
- "Idris 2 version 0.2.0 Released". Retrieved 2020-05-25.
- The Idris homepage, including documentation, frequently asked questions and examples
- Idris at the Hackage repository
- Documentation for the Idris Language (tutorial, language reference, etc.)