Idris

Idris was created by Edwin Brady at the University of St Andrews. It looks like Haskell, but its types are far more expressive: a type can depend on a value, such as the length of a list. That lets the compiler check properties that other languages only test.

Paradigm: Functional Programming

What Makes Idris Special

  • Dependent types. A type like Vect n a is a list of exactly n elements. The number is part of the type.
  • Types as a specification. A function type such as Vect n a -> Vect m a -> Vect (n + m) a states what the function does, and the compiler verifies it.
  • Totality checking. Idris can check that a function terminates and handles every case, which matters when a program is also a proof.
  • Type-driven development. The editor helps you write code from the type: it can split cases, fill holes, and suggest terms.
  • Linear types (Idris 2). Quantities let types track how many times a value is used, which brings safe resource handling.

Example: Vectors whose length is in the type

module Main

import Data.Vect

vappend : Vect n a -> Vect m a -> Vect (n + m) a
vappend []        ys = ys
vappend (x :: xs) ys = x :: vappend xs ys

vhead : Vect (S n) a -> a
vhead (x :: _) = x

main : IO ()
main = do
  let v = vappend [1, 2] [3, 4, 5]
  printLn v
  printLn (vhead v)

How It Works

  • Vect n a is a vector of length n holding elements of type a. n and m are numbers used in types.
  • The signature of vappend says the result has length n + m. If you wrote a body that dropped an element, the program would not compile.
  • vhead takes a Vect (S n) a, a vector of length at least one. Applying it to an empty vector is a type error, so no empty case is needed.
  • It prints [1, 2, 3, 4, 5] and then 1. The compiler proved the safety of vhead v before the program ran.

History and Where It Is Used

Idris is used for research in programming languages and verification, for teaching type-driven development, and for experiments in safe protocols and embedded domain-specific languages. Related proof languages include Agda, Lean and Coq, and lightweight versions of these ideas reach mainstream languages through generics and refined types.

Learn More