idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-08-17 17:20:23 +03:00
Code Issues Projects Releases Wiki Activity

FAQ/CONTRIBUTION updates

Browse Source 
We had a lot of things missing here, and the contributing guidelines
were extremely out of date and reflected the state when I first made the
Idris 2 repo public. I've updated both to reflect the current state of
the way we work, and to give better guidelines about what will be most
helpful.
This commit is contained in:
Edwin Brady 2021-07-16 11:16:46 +01:00
parent a20aba63ee
commit 3ee965e30d
5 changed files with 404 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

209
CONTRIBUTING.md
View File

@ -1,80 +1,155 @@
Contributing to Idris 2
=======================
Contributions are welcome! The most important things needed at this stage,
beyond work on the language core, are (in no particular order):
We welcome contributions! This document describes how you can contribute to
Idris 2, and the kind of contributions which will most benefit the project.
* Documentation string support (at the REPL and IDE mode).
* Generating HTML documentation from documentation strings (and possibly other
formations)
* A better REPL, including:
- `it` and `:let`
- readline and tab completion
- `:search` and `:apropos`
- help commands
- code colouring
- it'd be nice if Ctrl-C didn't quit the whole system!
* IDE mode improvements
- Syntax highlighting support for output
- Several functions from the version 1 IDE protocol are not yet implemented,
and I haven't confirmed it works in everything.
- (Not really part of Idris 2, but an editing mode for vim would be lovely!)
* Some parts of the Idris 1 Prelude are not yet implemented and should be
added to base/
* The lexer and parser are quite slow, new and faster versions with better
errors would be good.
- In particular, large sections commented out with {- -} can take a while
to lex!
* An alternative, high performance, back end. OCaml seems worth a try.
* JS and Node back ends would be nice.
* A Jupyter kernel for Idris, to allow for more industry standard literate programming.
Please remember when making contributions via pull requests, though, that Idris
is primarily a research project, and we are a small team, which limits the time
we have available for reviewing and maintaining PRs. Nobody works full time on
Idris - we're a team of academics and students at a university with other
demands on our time such as teaching, and writing and presenting research
papers, which will always take priority. This also means we have to be careful
to make sure that we can commit to maintaining any new features which are
contributed.
The default Prelude describes the rationale for what gets included and what
doesn't. Mostly what is there is copied from Idris 1, but it's not impossible
I've made some silly mistakes on the way. If you find any, please let me know
(or even better, submit a PR and a test case!).
This document outlines: the kinds of contributions we will almost certainly
accept; those we might accept; those we might accept after a proposal and
discussion; and, those we almost certainly won't. The guidelines here are based
on decisions we've previously made, and the way we have managed PRs in practice
up to now.
Some language extensions from Idris 1 have not yet been implemented. Most
notably:
General comments
----------------
* Type providers
- Perhaps consider safety - do we allow arbitrary IO operations, or is
there a way to restrict them so that they can't, for example, delete
files or run executables.
* Elaborator reflection
- This will necessarily be slightly different from Idris 1 since the
elaborator works differently. It would also be nice to extend it with
libraries and perhaps syntax for deriving implementations of interfaces.
Overall, when making a contribution, please try to make sure they follow the
general philosophy of the Idris project, which can be summarised as follows:
Other contributions are also welcome, but I (@edwinb) will need to be
confident that I'll be able to maintain them!
* Idris aims to make advanced type-related programming techniques accessible to
software practitioners
* Idris *allows* software developers to express invariants of their data and prove
properties of programs, but will not *require* them to do so
Many contributions will require acccompanying tests and documentation updates.
Bug fixes in particular should be accompanied by tests, to avoid future
regressions.
Library functions should be `total` as far as possible, and at least `covering`
where `total` is not possible.
Different people have different preferences about coding style. In general,
we haven't been too prescriptive about this. If you're editing a source file,
try to be consistent with the existing style choices made by previous authors.
We may need to be more formal about this in future!
Please remember to update CHANGELOG.md, and if it's your first contribution you
can add yourself to CONTRIBUTORS.
In all cases, a pull request must have a short description (one sentence is
usually enough) that explains its purpose. However obvious you think it might
be, it really helps when reviewing the changes.
Things we will almost certainly accept
--------------------------------------
* Anything which fixes an issue on the issue tracker
- In this case, please make sure you include a new test
* More tests, which test new features or, more importantly, existing features
which are not exercised enough in the existing tests
- Note that the 'test' subdirectory is intended for testing the type checker
and compiler, not specifically for testing libraries. However, we do need
a better way of testing libraries! (More on this below)
* Rewrites of existing features which demonstrably improve performance
* Documentation, and improvements to documentation generation tools
* Improvements to existing tool support, including:
- Type-driven program synthesis
- :search and related REPL commands
- Interactive editing
* Contributions of missing library functions, including proofs, which were
available in Idris 1 - at least on the assumption that we still think the
function is important enough, which gets increasingly unlikely over time!
Things we might accept
----------------------
* Additions to the `contrib` libraries
- However, please consider whether it would be better as a separate library.
If something is in the Idris2 repository, we need to commit to maintaining
it to some extent, so we have to be sure that we can do so. You can find
(and contribute to) a list of `libraries on the wiki <https://github.com/idris-lang/Idris2/wiki/Libraries>`_.
- For any library additions, please try to include as many documentation
strings as you can.
Things that should be discussed via the issue tracker first
-----------------------------------------------------------
* New language features
- Syntactic sugar, for example, is nice but any new feature needs to be
worth the additional burden it places on programmers learning the language
* Changes to any of the core representations (TT and CExp in particular)
- These have been fairly stable for a while, and external tools using the
Idris 2 API may be depending on them
* Changes to prelude and base libraries
- 'prelude' and 'base' are, in some sense, part of the language. There are a
lot of trade offs to be made in the design of the prelude especially - such
as interface hierarchies - and while you may not agree with the way it looks,
by and large these decisions have already been made so there must be a
compelling reason for them to be changed.
* Any fundamental changes to build system, library structure, or CI workflow
* Major refactorings (e.g. reorganisation of imports, mass renamings). These
may be a good idea, but they are often merely a matter of taste, so please
check whether they will be considered valuable first.
* A new approach to testing libraries: we don't have a unit testing or
property testing framework as part of the Idris system, itself, though it
would be valuable for testing the prelude and base libraries. This would be
nice to have, so proposals are welcome.
Things we probably won't accept
-------------------------------
* Minor refactorings. You may be making the code more beautiful, or more to
your taste, but please remember that every PR has to be reviewed, and if it
takes more time to run the tests and review it than it took to make the change,
it's costing us time rather than saving it.
- On the other hand, tidying up code as part of a larger PR is very welcome.
We encourage following the camp site rule: leave the code tidier than you
found it!
* Primitive updates without a strong justification
- Primitives increase the burden on back end authors, for example. They may
be necessary to support a new library, if a foreign function call is not
appropriate, but we won't accept a primitive on the basis that it could be
useful in future.
* Requests to migrate libraries from `contrib` to `base`. We do need to
organise libraries better, but this will be better achieved with a good
package manager.
* Fancy REPL features (e.g. readline, history, tab completion). We definitely
want this, but it would be better implemented as a separate tool using the
Idris 2 API, to minimise the maintenance burden on the compiler.
* Similarly, anything which adds an external dependency. We aim to keep
dependencies minimal for ease of initial installation.
* New back ends. You can implement new back ends via the Idris 2 API - and indeed
several people have. The back ends in this repository are limited to those
we are able to commit to maintaining.
Other possible contributions
----------------------------
There's plenty of other things that might be good ideas. If it isn't covered
above, and you're in doubt as to whether it might be a good idea, please let us
know that you're considering it and we can discuss how well it will fit. Please
just remember that whatever you contribute, we have to maintain!
Good places to discuss possible contributions are:
* The `mailing list <https://groups.google.com/forum/#!forum/idris-lang>`_.
* The Idris community on Discord `(Invite link) <https://discord.gg/YXmWC5yKYM>`_
* The issue tracker (in this case, please make your proposal as concrete as
possible).
On performance
--------------
If you're editing the core system, or adding any features, please keep an
eye on performance. In particular, check that the libraries build and tests
run in approximately the same amount of time before and after the change.
(Although running faster is fine as long as everything still works :))
Libraries
---------
Further library support would be very welcome, but unless it's adding something
that was in `prelude/` or `base/` in Idris 1, please add it initially into
`contrib/`. (We'll reorganise things at some point, but it will need some
thought and discussion).
Think about whether definitions should be `export` or `public export`. As
a general rule so far, type synonyms and anything where the evaluation
behaviour might be useful in a proof (so very small definitions) are
`public export` and everything else which is exported is `export`.
Syntax
------
Some things from Idris 1 definitely won't be implemented:
* `%access` directives, because it's too easy to export things by accident
* Uniqueness types (instead, Idris 2 is based on QTT and supports linearity)
* Some esoteric syntax experiments, such as match applications
* Syntax extensions (at least in the unrestricted form from Idris 1)
* DSL blocks (probably) unless someone has a compelling use case that can't
be done another way

6
README.md
View File

@ -92,18 +92,14 @@ lists the current plugins available for common text editors and their features.
Things still missing
--------------------
+ Disambiguation via 'with'
+ Cumulativity (so we currently have Type : Type! Bear that in mind when you
think you've proved something :))
+ 'rewrite' doesn't yet work on dependent types
+ Parts of the ide-mode, particularly syntax highlighting
+ Documentation strings and HTML documentation generation
+ ':search' and ':apropos' at the REPL
+ Metaprogramming (reflection, partial evaluation)
Contributions wanted
-------------------
+ [Contribution guidelines](CONTRIBUTING.md)
+ [Good first issues](https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22)
+ [Contributors wanted](https://github.com/idris-lang/Idris2/wiki/Contributions-wanted)

252
docs/source/faq/faq.rst
View File

@ -2,6 +2,37 @@
Frequently Asked Questions
**************************
What are the aims of the Idris project?
=======================================
Idris aims to make advanced type-related programming techniques accessible to
software practitioners. An important philosophy that we follow is that
Idris *allows* software developers to express invariants of their data and
prove properties of programs, but will not *require* them to do so.
Many of the answers in this FAQ demonstrate this philosophy, and we always
bear this in mind when making language and library design decisions.
Idris is primarily a research project, led by Edwin Brady at the University
of St Andrews, and has benefited from SICSA (https://www.sicsa.ac.uk) and
EPSRC (https://www.epsrc.ac.uk/) funding. This does influence some design
choices and implementation priorities, and means that some things are not
as polished as we'd like. Nevertheless, we are still trying to make it as
widely usable as we can!
Where can I find libraries? Is there a package manager?
=======================================================
We don't yet have a package manager, but you can still find a source of
libraries on the wiki: https://github.com/idris-lang/Idris2/wiki/Libraries
Fortunately, the dependencies are currently not that complicated, but we'd
still like a package manager to help! There isn't an official one yet, but
two are in development:
* Inigo: https://github.com/idris-community/inigo
* sae: https://github.com/DoctorRyner/sae
Can Idris 2 compile itself?
===========================
@ -92,11 +123,220 @@ install `rlwrap <https://linux.die.net/man/1/rlwrap>`_, this
utility provides command history simply by invoking the Idris2
repl as an argument to the utility ``rlwrap idris2``.
The goal, eventually, is to use the IDE mode as the basis of an implementation
of a sophisticated REPL, developed independently from the Idris 2 core.
The goal, eventually, is to use the IDE mode or the Idris API as the basis of
an implementation of a sophisticated REPL, developed independently from the
Idris 2 core. As far as we know, nobody is yet working on this: if you're
interested, please get in touch and we can help you get started!
Where can I find more answers?
==============================
Why does Idris use eager evaluation rather than lazy?
=====================================================
Idris uses eager evaluation for more predictable performance, in particular
because one of the longer term goals is to be able to write efficient and
verified low level code such as device drivers and network infrastructure.
Furthermore, the Idris type system allows us to state precisely the type
of each value, and therefore the run-time form of each value. In a lazy
language, consider a value of type ``Int``:
.. code-block:: idris
thing : Int
What is the representation of ``thing`` at run-time? Is it a bit pattern
representing an integer, or is it a pointer to some code which will compute
an integer? In Idris, we have decided that we would like to make this
distinction precise, in the type:
.. code-block:: idris
thing_val : Int
thing_comp : Lazy Int
Here, it is clear from the type that ``thing_val`` is guaranteed to be a
concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an
``Int``.
How can I make lazy control structures?
=======================================
You can make control structures using the special Lazy type. For
example, one way to implement a non-dependent ``if...then...else...``
would be via a function named ``ifThenElse``:
.. code-block:: idris
ifThenElse : Bool -> (t : Lazy a) -> (e : Lazy a) -> a
ifThenElse True t e = t
ifThenElse False t e = e
The type ``Lazy a`` for ``t`` and ``e`` indicates that those arguments will
only be evaluated if they are used, that is, they are evaluated lazily.
By the way: we don't actually implement ``if...then...else...`` this way in
Idris 2! Rather, it is transformed to a ``case`` expression which allows
dependent ``if``.
Evaluation at the REPL doesn't behave as I expect. What's going on?
===================================================================
Being a fully dependently typed language, Idris has two phases where it
evaluates things, compile-time and run-time. At compile-time it will only
evaluate things which it knows to be total (i.e. terminating and covering all
possible inputs) in order to keep type checking decidable. The compile-time
evaluator is part of the Idris kernel, and is implemented as an interpreter
in Idris. Since everything is known to have a normal form here, the evaluation
strategy doesn't actually matter because either way it will get the same
answer! In practice, it uses call by name, since this avoids evaluating
sub-expressions which are not needed for type checking.
The REPL, for convenience, uses the compile-time notion of evaluation. As well
as being easier to implement (because we have the evaluator available) this can
be very useful to show how terms evaluate in the type checker. So you can see
the difference between:
.. code-block:: idris
Main> \n, m => S n + m
\n, m => S (plus n m)
Main> \n, m => n + S m
\n, m => plus n (S m)
If you want to compile and execute an expression at the REPL, you can use
the ``:exec`` command. In this case, the expression must have type ``IO a``
(for any ``a``, although it won't print the result).
Why can't I use a function with no arguments in a type?
=======================================================
If you use a name in a type which begins with a lower case letter, and which is
not applied to any arguments, then Idris will treat it as an implicitly
bound argument. For example:
.. code-block:: idris
append : Vect n ty -> Vect m ty -> Vect (n + m) ty
Here, ``n``, ``m``, and ``ty`` are implicitly bound. This rule applies even
if there are functions defined elsewhere with any of these names. For example,
you may also have:
.. code-block:: idris
ty : Type
ty = String
Even in this case, ``ty`` is still considered implicitly bound in the definition
of ``append``, rather than making the type of ``append`` equivalent to...
.. code-block:: idris
append : Vect n String -> Vect m String -> Vect (n + m) String
...which is probably not what was intended! The reason for this rule is so
that it is clear just from looking at the type of ``append``, and no other
context, what the implicitly bound names are.
If you want to use an unapplied name in a type, you have three options. You
can either explicitly qualify it, for example, if ``ty`` is defined in the
namespace ``Main`` you can do the following:
.. code-block:: idris
append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty
Alternatively, you can use a name which does not begin with a lower case
letter, which will never be implicitly bound:
.. code-block:: idris
Ty : Type
Ty = String
append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty
As a convention, if a name is intended to be used as a type synonym, it is
best for it to begin with a capital letter to avoid this restriction.
Finally, you can turn off the automatic binding of implicits with the
directive:
.. code-block:: idris
%auto_implicits off
In this case, you can bind ``n`` and ``m`` as implicits, but not ``ty``,
as follows:
.. code-block:: idris
append : forall n, m . Vect n ty -> Vect m ty -> Vect (n + m) ty
Why don't the ``Functor``, ``Applicative``, ``Monad`` and other interfaces include the laws?
============================================================================================
On the face of it, this sounds like a good idea, because the type system allows
us to specify the laws. We don't do this in the prelude, though, for two
main reasons:
* It goes against the philosophy (above) that Idris *allows* programmers to
prove properties of their programs, but does not *require* it.
* A valid, lawful, implementation may not necessarily be provably lawful
within the Idris system, especially if it involves higher order functions.
There are verified versions of the interfaces in ``Control.Algebra``, which
extend interfaces with laws.
I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
=============================================================================================
Idris can't decide in general whether a program is terminating due to
the undecidability of the `Halting Problem
<https://en.wikipedia.org/wiki/Halting_problem>`_. It is possible, however,
to identify some programs which are definitely terminating. Idris does this
using "size change termination" which looks for recursive paths from a
function back to itself. On such a path, there must be at least one
argument which converges to a base case.
- Mutually recursive functions are supported
- However, all functions on the path must be fully applied. In particular,
higher order applications are not supported
- Idris identifies arguments which converge to a base case by looking for
recursive calls to syntactically smaller arguments of inputs. e.g.
``k`` is syntactically smaller than ``S (S k)`` because ``k`` is a
subterm of ``S (S k)``, but ``(k, k)`` is
not syntactically smaller than ``(S k, S k)``.
If you have a function which you believe to be terminating, but Idris does
not, you can either restructure the program, or use the ``assert_total``
function.
Does Idris have universe polymorphism? What is the type of ``Type``?
====================================================================
Idris 2 currently implements ``Type : Type``. Don't worry, this will not be the
case forever! For Idris 1, the FAQ answered this question as follows:
Rather than universe polymorphism, Idris has a cumulative hierarchy of
universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
Cumulativity means that if ``x : Type n`` and ``n <= m``, then
``x : Type m``. Universe levels are always inferred by Idris, and
cannot be specified explicitly. The REPL command ``:type Type 1`` will
result in an error, as will attempting to specify the universe level
of any type.
What does the name “Idris” mean?
================================
British people of a certain age may be familiar with this
`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
that doesn’t help, maybe you can invent a suitable acronym :-) .
Where can I find the community standards for the Idris community?
==================================================================
The Idris Community Standards are stated `here
<https://www.idris-lang.org/documentation/community-standards/>`_ .
The `Idris 1 FAQ <https://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
mostly still relevant.

3
docs/source/index.rst
View File

@ -19,13 +19,14 @@ Documentation for the Idris 2 Language
:maxdepth: 1
tutorial/index
faq/faq
backends/index
updates/updates
typedd/typedd
reference/packages
libraries/index
app/index
ffi/index
proofs/index
faq/faq
implementation/index
reference/index

13
docs/source/libraries/index.rst Normal file
View File

@ -0,0 +1,13 @@
Where To Find Libraries
=======================
You can find a canonical source of Idris libraries on the wiki on github:
https://github.com/idris-lang/Idris2/wiki/Libraries
Please feel free to contribute your own libraries there! Eventually, we aim to
have a package manager for managing libraries and dependencies. We do not yet
have an official one, but there are (at least) two in development:
* Inigo: https://github.com/idris-community/inigo
* sae: https://github.com/DoctorRyner/sae