What Contributions are Needed - idris-lang/Idris2 GitHub Wiki

Contributions are welcome! If you're interested in helping, please get in touch! A good place to ask about possible contributions in the first instance is via the mailing list or the Idris Discord community.

What contributions are needed?

The contributing guidelines outline what contributions are needed, and which are likely to be accepted. Those guidelines focus on the language core. Some things which would be useful beyond the language core are:

  • Improvements to documentation generation
  • REPL improvements including :search
  • A nicer REPL (implemented via the Idris 2 API or IDE mode, rather than as part of Idris 2 itself) including:
    • readline and tab completion
    • :apropos
    • code colouring
  • 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. These should be implemented via the Idris 2 API, rather than as part of the main Idris 2 repo.
  • More libraries, which can be added to the list of Third-party Libraries

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!

  • Infer type parameters from implied interface types:

    Instead of needing to write (f : Type -> Type) we would ideally just write f below:

    interface Functor f => Applicative (f : Type -> Type) where
    pure  : a -> f a
    (<*>) : f (a -> b) -> f a -> f b

    f has already had its kind (or should I just say Type in Idris) defined in:

    interface Functor (f : Type -> Type) where
    map : (m : a -> b) -> f a -> f b

    so it seems a bit redundant to have to specify it again in the way shown above.

  • Suggest names in scope to cope with user-written typos. At the moment typing Lt instead of LT yields and "out of scope error". It would be nice to be presented with a list of identifiers in scope with a small edit distance to what we wrote.

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

  • 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.

  • 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.

  • Get rid of need to use msys2 on Windows, instead the dependencies should all be the Windows versions of the dependencies (Chez, make, etc).

  • 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] [...] 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

  • Networking support

  • Proper ECMAScript-module and TypeScript interfacing

  • Allow multiple source locations per fc, since desugaring sometimes combines different parts of the source into one entity.

    For example, we can now define multiple definitions in one declarations:

    def1, def2, def3 : Type

    and that desugars into 3 declarations:

    def1 : Type
def2 : Type
def3 : Type

    Maybe we should have the fc for each of them be [{start: (1,i), end: (1, i+4)}, {start: (1, 18), end: (1, 22)}]

    Another such example are lists: [ x1 , x2, x3 ] desugars into x1 :: x2 :: x3 :: Nil so the Nil should get the FC of the opening and closing brackets.

  • Add multiplicity polymorphism, without resorting to subtyping

  • Prove the compiler correct, assuming that the theory behind Idris is consistent. Obviously a longshot.