-
Notifications
You must be signed in to change notification settings - Fork 3
Unofficial FAQ
Based on conversations from the #idris IRC channel.
It's covered in section 12.6 JavaScript Target of the tutorial. Some javascript notes are in the works.
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.
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
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.
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 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.
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.
- (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
andage
live in thePerson
namespace.
-
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.
As-patterns (of the form list@(x:xs)
) are not available in Idris at the moment.
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.
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 commandline 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.
<edwinb> Doing modules right is a research problem I have almost no interest in. Not that I'm stopping anyone else.
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.
Because Monad inherits from Applicative, some duplicated operations are not present. See traverse
in Prelude.Applicative
.
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},
}
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
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.
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