Idris

A language with dependent types

Introduction | Examples | Documentation | Download

Introduction

Idris is an experimental language with full dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. There is now a tutorial developing.

The aims of the project are:

• To provide a platform for realistic programming with dependent types. By realistic, we mean the ability to interact with the outside world and use primitive types and operations, to make a dependently typed language suitable for systems programming. This includes networking, file handling, concurrency, etc.
• To show that full dependent types do not mean we have to abandon the functional style we have come to know and love with languages like Haskell and OCaml. We aim to show that lightweight dependently typed programming means allowing the programmer full access to values in types, and letting the type checker do the hard work so you don't have to!

See darcs repository. You can also look there for library code. Some particular things worth looking at are:

• adder.idr, a variadic adder. This uses dependent types to define a function which can take a variable number of arguments in a type safe way.
• partition.idr, length preserving quicksort. Defines vectors (lists with a statically known length) and partitions of vectors. As you see, there are no local definitions or where clauses yet (there will be). This example requires a small amount of theorem proving, to show that moving a value from the front to the middle of a list results in a list of the same length (in mkPartitionR).
• interp.idr, a type preserving interpreter. Every dependently typed language has to be able to do this! It's our version of "Hello world". Note in particular fPlus and fPlusInf. They need some type information, because terms are defined with respect to an environment. fPlus does this by explicitly stating the type, fPlusInf just provides a starting environment which is actually all the type checker needs.
• hello.idr, speaking of hello world... this one does some I/O, and demonstrates the rudimentary do notation.
• concurrent.idr, a test for the concurrency primitives. I want to be able to write type-safe concurrent code, so fork and some locking functions will help.

The most comprehensive documentation at the moment is the tutorial. Downloading and installing, and running a first program is described here.

Download

• The most recent tarball, including Epic and Ivor is always available from http://www-fp.cs.st-and.ac.uk/~eb/idris/idris-current.tgz.
• darcs get http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris

Requires GHC version 6.10 or greater to build; earlier versions should work but will need some fiddling.

You'll also need Ivor the Proof Engine. I will at some point make a release that collects all the non-standard stuff you need into one tarball.

Edwin Brady -- eb@dcs.st-and.ac.uk -- 29th November 2009