Idris 0.12 Released

A new version of Idris, 0.12, 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.11 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.

(Note: If you are installing from source, Idris 0.12 does not currently build with GHC 8.0.1 due to dependency issues. There’ll be a patch release once this issue is resolved.)

Language updates

  • rewrite can now be used to rewrite equalities on functions over dependent types
  • rewrite can now be given an optional rewriting lemma, with the syntax rewrite [rule] using [rewrite_lemma] in [scope].
  • Reorganised elaboration of implementation, so that interfaces with dependencies between methods now work more smoothly
  • Allow naming of parent implementations when defining an implementation. For example:
[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

-- use PlusNatSemi as the parent implementation
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

-- use MultNatSemi as the parent implementation
[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1
  • Interface definitions can now include data declarations (but not data definitions). Any implementation of the interface must define the method using a data type. The effect is to cause Idris to treat the method as a data type (for unification and interface resolution purposes).
  • Experimentally, allow named implementations to be available by default in a block of declarations with using notation. For example:
using implementation PlusNatMonoid
  test : Nat -> Nat
  test x = x <+> x <+> neutral
  • Constraint arguments can now appear anywhere in function types, not just at the top level or after an implicit argument binding.
  • Experimental extended with syntax, which allows calling functions defined in a with block directly. For example:
data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : SnocList xs -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs

my_reverse : List a -> List a
my_reverse xs with (snocList xs)
  my_reverse [] | Empty = []
  my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p

The | p on the right hand side means that the with block function will be called directly, so the recursive structure of SnocList can direct the recursion structure of my_reverse.
* Added %fragile directive, which gives a warning and a message when a fragile name is referenced. For use in detailing fragile APIs.
* The totality checker now looks under case blocks, rather than treating them as mutually defined functions with their top level function, meaning that it can spot more total functions.
* The totality checker now looks under if...then...else blocks when checking for productivity.
* The %assert_total directive is now deprecated. Instead, you can use one of the functions assert_total, assert_smaller or assert_unreachable to describe more precisely where a totality assertion is needed.

Library updates

  • Control.WellFounded module removed, and added to the Prelude as Prelude.WellFounded.
  • Added Data.List.Views with views on List and their covering functions.
  • Added Data.Nat.Views with views on Nat and their covering functions.
  • Added Data.Primitives.Views with views on various primitive types and their covering functions.
  • Added System.Concurrency.Sessions for simple management of conversations between processes

iPKG Updates

  • Taking cues from cabal, the iPKG format has been extended to include more package metadata information. The following fields have been added:
    • brief: Brief description of the package.
    • version: Version string to associate with the package.
    • readme: Location of the README file.
    • license: Description of the licensing information.
    • author: Author information.
    • maintainer: Maintainer information.
    • homepage: Website associated with the package.
    • sourcepage: Location of the DVCS where the source can be found.

Miscellaneous updates

  • The Idris man page is now installed as part of the cabal/stack build process.
  • Improved startup performance by reducing the processing of an already imported module that has changed accessibility.
  • A limited set of command line options can be used to override package declared options. Overridable options are currently, logging level and categories, default totality check, warn reach, IBC output folder, and idris path. Note overriding IBC output folder, only affects the installation of Idris packages.
  • Remove deprecated options --ideslave and --ideslave-socket. These options were replaced with --ide-mode and --ide-mode-socket in 0.9.17
  • The code generator output type MavenProject was specific to the Java codegen and has now been deprecated, together with the corresponding --mvn option.
  • Definitional equality on Double is now bit-pattern identity rather than IEEE’s comparison operator. This prevents a bug where programs could distinguish between -0.0 and 0.0, but the type theory could not, leading to a contradiction. The new fine-grained equality prevents this.
  • Naming conventions for Idris packages in an iPKG file now follow the same rules for executables. Unquoted names must be valid namespaced Idris identifiers e.g. package my.first.package. Quoted package names allow for packages to be given valid file names, for example, package "my-first-package".

Reflection changes

  • The implicit coercion from String to TTName was removed.
  • Decidable equality for TTName is available.

Big Tech Day 9

On June 3rd, Edwin presented an introduction to Idris at Big Tech Day 9.

The talk’s abstract:

Idris is a general purpose functional programming language with full dependent types, building on state-of-the-art techniques in programming language research. Dependent types allow types to be predicated on any value – in this way, required properties of a program can be captured in the type system, and verified by a type checker. This includes functional properties (i.e. does the program give the correct answer) and extra-functional properties (i.e. does the program run within specified resource constraints). Idris aims to bring type-based program verification techniques to programming practitioners while supporting efficient systems programming via an optimising compiler and interaction with external libraries. In this talk, I’ll use a series of examples to show how dependent types can be used for verifying realistic and important properties of software, from simple properties such as array bounds verification, to more complex properties of communicating and distributed systems.

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.

Idris 0.10 Released

A new version of Idris, 0.10, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. There’s only a small number of changes from version 0.9.20, which 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 Updates

  • The class and instance keywords have been deprecated. The class keyword has been replaced by interface. Instances are now called implementations and are introduced by giving the interface name and parameters. For example:
    interface Eq a where
        (==) : a -> a -> Bool
        (/=) : a -> a -> Bool
    
        (==) x y = not (/=) x y
        (/=) x y = not (==) x y
    
    Eq Bool where
        True  == True  = True
        True  == False = False
        False == True  = False
        False == False = True
    
    Eq a => Eq (Maybe a) where
        Nothing  == Nothing  = True
        Nothing  == (Just _) = False
        (Just _) == Nothing  = False
        (Just a) == (Just b) = a == b
    

    This is as before, but without the instance keyword.

    The rationale for this change is that interfaces as implemented in Idris have several differences from Haskell type classes, even though they have a lot in common. They can be parameterised by things which are not types (including values and interfaces themselves). They are primarily for overloading interfaces, rather than classifying types, and hence there can be multiple implementations.

  • New Fractional interface, with functions (/) and recip.

REPL Updates

  • New command :watch which watches the currently loaded file, and reloads it if it has been changed.

Miscellaneous Updates

  • Idris’ logging infrastructure has been categorised. Command line and repl are available. For command line the option --logging-categories CATS is used to pass in the categories. Here CATS is a colon separated quoted string containing the categories to log. The REPL command is logcats CATS, where CATS is a whitespace separated list of categories. Default is for all categories to be logged.
  • New flag --listlogcats to list logging categories.

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.

Idris 0.9.20 released

A new version of Idris, 0.9.20, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates 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.

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.

Language updates

  • Improved unification by implementing a pattern unification rule
  • Changed scoping rules for unbound implicits: any name which would be a valid unbound implicit is now always an unbound implicit. This is much more resilient to changes in inputs, but does require that function names be explicitly qualified when in argument position.
  • Name binding in patterns follows the same rule as name binding for implicits in types: names which begin with lower case letters, not applied to any arguments, are treated as bound pattern variables.
  • The previous syntax for tactic proofs and the previous interactive prover are now deprecated in favour of reflected elaboration. They will be removed at some point in the future.
  • The syntax `{{n}} quotes n without resolving it, allowing short syntax for defining new names. `{n} still quotes n to an existing name in scope.
  • A new primitive operator prim__strSubstr for more efficient extraction of substrings. External code generators should implement this.
  • Added %deprecate directive, which gives a warning and a message when a deprecated name is referenced.

Library updates

  • The Neg class now represents numeric types which can be negative. As such, the (-) operator and abs have been moved there from Num.
  • A special version of (-) on Nat requires that the second argument is smaller than or equal to the first. minus retains the old behaviour, returning Z if there is an underflow.
  • The (+), (-), and (*) operations on Fin have been removed.
  • File IO operations (for example openFile/fread/fwrite) now return Either FileError ty where the return type was previously ty to indicate that they may fail.
  • New Logging Effects have been added to facilitate logging of effectful programmes.
  • Elaborator reflection is now a part of the prelude. It is no longer necessary to import Language.Reflection.Elab.
  • The PERF effect allows for simple performance metrics to be collected from Effectful programs.
  • Some constructors that never actually occurred have been removed from the TT and Raw reflection datatypes in Language.Reflection.

Tool updates

  • Records are now shown as records in :doc, rather than as the underlying datatype
  • iPKG files have a new option pkgs which takes a comma-separated list of package names that the idris project depends on. This reduces bloat in the opts option with multiple package declarations.
  • iPKG files now allow executable = "your filename here" in addition to the existing executable = yourFilenameHere style. While the unquoted version is limited to filenames that look like namespaced Idris identifiers (your.filename.here), the quoted version accepts any valid filename.
  • Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now adds missing clauses if there is already a definition.

Miscellaneous updates

  • Disable the deprecation warnings for %elim and old-style tactic scripts with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings flags.

Idris 0.9.19 released

A new version of Idris, 0.9.19, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates 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.

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.

Language changes

  • More flexible case construct, allowing each branch to target different types, provided that the case analysis does not affect the form of any variable used in the right hand side of the case.
  • decl syntax rules to allow syntax extensions at the declaration level
  • As usual, lots of improvements and fixes in elaboration

Library changes

  • The Show class has been moved into Prelude.Show and augmented with the method showPrec, which allows correct parenthesisation of showed terms. This comes with the type Prec of precedences and a few helper functions.
  • Use predicates instead of boolean equality proofs as preconditions on List functions
  • Moved System.Interactive, along with getArgs to the Prelude, in Prelude.Interactive.

Tool changes

  • New REPL command :printerdepth that sets the pretty-printer to only descend to some particular depth when printing. The default is set to a high number to make it less dangerous to experiment with infinite structures. Infinite depth can be set by calling :printerdepth with no argument.
  • Compiler output shows applications of >>= in do-notation
  • fromInteger i where i is an integer constant is now shown just as i in compiler output
  • An interactive shell, similar to the prover, for running reflected elaborator actions. Access it with :elab from the REPL.
  • Major improvements to reflected elaboration scripts, including the ability to run them in a declaration context and many bug fixes.
  • New command-line option --highlight that causes Idris to save highlighting information when successfully type checking. The information is in the same format sent by the IDE mode, and is saved in a file with the extension .idh.
  • Highlighting information is saved by the parser as well, allowing it to highlight keywords like case, of, let, and do
  • Some improvements in interactive editing, particularly in lifting out definitions and proof search. Proof search is now aware of type classes.
  • Experimental Windows support for console colours.

Other changes

Idris 0.9.18 released

A new version of Idris, 0.9.18, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. Updates 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.

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.

Language changes

  • There is a new syntax for records, corresponding to type class syntax (which is also a record-like structure). See dependent records in the documentation
  • Records can now be coinductive, using the corecord keyword
  • Type class constructors can be given user accessible names (corresponding to the new record syntax)
  • if...then...else is now built in syntax rather than a syntax macro, desugaring to ifThenElse. This is for cleaner overloading and better error messages in domain specific languages.
  • Pattern matching lambdas and case expressions can now be labelled impossible, in
    the same way as top level patterns
  • Added a %hint function annotation, which allows functions to be used in proof search for auto arguments. Only functions which return instances of a data or record type are allowed as hints
  • Strings are now UTF8 encoded, and Idris source is assumed to be UTF8 encoded
  • Some reorganisation of primitives:
    • Buffer and BitVector removed (due to insufficient testing and lack of a maintainer)
    • Float renamed to Double
    • Externally defined primitives now supported with %extern directive
    • Ptr and ManagedPtr removed and replaced with external primitives
  • New quotation syntax `{n} for a quotation of the reflected representation of the name n. If n is lexically bound, then the resulting quotation will be for it, whereas if it is not, then it will succeed with a quotation of the unique global name that matches
  • As usual, lots of improvements and fixes in elaboration, especially with type class resolution
    and name disambiguation

Library changes

  • The default Semigroup and Monoid instances for Maybe are now prioritised choice, keeping the first success as Alternative does. The version that collects successes is now a named instance
  • The return types of Vect.findIndex, Vect.elemIndex and Vect.elemIndexBy were changed from Maybe Nat to Maybe (Fin n)

Tool changes

  • :exec REPL command now takes an optional expression to compile and run/show
  • A new :browse command shows the contents of a namespace
  • Agda-style semantic highlighting is supported over the IDE protocol

Idris 0.9.17 released

A new version of Idris, 0.9.17, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org.

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.

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.

The main new features and updates are:

  • Library operators have been renamed for consistency with corresponding operators in Haskell. In particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is now an alias for Functor.map. Correspondingly, ($>) and (<$) have been renamed to (<*) and (*>). The cascading effects of this rename are that Algebra.(<*>) has been renamed to Algebra.(<.>) and Matrix.(<.>) is now Matrix.(<:>).
  • Types errors have been improved, now giving the provenance of incorrect types
  • Documentation has been updated and moved to docs.idris-lang.org, hosted by Read the Docs.
  • Web documentation is now available for packages, from the Documentation page.
  • A new package contrib has been added to the libraries. This is for things which are less mature or less used than the contents of base.contrib is not available by default, so you may need to add -p contrib to your .ipkg file or Idris command line.
  • Instances and type providers can now be given documentation strings.
  • Lots of issues relating to type class resolution have been resolved. In particular:
    • Arguments are now checked for injectivity, since this is assumed throughout unification
    • Multi-parameter type classes can now be given determining parameters, which are the parameters used to resolve class instances. Only determining parameters are assumed and checked to be injective.
  • Binding forms in dsl notation are now given an extra argument: a reflected representation of the name that the user chose. Specifically, the rewritten lambda, pi, and let binders will now get an extra argument of type TTName. This allows more understandable dynamic errors in DSL code and more readable code generation results.
  • The Foreign Function Interface has been updated to support multiple back end descriptions.
  • A new FFI_Export type has been added, supporting export of functions to be called by foreign code. Details of the FFI and its interaction with back ends are given in this draft paper.

Idris 0.9.16 released

A new version of Idris, 0.9.16, has been released. You can find this on hackage, or from the download page.

The tutorial has also been updated.

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.

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.

The main new features and updates are:

  • Inductive-inductive definitions are now supported (i.e. simultaneously defined types where one is indexed by the other)
  • Implicits and type class constraints can now appear in scopes other than the top level
  • Importing a module no longer means it is automatically reexported. A new public modifier has been added to import statements, which will reexport the names exported from that module
  • Implemented @patterns. A pattern of the form x@p on the left hand side matches p, with x in scope on the right hand side with value p
  • Vect, Fin and So moved out of prelude into base, in modules Data.Vect, Data.Fin and Data.So respectively
  • A new tactic sourceLocation that fills the current hole with the current source code span, if this information is available. If not, it raises an error
  • :search and :apropos commands can now be given optional package lists to search
  • Better Unicode support for the JavaScript/Node codegen
  • Modules can now have API documentation strings

Additionally, several long-standing issues have been resolved, particularly with pattern matching and coverage checking.

Idris 0.9.15.1 released

A new version of Idris, 0.9.15.1, has been released. You can find this on hackage, or from the download page.

The tutorial has also been updated.

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.

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.

The main new features and updates are:

  • Naming of data and type constructors is made consistent across the standard library.
    • Note: This change will break existing code!
    • Data and Type Constructors now consistently begin with a capital letter, which means in particular we have Refl, FZ and FS for refl, fZ and fS.
    • The empty type is now called Void, and its eliminator void.
  • EXPERIMENTAL support for Uniqueness Types
  • EXPERIMENTAL support for Partial Evaluation, as described in Scrapping your Inefficient Engine.
  • The Java and LLVM backends have been factored out into separate projects, idris-java and idris-llvm.

There are several minor updates and improvements:

  • More efficient representation of the proof state, leading to faster elaboration of large expressions.
  • Two new tactics: skip and fail. skip does nothing, and fail takes a string as an argument and produces it as an error, with corresponding reflected tactics.
  • Improved display in the interactive prover.
  • Unary negation now desugars to `negate`, which is a method of the `Neg` type class. This allows instances of `Num` that can’t be negative, like `Nat`, and it makes correct IEEE Float operations easier to encode. Additionally, unary negation is now available to DSL authors.
  • New REPL command `:printdef` displays the internal definition of a name.
  • New REPL command `:pprint` pretty-prints a definition or term with LaTeX or HTML highlighting.
  • Terms in code blocks in documentation strings are now parsed and type checked. If this succeeds, they are rendered in full colour in documentation lookups, and with semantic highlighting for IDEs.
  • Fenced code blocks in docs defined with the “example” attribute are rendered as code examples.
  • Fenced code blocks declared to be Idris code that fail to parse or type check now provide error messages to IDE clients.