This is the in-progress, unofficial user manual for Idris. Contributions are welcome!

• Language features
• Using the REPL
  • REPL commands
  • Colours
  • Initialisation scripts
• Codegen
• Advanced
• Miscellaneous
  • Implicit arguments
  • Typeclasses
• Language extensions
  • Type providers
• Syntax Guide

The command :help (or :h or :?) prints a short summary of the available commands.

If you would like to leave Idris, simply use :q or :quit.

To evaluate an expression, simply type it. If Idris is unable to infer the type, it can be helpful to use the operator the to manually provide one, as Idris's syntax does not allow for direct type annotations. Examples of the include:

Idris> the Nat 4
4 : Nat
Idris> the Int 4
4 : Int
Idris> the (List Nat) [1,2]
[1,2] : List Nat
Idris> the (Vect _ Nat) [1,2]
[1,2] : Vect 2 Nat

This may not work in cases where the expression still involves ambiguous names. The name can be disambiguated by using the with keyword (see Namespaces and type-directed disambiguation):

Idris> sum [1,2,3]
When elaborating an application of function Prelude.Foldable.sum:
        Can't disambiguate name: Prelude.List.::, 
                                 Prelude.Stream.::, 
                                 Prelude.Vect.::
Idris> with List sum [1,2,3]
6 : Integer

To add a let binding to the REPL, use :let. It's likely you'll also need to provide a type annotation. :let also works for other declarations as well, such as data.

Idris> :let x : String; x = "hello"
Idris> x
"hello" : String
Idris> :let data Foo : Type where Bar : Foo
Idris> Bar
Bar : Foo

To ask Idris for the type of some expression, use the :t command. Additionally, if used with an overloaded name, Idris will provide all overloadings and their types. To ask for the type of an infix operator, surround it in parentheses.

Idris> :t "foo"
"foo" : String
Idris> :t plus
Prelude.Nat.plus : Nat -> Nat -> Nat
Idris> :t (++)
Builtins.++ : String -> String -> String
Prelude.List.++ : (List a) -> (List a) -> List a
Prelude.Vect.++ : (Vect m a) -> (Vect n a) -> Vect (m + n) a
Idris> :t plus 4
plus (Builtins.fromInteger 4) : Nat -> Nat

You can also ask for basic information about typeclasses with :doc:

Idris> :doc Monad
Type class Monad

Parameters:
    m

Methods:
    (>>=) : Monad m => m a -> (a -> m b) -> m b
        
        infixl 5
        
Instances:
    Monad id
    Monad PrimIO
    Monad IO
    Monad Maybe

...

Other documentation is also available from :doc:

Idris> :doc (+)
Prelude.Classes.+ : (a : Type) -> (Num a) -> a -> a -> a

infixl 8

Arguments:
        Class constraint Prelude.Classes.Num a
        __pi_arg : a
        __pi_arg1 : a

Idris> :doc Vect
Data type Prelude.Vect.Vect : Nat -> Type -> Type

Arguments:
        Nat
        Type

Constructors:

Prelude.Vect.Nil : (a : Type) -> Vect 0 a


Prelude.Vect.:: : (a : Type) -> (n : Nat) -> a -> (Vect n a) -> Vect (S n) a

infixr 7

Arguments:
        a
        Vect n a

Idris> :doc Monad
Type class Prelude.Monad.Monad
Methods:

Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b

infixl 5

Arguments:
        Class constraint Prelude.Monad.Monad m
        __pi_arg : m a
        __pi_arg1 : a -> m b

The command :apropos searches names, types, and documentation for some string, and prints the results. For example:

Idris> :apropos eq
eqPtr : Ptr -> Ptr -> IO Bool


eqSucc : (left : Nat) -> (right : Nat) -> (left = right) -> S left = S right
S preserves equality

lemma_both_neq : ((x = x') -> _|_) -> ((y = y') -> _|_) -> ((x, y) = (x', y')) -> _|_


lemma_fst_neq_snd_eq : ((x = x') -> _|_) -> (y = y') -> ((x, y) = (x', y)) -> _|_


lemma_snd_neq : (x = x) -> ((y = y') -> _|_) -> ((x, y) = (x, y')) -> _|_


lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_


lemma_x_neq_xs_eq : ((x = y) -> _|_) -> (xs = ys) -> (x :: xs = y :: ys) -> _|_


lemma_x_neq_xs_neq : ((x = y) -> _|_) -> ((xs = ys) -> _|_) -> (x :: xs = y :: ys) -> _|_


prim__eqB16 : Bits16 -> Bits16 -> Int

prim__eqB16x8 : Bits16x8 -> Bits16x8 -> Bits16x8

prim__eqB32 : Bits32 -> Bits32 -> Int

prim__eqB32x4 : Bits32x4 -> Bits32x4 -> Bits32x4

prim__eqB64 : Bits64 -> Bits64 -> Int

prim__eqB64x2 : Bits64x2 -> Bits64x2 -> Bits64x2

prim__eqB8 : Bits8 -> Bits8 -> Int

prim__eqB8x16 : Bits8x16 -> Bits8x16 -> Bits8x16

prim__eqBigInt : Integer -> Integer -> Int

prim__eqChar : Char -> Char -> Int

prim__eqFloat : Float -> Float -> Int

prim__eqInt : Int -> Int -> Int

prim__eqString : String -> String -> Int

prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)

sequence : Traversable t => Applicative f => (t (f a)) -> f (t a)


sequence_ : Foldable t => Applicative f => (t (f a)) -> f ()


Eq : Type -> Type
The Eq class defines inequality and equality.

GTE : Nat -> Nat -> Type
Greater than or equal to

LTE : Nat -> Nat -> Type
Proofs that n is less than or equal to m

gte : Nat -> Nat -> Bool
Boolean test than one Nat is greater than or equal to another

lte : Nat -> Nat -> Bool
Boolean test than one Nat is less than or equal to another

ord : Char -> Int
Convert the number to its ASCII equivalent.

replace : (x = y) -> (P x) -> P y
Perform substitution in a term according to some equality.

sym : (l = r) -> r = l
Symmetry of propositional equality

trans : (a = b) -> (b = c) -> a = c
Transitivity of propositional equality

:search does a type-based search, in the spirit of Hoogle. See Type-directed search (:search) for more details. Here is an example:

Idris> :search a -> b -> a
= Prelude.Basics.const : a -> b -> a
Constant function. Ignores its second argument.

= assert_smaller : a -> b -> b
Assert to the totality checker than y is always structurally
smaller than x (which is typically a pattern argument)

> malloc : Int -> a -> a


> Prelude.pow : Num a => a -> Nat -> a


> Prelude.Classes.(*) : Num a => a -> a -> a


> Prelude.Classes.(+) : Num a => a -> a -> a
... (More results)

:search can also look for dependent types:

Idris> :search plus (S n) n = plus n (S n)
< Prelude.Nat.plusSuccRightSucc : (left : Nat) ->
                                  (right : Nat) ->
                                  S (left + right) = left + S right

The command :l File.idr will load File.idr into the currently-running REPL, and :r will reload the last file that was loaded.

All Idris definitions are checked for totality. The command :total <NAME> will display the result of that check. If a definition is not total, this may be due to an incomplete pattern match. If that is the case, :missing or :miss will display the missing cases.

To list all unproven metavariables, use the command :m. This will display their qualified names and the expected types. To interactively prove a metavariable, use the command :p name where name is the metavariable. Once the proof is complete, the command :a will append it to the current module.

Once in the interactive prover, the following commands are available:

• :q - Quits the prover (gives up on proving current lemma).
• abandon - Same as :q
• state - Displays the current state of the proof.
• term - Displays the current proof term complete with its yet-to-be-filled holes (is only really useful for debugging).
• undo - Undoes the last tactic.
• qed - Once the interactive theorem prover tells you "No more goals," you get to type this in celebration! (Completes the proof and exits the prover)

• compute - Normalizes all terms in the goal (note: does not normalize assumptions)

----------                 Goal:                  ----------
 (Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma> compute
----------                 Goal:                  ----------
 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
-lemma>

• exact - Provide a term of the goal type directly.

----------                 Goal:                  ----------
 Nat
-lemma> exact Z
lemma: No more goals.
-lemma>

• refine - Use a name to refine the goal. If the name needs arguments, introduce them as new goals.

• trivial - Satisfies the goal using an assumption that matches its type.

----------              Assumptions:              ----------
 value : Nat
----------                 Goal:                  ----------
 Nat
-lemma> trivial
lemma: No more goals.
-lemma>

• intro - If your goal is an arrow, turns the left term into an assumption.

----------                 Goal:                  ----------
 Nat -> Nat -> Nat
-lemma> intro
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
 Nat -> Nat
-lemma>

You can also supply your own name for the assumption:

----------                 Goal:                  ----------
Nat -> Nat -> Nat
-lemma> intro number
----------              Assumptions:              ----------
 number : Nat
----------                 Goal:                  ----------
Nat -> Nat

• intros - Exactly like intro, but it operates on all left terms at once.

----------                 Goal:                  ----------
 Nat -> Nat -> Nat
-lemma> intros
----------              Assumptions:              ----------
 n : Nat
 m : Nat
----------                 Goal:                  ----------
 Nat
-lemma>

• let - Introduces a new assumption; you may use current assumptions to define the new one.

----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
 BigInt
-lemma> let x = toIntegerNat n
----------              Assumptions:              ----------
 n : Nat
  x = toIntegerNat n: BigInt
----------                 Goal:                  ----------
 BigInt
-lemma>

• rewrite - Takes an expression with an equality type (x = y), and replaces all instances of x in the goal with y. Is often useful in combination with 'sym'.

----------              Assumptions:              ----------
 n : Nat
 a : Type
 value : Vect Z a
----------                 Goal:                  ----------
 Vect (mult n Z) a
-lemma> rewrite sym (multZeroRightZero n)
----------              Assumptions:              ----------
 n : Nat
 a : Type
 value : Vect Z a
----------                 Goal:                  ----------
 Vect Z a
-lemma> 

• induction - (Note that this is still experimental and you may get strange results and error messages. We are aware of these and will finish the implementation eventually!) Prove the goal by induction. Each constructor of the datatype becomes a goal. Constructors with recursive arguments become induction steps, while simple constructors become base cases. Note that this only works for datatypes that have eliminators: a datatype definition must have the %elim modifier.

Example: To prove associativity of addition on Nat:

module Foo

plusAssoc : plus n (plus m o) = plus (plus n m) o
plusAssoc = ?rhs

we can perform induction on n:

*Foo> :p rhs
----------                 Goal:                  ----------
{ hole 0 }:
 (n : Nat) ->
 (m : Nat) ->
 (o : Nat) ->
 plus n (plus m o) = plus (plus n m) o
-Foo.rhs> intros
----------              Other goals:              ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
----------                 Goal:                  ----------
{ hole 3 }:
 plus n (plus m o) = plus (plus n m) o
-Foo.rhs> induction n
----------              Other goals:              ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
----------                 Goal:                  ----------
elim_Z0:
 plus Z (plus m o) = plus (plus Z m) o
-Foo.rhs> compute 
----------              Other goals:              ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
----------                 Goal:                  ----------
elim_Z0:
 plus m o = plus m o
-Foo.rhs> trivial
----------              Other goals:              ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
----------                 Goal:                  ----------
elim_S0:
 (n__0 : Nat) ->
 (plus n__0 (plus m o) = plus (plus n__0 m) o) ->
 plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
-Foo.rhs> intros
----------              Other goals:              ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
 n__0 : Nat
 ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 5 }:
 plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
-Foo.rhs> compute 
----------              Other goals:              ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
 n__0 : Nat
 ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 5 }:
 S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)
-Foo.rhs> rewrite ihn__0 
----------              Other goals:              ----------
{ hole 5 }
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
 n : Nat
 m : Nat
 o : Nat
 n__0 : Nat
 ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 6 }:
 S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))
-Foo.rhs> trivial 
rhs: No more goals.
-Foo.rhs> qed
Proof completed!
Foo.rhs = proof
  intros
  induction n
  compute 
  trivial
  intros
  compute 
  rewrite ihn__0 
  trivial 

Two goals were created: one for Z and one for S.

• sourceLocation - Solve the current goal with information about the location in the source code where the tactic was invoked. This is mostly for embedded DSLs and programmer tools like assertions that need to know where they are called. See Language.Reflection.SourceLocation for more information.

• applyTactic - Apply a user-defined tactic. This should be a function of type List (TTName, Binder TT) -> TT -> Tactic, where the first argument represents the proof context and the second represents the goal. If your tactic will produce a proof term directly, use the Exact constructor from Tactic.
• attack - ?
• equiv - Replaces the goal with a new one that is convertible with the old one
• fill - ?
• focus - ?
• mrefine - Refining by matching against a type
• reflect - ?
• solve - Takes a guess with the correct type and fills a hole with it, closing a proof obligation. This happens automatically in the interactive prover, so solve is really only relevant in tactic scripts used for helping implicit argument resolution.
• try - ?

The command :e launches your default editor on the current module. After control returns to Idris, the file is reloaded.

The current module can be compiled to an executable using the command :c <FILENAME> or :compile <FILENAME>. This command allows to specify codegen, so for example JavaScript can be generated using :c javascript <FILENAME>. The :exec command will compile the program to a temporary file and run the resulting executable.

Unlike GHCI, the Idris REPL is not inside of an implicit IO monad. This means that a special command must be used to execute IO actions. :x tm will execute the IO action tm in an Idris interpreter.

Sometimes, an Idris program will depend on external libraries written in C. In order to use these libraries from the Idris interpreter, they must first be dynamically loaded. This is achieved through the %dynamic <LIB> directive in Idris source files or through the :dynamic <LIB> command at the REPL. The current set of dynamically loaded libraries can be viewed by executing :dynamic with no arguments. These libraries are available through the Idris FFI in type providers and :exec.

Idris terms are available in amazing colour! By default, the Idris REPL uses colour to distinguish between data constructors, types or type constructors, operators, bound variables, and implicit arguments. This feature is available on all POSIX-like systems, and there are plans to allow it to work on Windows as well.

If you do not like the default colours, they can be turned off using the command

:colour off

and, when boredom strikes, they can be re-enabled using the command

:colour on

To modify a colour, use the command

:colour <CATEGORY> <OPTIONS>

where <CATEGORY is one of keyword, boundvar, implicit, function, type, data, or prompt, and is a space-separated list drawn from the colours and the font options. The available colours are default, black, yellow, cyan, red, blue, white, green, and magenta. If more than one colour is specified, the last one takes precedence. The available options are dull and vivid, bold and nobold, italic and noitalic, underline and nounderline, forming pairs of opposites. The colour default refers to your terminal's default colour.

The colours used at startup can be changed using REPL initialisation scripts.

Colour can be disabled at startup by the --nocolour command-line option.

When the Idris REPL starts up, it will attempt to open the file repl/init in Idris's application data directory. The application data directory is the result of the Haskell function call getAppUserDataDirectory "idris", which on most Unix-like systems will return $HOME/.idris and on various versions of Windows will return paths such as "C:/Documents And Settings/user/Application Data/appName".

The file repl/init is a newline-separate list of REPL commands. Not all commands are supported in initialisation scripts — only the subset that will not interfere with the normal operation of the REPL. In particular, setting colours, display options such as showing implicits, and log levels are supported.

:colour prompt white italic bold
:colour implicit magenta italic

The syntax (| x, y, z |) means to try elaborating all three options and keep the one that works. This is used, for example, when translating integer literals.

Idris> the Nat (| "foo", Z, (-3) |)
0 : Nat

The syntax with NAME EXPR causes members of the namespace NAME to be privileged when resolving overloading. This is particularly useful at the REPL:

Idris> [1,2,3]
Can't disambiguate name: Prelude.List.::, Prelude.Stream.::, Prelude.Vect.::
Idris> with Vect [1,2,3]
[1, 2, 3] : Vect 3 Integer

If you're having a hard time debugging why the unifier won't accept something (often while debugging the compiler itself), try applying the special operator %unifyLog to the expression in question. This will cause the type checker to spit out all sorts of informative messages.

Pattern matching is only allowed on implicit arguments when they are referred by name, e.g.:

foo : {n : Nat} -> Nat
foo {n = Z} = Z
foo {n = S k} = k

or

foo : {n : Nat} -> Nat
foo {n = n} = n

The latter could be shortened to the following:

foo : {n : Nat} -> Nat
foo {n} = n

That is, {x} behaves like {x=x}.

In order to show that an instance of some typeclass is defined for some type, one could use the %instance keyword:

foo : Num Nat
foo = %instance

Idris type providers are a way to get the type system to reflect observations about the world outside of Idris. Similarly to F# type providers, they cause effectful computations to run during type checking, returning information that the type checker can use when checking the rest of the program. While F# type providers are based on code generation, Idris type providers use only the ordinary execution semantics of Idris to generate the information.

A type provider is simply a term of type IO (Provider t), where Provider is a data type with constructors for a successful result and an error. The type t can be either Type (the type of types) or a concrete type. Then, a type provider p is invoked using the syntax %provide (x : t) with p. When the type checker encounters this line, the IO action p is executed. Then, the resulting term is extracted from the IO monad. If it is Provide y for some y : t, then x is bound to y for the remainder of typechecking and in the compiled code. If execution fails, a generic error is reported and type checking terminates. If the resulting term is Error e for some string e, then type checking fails and the error e is reported to the user.

Example Idris type providers can be seen at this repository. More detailed descriptions are available in David Christiansen's WGP '13 paper and M.Sc. thesis.