Idris 0.11 Released

A new version of Idris, 0.11, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. The changes since version 0.10 are detailed below.

Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.

Language changes

  • More flexible holes: Holes can now depend on other holes in a term (such as implicit arguments which may be inferred from the definition of the hole).
  • Programs with holes can now be compiled. Attempting to evaluate an expression with a hole results in a run time error.
  • Dependent pairs now can be specified using a telescope-style syntax, without requirement of nesting, e.g. it is possible to now write the following:
        (a : Type ** n : Nat ** Vect n a)
    

    Instead of:

        (a : Type ** (n : Nat ** Vect n a))
    
  • Idris will give a warning if an implicit is bound automatically, but would otherwise be a valid expression if the name was used as a global
  • The [static] annotation is changed to %static to be consistent with the other annotations
  • Added %auto_implicits directive. The default is %auto_implicits on. Placing %auto_implicits off in a source file means that after that point, any implicit arguments must be bound, e.g.:
        append : {n,m,a:_} -> Vect n a -> Vect m a -> Vect (n + m) a
    

    Only names which are used explicitly in the type need to be bound, e.g.:

        Here  : {x, xs : _} -> Elem x (x :: xs)
    

    In Here, there is no need to bind any of the variables in the type of xs (it could be e.g. List a or Vect n a; a and n will still be implicitly bound).

    You can still implicitly bind with using:

        using (xs : Vect _ _)
          data Elem  : {a, n : _} -> a -> Vect n a -> Type where
               Here  : {x : _} -> Elem x (x :: xs)
               There : {x, y : _} -> Elem x xs -> Elem x (y :: xs)
    

    However, note that only names which appear in both the using block and the type being defined will be implicitly bound. The following will therefore fail because n isn’t implicitly bound:

        using (xs : Vect n a)
          bad : Elem x xs -> Elem x (y :: xs)
    

Library changes

  • Effects can now be given in any order in effect lists (there is no need for the ordering to be preserved in sub lists of effects)
  • Sigma has been renamed to DPair
  • Accessor functions for dependent pairs have been renamed to bring them into line with standard accessor functions for pairs. The function getWitness is now fst, and getProof is snd.
  • File Modes expanded: Append, ReadWriteTruncate, and ReadAppend added, Write is deprecated and renamed to WriteTruncate
  • C11 Extended Mode variations added to File Modes.

Updated export rules

  • The export rules are:
    • private means that the definition is not exported at all
    • export means that the top level type is exported, but not the definition. In the case of data, this means the type constructor is exported but not the data constructors
    • public export means that the entire definition is exported
  • By default, names are private. This can be altered with an %access directive as before
  • Exported types can only refer to other exported names
  • Publicly exported definitions can only refer to publicly exported names

Improved C FFI

  • Idris functions can now be passed as callbacks to C functions or wrapped in a C function pointer.
  • C function pointers can be called.
  • Idris can access pointers to C globals.

Elaborator reflection updates

  • Datatypes can now be defined from elaborator reflection:
    • declareDatatype adds the type constructor declaration to the context
    • defineDatatype adds the constructors to the datatype
    • To declare an inductive-recursive family, declare the types of the function and the type constructor before defining the pattern-match cases and constructors.

External Dependencies

  • Curses has been removed as an external dependancy.

Future Release Plans

Version 1.0 of the Idris language is intended to coincide with the completion of the book Type Driven Development with Idris. The version of Idris on Hackage will be kept up to date with the latest draft of the book.

Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.

Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.