Contributions wanted

Contributing to Idris

Contributions are welcome! This page lists some of the most important missing features, and is a good place to add feature requests and proposals. If you're interested in helping with any of these, please get in touch! A good place to ask in the first instance is via the mailing list.

Most important missing features

The most important things needed at this stage, beyond work on the language core, are (in no particular order):

• CI integration.
• 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
• 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/
• Partial evaluation, especially for specialisation of interface implementations.
• 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. Or maybe GRIN
• JS and Node back ends would be nice.

Feature requests

If you have a feature request, or a proposal, please describe it here (or make a new page, if it's large). Since we don't have that many people working on Idris 2 at the moment (it's about half a full time person, plus various others in their spare time) there's no guarantee that anyone will be able to work on it, but perhaps someone will be inspired!

• Selective imports, i.e. ability to import only some things from a module by writing import Foo (foo, Foo(..), interface FooLike)

  • Specifically, we could replicate what Purescript does. Having hiding and as seems nifty too.

• Much more modularity, so a lot of features can be split off as separate modules in separate projects.

  • For instance, the backends and languages that work through the FFI could be done this way, and maybe even the Idris language itself, with it being easier to have other dependently typed languages that use TTImp and the backend system, making Idris more of an ecosystem than just a language.
  • Having the REPL also be separate would be useful as well.

• Making Idris completely self hosting.

• Getting rid of the C dependencies, and the requirement for a POSIX enviornment.

  • This would not only make working on Idris in Windows easier, it could make it much easier to implement say Idris in the browser, Idris on a phone operating system, or Idris .Net.

• Have %default total be the default behaviour, and allow for the main method to be total for ongoing programs as well, maybe by allowing for a main with a parameter that takes in something like Fuel.

  • [edwinb] Once I've done a bit more work on the coverage checker, I'm going to make %default covering the default behaviour. I'm not going to go as far as %default total, though, for the same reason I didn't in Idris 1: That is, while I think this is desirable (indeed, required) in a theorem prover, we're not quite ready for it yet in a programming language.

• Generalize auto implicits to use custom tactics, a-la this Agda proposal.

• A facility to generalize Nat(like) optimization to arbitrary user datatypes, e.g. Bi{p|n|z} to Integers, and BizMod2 to fixed-size machine words.

• Ability to/documentation on proving totality.

• Make local definitions from let appear in the context of a hole, for example in the following:

  Foo : Nat -> Nat
  Foo n = let k : Nat
              k = n + n in ?hole
    where
      succ : Nat -> Nat
      succ x = S x
  

  We will see this information displayed in a hole:

  Main> :t hole
     n : Nat
     k : Nat
  -------------------------------------
  hole : Nat
  

  Rationale: I think the current behaviour is because let binding (with type ascriptions) is synonymous with where clauses. However, in practice let definitions seem to be more like intermediate values we construct in order to define the result, whereas where clauses seem to be more like context-aware top-level functions.

  If we would still like to keep let and where identical, then we should consider making local definitions from both appear in holes.

  Extension: Since simply displaying every let-bound identifier variable might clutter the hole, IDEs should make it possible to hide the let-bound identifiers, e.g.:

  Main> :t hole
     n : Nat
     [+] ...   
  -------------------------------------
  hole : Nat
  

  and when the user clicks/expands [+]:

  Main> :t hole
     n : Nat
     [-] k : Nat   
  -------------------------------------
  hole : Nat
  

• Consider adjusting the QTT part of the core type theory to something that also tracks usage in types. This could possibly open up optimisations during typechecking, e.g. a half-formed idea of how this would go is as follows: if we know that a type variable is not used at all (neither in terms nor in types) we can stop tracking it completely. There's an outline of a type theory like this in this short abstract of Abel's.

• Rust backend that translates linearity on the Idris side to affinity/ownership/lifetimes on the Rust side.

• Function extensionality

  • This requires quite big changes to underlying type theory, making it into something like OTT.

• Permit using the default keyword as an identifier, e.g. for the function name in a Default interface like this one.

• Support for "Go to definition" in the IDE mode

• Mixfix operators

• Eff