-
Notifications
You must be signed in to change notification settings - Fork 3
Unofficial FAQ
Based on conversations from the #idris IRC channel.
Sometimes when invoking cabal update; cabal install idris
cabal will complain about possible package breakage. For example:
regex-base-0.93.2 (reinstall) changes: mtl-2.1.2 -> 2.2.1
cabal: The following packages are likely to be broken by the reinstalls:
regex-posix-0.95.2
regex-compat-0.95.1
Use --force-reinstalls if you want to install anyway.
Here cabal is complaining that some of your packages are not up-to-date. First try cabal update
if you haven't done so already. If that is not successful, then cabal has some flags that might be helpful in resolving package selection:
--reinstall Install even if it means installing the same version again.
--avoid-reinstalls Do not select versions that would destructively overwrite installed packages.
--force-reinstalls Reinstall packages even if they will most likely break other installed packages.
--upgrade-dependencies Pick the latest version for all dependencies, rather than trying to pick an installed version.
Please try those.
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.
Idris has typed laziness as of February 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.
It's covered in section 12.6 JavaScript Target of the tutorial. Some JavaScript notes are in the works.
API documentation for the shipped packages is listed on the documentation page Unfortunately, the default prelude and shipped packages for Idris
are not necessarily complete with regards to documentation.
Other ways to find functions include:
- REPL commands:
- Use
:apropos
to search for text in documentation and function names. - Use
:search
to search for functions of a given type. - Use
:browse
to list the contents of a given namespace.
- Use
- Use the REPL’s auto-complete functionality.
- Grep through the source code in
libs/
If you find that the shipped packages are lacking in documentation, please feel free to write some. Or bug someone to do so.
Idris
has syntax for providing rich documentation, which is then viewable using the :doc
command and listed in generated HTML API documentation.
Guidelines for documentation are also in development.
Idris has an IRC channel (#idris) on Freenode. Our policy is that we do not log IRC chat at all; IRC should be seen as a rolling conversation. That being said sometimes the discussions on IRC can be useful as a basis for generating FAQ answers, user/dev documentation, and the logging/resolving of issues. If you feel that an IRC discussion you have witnessed should be made into an issue/FAQ/documentation, please be considerate and ask permission of those involved for their opinions to be placed in a more permanent place. Please also be considerate if those people ask you to amend results if they believe that there was an error in the transcription.
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
When you want to use Foo
in other modules, don't forget to public export
it. Otherwise, the type checker doesn't know that Foo
and Integer
represent the same type.
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.
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 accidentally 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.
-
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 typeVoid
and usevoid : Void -> a
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 -> Void) -> Void
-- 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.
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
tbl
In the past some users have mentioned that Float
and Double
should be renamed Float32
and Float64
to adhere to 'more modern' naming conventions. Idris has Float
and Double
because that is what the developer decide upon at the time. If you feel that the names should be changed then please submit a PR addressing Issue #379
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.
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.
Idris works well under MinGW: see Idris on Windows. Alternatively, users have reported success using Idris with Cygwin by doing the following:
-
Install Haskell Platform
-
Install Cygwin then additionally install the following packages:
- make
- libgmp-devel
- gcc-mingw
-
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 command line install the package then
cabal install
Then just run make in the folder that you downloaded Idris to.
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.
Modules in Idris support separate typechecking and namespaces, and so aren't sophisticated modules in the ML sense. You can achieve similar kinds of abstraction to ML modules using interfaces, since (like ML modules) interfaces can include data type and function declarations, and have multiple implementations to be used in different contexts. Also, interfaces are first class, so you can construct implementations at run time, choosing an appropriate implementation for a given context.
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 normalizes the terms, while the proof shell requires the user to control normalization by hand. This is to make it easier to use rewriting, which uses a purely syntactic match.
Because Monad inherits from Applicative, some duplicated operations are not present. See traverse
in Prelude.Traversable
.
(->)
is a binder in Idris, not an operator, because (->)
needs to be able to introduce new names for arguments. Trying to write the type of (->)
sheds some more light on this.
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).
12:49 CEST < edwinb> you might want a different form before you do a rewrite
12:49 CEST < edwinb> you can also use 'equiv'
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},
}
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
By default, cabal installs sandboxed executables into .cabal-sandbox/bin/
, so don't forget to add that into your PATH
.
Binary Packages
Tool Support
Community
- Libraries, available elsewhere
- Idris Developer Meetings
- The Zen of Idris
Development