Unofficial FAQ

Based on conversations from the #idris IRC channel.

Where is the official FAQ?

• http://idris-lang.org/documentation/faq

How does the Javascript back-end work?

It's covered in section 12.6 JavaScript Target of the tutorial. Some javascript notes are in the works.

Is there some documentation for the standard lib? List of functions?

Unfortunately, the default prelude and shipped packages for Idris are not necessarily complete with regards to documentation. Ways to find out the list of functions that are shipped with Idris are as follows:

• Grep through the source code in libs/
• Use the REPLs auto-complete functionality.
• Make use of the :apropos command.

If you find that the shipped packages are lacking in documentation, please feel free to write some. Or bug someone to do so. Idris does have support for providing rich documentation, that is viewable using the :doc command. Guidelines for documentation are also in development. A Haddock like HTML generator for Idris code will be developed in the near future.

Can I do type aliases in Idris?

Yes, yes you can!

Within Idris, types are a first class language construct and can be manipulated like any other value. This makes the creation of type aliases rather simple. You define a new variable that represents the type. For example, the following Haskell code

type Foo = Integer

can be replicated in Idris as:

foo : Type
foo = Integer

Why isn't Idris lazy?

Idris is a total language, which means it has the Church-Rosser property, therefore we can reduce expressions however we want, lazily or eagerly, and the result will be the same.

However, in practice, laziness presents problems for reasoning about performance. In particular, laziness can make it hard to reason about the predictability of a program. Laziness can be made efficient as evidenced by Haskell compilers such as GHC. Furthermore, some of the benefits of laziness cannot be realized in total languages.

In Haskell, we can define new operators with "short circuit" behavior (like C's boolean evaluation for if-statements). This allows undefined or non-terminating terms to not be evaluated when the result is not needed. However, in a total language we don't have undefined and non-terminating terms so we need not worry about evaluating them.

To summarize, the choice lazy vs. eager does not make a theoretical difference, we don't need to worry about evaluating an undefined or non-terminating term, and eager evaluation is more predictable.

Will there be support for unicode characters for operators?

Taken from the following comment. There are several reasons why we should not support unicode operators:

• It's hard to type (this is important if you're using someone else's code, for example). I know various editors have their own input methods, but you have to know what they are.
• Not every piece of software easily supports it. It doesn't render properly on my phone email client, for example, occasionally messes up the terminal I run my irc client in, doesn't always render properly in my browser, etc. All of these are things I can fix but to have to do so as a barrier to entry to using a programming language doesn't seem to be a good idea to me.
• Even if we leave it out of the standard library (which we will in any case!) as soon as people start using it in their library code, others have to deal with it.
• Too many characters look too similar. We had enough trouble with confusion between 0 and O without worrying about all the different kinds of colons and brackets.
• There seems to be a tendency to go over the top with use of Unicode. For example, using sharp and flat for delay and force (or is it the other way around?) in Agda seems gratuitous. I really don't want to encourage this sort of thing, when words are often better.

I know that used with care it can make things look pretty. But so can lhs2TeX. And I'm sure that in a few years time things will be different and software will cope better and it will make sense to revisit this. For now, however, I would prefer not to allow arbitrary unicode symbols in operators.

What does Incorrect ibc version -- please rebuild warning mean?

Idris has an intermediary bytecode representation that contains a successfully typed Idris program: ibc files. As part of the bytecode representation the version of Idris used is noted. When upgrading between different versions of Idris stale ibc files can be accidently left lying around. Using stale ibc files with the current release will result in a ibc version mismatch.

This warning can be easily fixed by purging your project of all generated ibc files and rebuilding your project. The idris-dev has a relib target for such purposes.

Can I have lazy evaluation if I want it?

Idris has typed laziness as of Februrary 2014. As stated in an email by Edwin Brady

It is defined like so:

data Lazy : Type -> Type where
     Delay : (val : a) -> Lazy a

Force : Lazy a -> a
Force (Delay x) = x

Fortunately, Force and Delay can be left implicit - the elaborator knows about 'Lazy' and will insert Force and Delay as necessary to make a term well-typed. This means that in most cases you won't have to do anything special.

Idris used to have laziness annotations: In a function declaration, a parameter can be made lazy be prefixing it with | (pipe character). For example,

or : Bool -> |Bool -> Bool
or : True _     = True
or : False True = True

only evaluates its second argument if the first is False.

Where are records?

• (2012-01-27) The 'record' keyword is just like the 'data' keyword except that you can only have one constructor, and you need to annotate the binders with names to get projection functions.

For example,

record Foo : Nat -> Type where
     MkFoo : (name : String) ->
             (things : Vect a n) ->
             Foo n

Now it is possible to instantiate a Foo record with MkFoo someString someVect and project the contents with name and thing.

• (2012-01-27) Records can be updated with the syntax record { field = val } x.

For example,

record Person : Type where
    MkPerson : (name : String) -> (age : Int) -> Person

newName : Person -> String -> Person 
newName p n = record { name = n } p

Update syntax is first class, so record { name = n } is itself a function. Updates can change the type of fields, provided that they do not change the type of the record or update the values of other fields (except if those fields are implicit).

• Field names live in their own sub-namespace. So in the above example, name and age live in the Person namespace.

Where is Agda's () pattern and what is impossible?

• impossible is a keyword used under certain circumstances to signal that a particular function pattern can never match. However, impossible cannot be used under all such circumstances, and is actually fairly limited. For the general case of proving that a particular pattern is impossible, construct a value of type _|_ and use FalseElim to return a value of the correct type.

impossible can only be used if the pattern it applies to cannot be unified. For example, in

f : (n : Nat) -> Vect n a -> Nat
...
f Z (_::_) impossible
f (S _) [] impossible

both "impossible" cases generate conflicting constraints for n: it must match both S k and Z.

impossible can't be used to implement functions like this:

g : a -> (a -> _|_) -> _|_
-- g _ _ impossible -- WRONG!
g a notA = notA a

Here, the impossibility is not caught by the compiler during the unification phase, so impossible doesn't work (and if you try, the compiler will complain that "this is a valid case"). Instead, we need to implement a function body.

Where are Haskell's as-patterns?

As-patterns (of the form list@(x:xs)) are not available in Idris at the moment.

Can't propositional arguments be made implicit?

For example, isCons l = True in the following,

head : (l : List a) -> (isCons l = True) -> a
head (x::xs) p = x

• (2012-01-26) Maybe in the future we can have a trivial tactic that fills in such things.

• (later 2012-01-26) The future is here.

The following should work:

head : (xs : List a) -> {auto p : isCons xs = True} -> a
head (x :: xs) = x

Why are there both Haskell-style and GADT/Agda-style data declarations? Doesn't the latter subsume the former?

• Sometimes Haskell-style is less verbose.

Why does my instance declaration give the error "Can't resolve instance"?

This can be a result of not having fulfilled the prerequisites for the instance. For example, if you try to implement Monad for your type F without first implementing Functor and Applicative, you may get the message:

Can't resolve type class Monad F

on the line that begins your instance declaration. Inspect the type class definition to find out what prerequisites there are.

Does Idris work with Cygwin?

Idris works well under MinGW: see Idris on Windows. Alternatively, users have reported success using Idris with Cygwin by doing the following:

1. Install Haskell Platform

2. Install Cygwin then additionally install the following packages:

   • make
   • libgmp-devel
   • gcc-mingw

3. At the Cygwin console, run cabal install idris

You should add %AppData%\cabal\bin to your Path environment variables so you can run idris from the console. Now you should be able to run Idris from Powershell and Cygwin.

To use versions greater than 0.9.7, also install the Cygwin packages:

• libffi-devel
• pkg-config
• libffi

A tiny change needs to be made to the Haskell bindings for libffi to get them to work with Cygwin. Run

cabal unpack libffi

Now you need to go into the file libffi.cabal and delete the following two lines

pkgconfig-depends: libffi
extra-libraries:    ffi

In the commandline install the package then

cabal install

Then just run make in the folder that you downloaded Idris to.

Can I use C structs directly when binding functions through the FFI?

Currently there is no support for this. It is technically feasible, but at the moment the focus has been on keeping the FFI simple. Patches implementing this functionality will be considered, but there is no guarantee at this time. The best approach would be to contact edwinb and the other idris developers before starting in on the work.

Why is the module system so basic/limited?

<edwinb> Doing modules right is a research problem I have almost no interest in. Not that I'm stopping anyone else.

My proof works in the file, but not interactively. What gives?

The following code type checks, but if you comment out the proof and try to do it in the interpreter via :p, it needs an additional compute before intros or it won't work:

multOneRight : (left : Nat) -> left * 1 = left
multOneRight O        = refl
multOneRight (S left) =
  let inductiveHypothesis = multOneRight left in
      ?multOneRightStepCase

multOneRightStepCase = proof
  intros
  rewrite inductiveHypothesis
  trivial

This is because the type checker normalises the terms, while the proof shell requires the user to control normalisation by hand. This is to make it easier to use rewriting, which uses a purely syntactic match.

Where is mapM?

Because Monad inherits from Applicative, some duplicated operations are not present. See traverse in Prelude.Applicative.

Why do functions without accompanying definitions type check?

Idris supports type checking and using incomplete functions at the REPL to better aid the interactive development process, similarly to functions with meta-variables. However, it is still not possible to compile those incomplete programs (as expected).

Why do I have to use the compute tactic manually?

12:49 CEST < edwinb> you might want a different form before you do a rewrite
12:49 CEST < edwinb> you can also use 'equiv'

What paper should I cite, if I want to reference Idris?

Use the one from the Journal of Functional Programming:

EDWIN BRADY (2013). Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23, pp 552-593. doi:10.1017/S095679681300018X.

or in BibTex:

@article{JFP:9060502,
author = {BRADY,EDWIN},
title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
journal = {Journal of Functional Programming},
volume = {23},
issue = {05},
month = {9},
year = {2013},
issn = {1469-7653},
pages = {552--593},
numpages = {42},
doi = {10.1017/S095679681300018X},
URL = {http://journals.cambridge.org/article_S095679681300018X},
}

Building Idris

Can Idris be built without the LLVM backend?

Yes, it can. If the LLVM flag is set to false in the cabal invocation the LLVM backend will be stubbed out and none of its dependencies will be required to build Idris. The flag is passed like this: cabal install -f -LLVM

How do I get cabal to find gc.h?

This is an open bug; see https://github.com/edwinb/Idris-dev/issues/427. The work-around, if you're using linux (or some other OS) with pkg-config installed, is to install gc (you can manually install gc from http://www.hpl.hp.com/personal/Hans_Boehm/gc/gc_source/; I installed 7.2d, but I don't think it matters much), and then, assuming you are building from source, apply https://github.com/edwinb/Idris-dev/pull/428 locally.

Cabal fails to install Idris, what could I do?

If you have not forgot to cabal update, it could be caused by dependency issues, and in most cases it helps to create a sandbox:

cabal sandbox init
cabal install idris

If the problem is not in dependencies, it could be caused by unexpected updates of the packages used by Idris, in which case it might help to get a fresh (development) version from github:

git clone git@github.com:idris-lang/Idris-dev.git
make

I have installed Idris into a cabal sandbox, but where is the executable?

By default, cabal installs sandboxed executables into .cabal-sandbox/bin/, so don't forget to add that into your PATH.