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.

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. 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!

Future plans include some more useful syntax (local definitions/where clauses being the most important), a compiler, links to the Ivor theorem prover and pluggable decision procedures.

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.

Imagine there is some documentation here. Take a look at some code samples until it appears!

To load a program foo.idr, enter idris foo.idr at the shell prompt. You can then enter expressions to be evaluated. An expression of type IO a for some a will be executed (slowly, at the moment). You may get error messages, which will probably be incomprehensible. I will deal with this soon too...

Some notes on some less obvious features will be useful, however:

• # is the type of types.
• Function types are written (x:A)->B, or A->B if x does not appear free in B.
• There are some built in types:
  • Dependent equality; a=b. There is no need for a and b to be the same type. refl a is an instance of a=a.
  • The unit type, () with one instance, II.
  • The empty type, _|_ with no instances.
  • Int and String as normal, and Bool with constructors True and False.
  • Resources; Lock for semaphores, Handle for files.

• If a name appears in a type without being declared, it is made implicit and its type must be inferrable. e.g. in
  f:Nat -> (B x)
  then assuming the type of B is known (e.g. B:Nat->#), then the type of x is inferrable and should not be written down when f is called, e.g.
  f (S O).
  If you want to make x explicit with some value y, write the call as
  f {x=y} (S O).

  Implicit arguments can also be written down explicitly, e.g. in
  f:{x:Nat}->Nat->(B x),
  x is implicit --- this is identical to the declaration above.

• There are arithmetic operators, +,-,*,/. String concatenation is ++. Comparison operators, which return a Bool, are <, >, <=, >= and ==.
• There is Haskell style do notation for the IO monad, e.g:
do {
  x <- getStr;
  putStrLn x;
}