Idris 1.2.0 released

A new version of Idris, 1.2.0, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. This version includes several bug fixes and performance improvements, and other changes since version 1.1.1 as 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

  • In @-patterns such as x@p, x is now in scope on the right-hand side of any definitions in where clauses, provided the left-hand side of the definition does not shadow it.
  • The LinearTypes language extension has been revised. It implements the rules from Bob Atkey’s draft “The Syntax and Semantics of Quantitative Type Theory” and now works with holes and case expressions.
  • Backticked operators can appear in sections, e.g. (`LTE` 42) or (1 `plus`).
  • Backticked operators can have their precendence and associativity set like other operators, e.g. infixr 8 `cons`. Backticked operators with undeclared fixity are treated as non-associative with precedence lower than all declared operators.
  • Allow non-injective implementations if explicitly named, e.g.,

    LTB : Nat -> Type
    LTB b = DPair Nat (\ n  => LT n b)
    
    implementation [uninhabltb] Uninhabited (LTB Z) where
      uninhabited (MkDPair n prf) = absurd prf
    

    It is possible to use using implementation uninhabltb to add the implementation to the automated resolution, but if it fails to find the instance due to non-injectivity, one must pass it explicitly to target function, i.e. absurd @{uninhabltb}.

  • Verbatim strings now support trailing quote characters. All quote characters until the final three are considered part of the string. Now a string such as """"hello"""" will parse, and is equivalent to "\"hello\"".
  • C FFI now supports pasting in any expression by prefixing it with ‘#’, e.g.

    intMax : IO Int
    intMax = foreign FFI_C "#INT_MAX" (IO Int) 
    
  • The deprecated keywords %assert_total, abstract, and [static] have been removed as well as the use of “public” instead of “public export” to expose a symbol.
  • The syntax for pattern-match alternatives now works for let statements in do blocks in addition to let expressions and <- statements, e.g.

    do …
       let Just x = expr | Nothing => empty
       …
    

    This means that a with-application (using |) cannot be used in that position anymore.

Library Updates

  • Removed oldeffects library from libs folder, use effects or Control.ST instead.
  • Added Text.Literate, a module for working with literate source files.
  • Added Data.IORef, for working with mutable references in IO and JS_IO.
  • Added discriminate and construct tactics to Pruviloj.
  • Added IsSucc type to Prelude, which proves that a Nat is a successor.
  • Added Data.IOArray, containing primitives for mutable arrays.
  • Added Language.JSON, for total serialization/deserialization of JSON data.
  • Reworked operator fixity for many operators.
    • Changed && and || to be right-associative. Increased precedence of && to be higher than that of ||.
    • Removed associativity from Boolean comparison operators ==, /=, <, <=, >, and >=. Increased precedence of /= and == to match the others.
    • Made <|>, <$>, and . right-associative.
    • Swapped precedence of <|> and <*> (and its related operators, <* and *>). Now <|> has a lower precedence.
    • Lowered the precedence of >>= to be below that of <|>.
  • Added some useful string manipulation functions to Data.String.Extra.
  • Added Control.Delayed, a module for conditionally making a type Inf or Lazy.
  • Added Data.Fuel, which implements the Fuel data type and the partial forever function.
  • Added Data.Bool.Extra, a module with properties of boolean operations.
  • Moved core of Text.Lexer to Text.Lexer.Core. Added several new combinators and lexers to Text.Lexer.
  • Moved core of Text.Parser to Text.Parser.Core. Added several new combinators to Text.Parser. Made the following changes.
    • Flipped argument order of parse.
    • Renamed optional to option and flip argument order.
    • Renamed maybe to optional.
    • Generalised many combinators to use an unknown commit flag where possible.
  • Prelude.Doubles.atan2 is now implemented as a primitive instead of being coded in Idris.
  • Added Test.Unit to contrib for simple unit testing.
  • Removed several deprecated items from the libraries shipped with Idris.
  • Moved abs from the Neg interface into its own Abs interface. Nat implements Abs with abs = id.
  • Added Control.ST.File, an ST based implementation of the same behaviour implemented by Effect.File in the effects package.

Tool Updates

  • Private functions are no longer visible in the REPL except for modules that are explicitly loaded.
  • The –interface option now creates CommonJS modules on the node backend.
  • The C backend now pass arguments to the C compiler in the same order as they were given in the source files.
  • Backslash, braces and percent symbols are now correctly pretty printed in LaTeX.
  • Errors and warnings now consistently have the following format:

    reg068.idr:1:6-8:
    |
    1 | data nat : Type where --error
    |      ~~~
    Main.nat has a name which may be implicitly bound.
    This is likely to lead to problems!
    

    The code is highlighted when highlighting information is available. How much highlighting information is available depends on where the error occurred.

  • The parser provider has been switched from Trifecta to Megaparsec. This could possibly cause some subtle deviations in parsing from previous versions of Idris.
  • Many more errors now report beginning and ending position (which may be on different lines), instead of just a single point. The format is
    Foo.idr:9:7-15: if ending column is on the same line or
    Foo.idr:9:7-10:15: if the ending column is on a different line.
  • Error messages were changed so that the last column is inclusive, e.g.
    Foo.idr:9:7-15: includes column 15. Previously the error would have read Foo.idr:9:7-16:.

Packaging Updates

  • Package names now only accept a restrictive charset of letters, numbers and the -_ characters. Package names are also case insensitive.
  • When building makefiles for the FFI, the environment variables IDRIS_INCLUDES and IDRIS_LDFLAGS are now set with the correct C flags.

Idris 1.1.1 released

A new version of Idris, 1.1.1, has been released. You can find this on hackage, or from the download page. Documentation is available from docs.idris-lang.org. This includes the following updates, fixing some issues with version 1.1.0:

  • Fixed installation issue
  • Fixed a potential segfault when concatenating strings
  • Erasure analysis is now faster thanks to a bit smarter constraint solving.

Idris 1.1.0 released

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

Library Updates

  • Added Text.Lexer and Text.Parser to contrib. These are small libraries for implementing total lexical analysers and parsers.
  • Added Text.PrettyPrint.WL an implementation of the Wadler-Leijen Pretty-Print algorithm.
  • New instances:
    • Added Catchable for ReaderT, WriterT, and RWST.
    • Added MonadTrans for RWST.
  • Added utility functions to Data.SortedMap and Data.SortedSet (contrib), most notably merge, merging two maps by their Semigroup op (<+>)
  • Prelude.WellFounded now contains an interface Sized a that defines a size mapping from a to Nat. For example, there is an implementation for lists, where size = length.

    The function sizeAccessible then proves well-foundedness of the relation Smaller x y = LT (size x) (size y), which allows us to use strong induction conveniently with any type that implements Sized.

    In practice, this allows us to write functions that recurse not only on direct subterms of their arguments but on any value with a (strictly) smaller size.

    A good example of this idiom at work is Data.List.Views.splitRec from base.

  • Added utility lemma decEqSelfIsYes : decEq x x = Yes Refl to Decidable.Equality. This is primarily useful for proving properties of functions defined with the help of decEq.

Tool Updates

  • New JavaScript code generator that uses an higher level intermediate representation.
  • Various optimizations of the new JavaScript code generator.
  • Names are now annotated with their representations over the IDE protocol, which allows IDEs to provide commands that work on special names that don’t have syntax, such as case block names.

Idris 1.0 Released

Idris version 1.0 has been released. You can find it on hackage or from the download page. Documentation is available from docs.idris-lang.org.

Thanks to everyone who has contributed, whether by providing code, documentation, testing, issue reports, or encouragement. You can find the names of the contributors in the source repository.

What do we mean by “1.0”?

Idris version 1.0 corresponds to the language as described in Type-Driven Development with Idris, published last week by Manning.

As described here, there is still much to do. Idris is primarily a research tool, arising from research into software development with dependent types which aims to make theorem proving and software verification accessible and practical for software developers in general. In calling this “1.0”, we mean no more than that the core language and base libraries are stable, and that you can expect any code that compiles with version 1.0 to compile with any version 1.x.

Since Idris has less than one person working on it full time, we don’t promise “production readiness”, in that there is still a lot to do to make the compiler and run time efficient, and there may be libraries you need which are not available. And, there will certainly be bugs! Please let us know via the issue tracker if you encounter any problems.

Contributions

We will always welcome contributions, however small. Some specific contributions needed are described on the wiki.

Have fun!

Community

You can get in touch in several ways:

Mailing list
Long-form discussion happens on the mailing list.
IRC
There is also an irc channel #idris on freenode. Point your irc client to chat.freenode.net then /join #idris. Alternatively, there is a web interface.
Twitter
@idrislang on Twitter
GitHub
The Idris source is available from our repository. Tools and code by the wider Idris community are available in a GitHub organisation.

All participants in these forums are requested to abide by the community standards.

Idris 0.99.1 Released

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

This release mostly contains bug fixes and minor improvements, aiming towards releasing version 1.0 around the same time as the publication of Type Driven Development with Idris which will be very soon. There is also a new experimental feature, working towards support for linear types, but don’t expect this to work properly yet :). The changes since version 0.99 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

  • Language pragmas are now required for the less stable existing features, in addition to the existing TypeProviders and ErrorReflection:
    • ElabReflection, which must be enabled to use %runElab
    • UniquenessTypes, which must be enabled to use UniqueType
    • DSLNotation, which must be enabled to define a dsl block
    • FirstClassReflection, which must be enabled to define a %reflection function
  • New language extension LinearTypes:
    • This allows adding a /multiplicity/ to a binder which says how often it is allowed to be used; either 0 or 1 (if unstated, multiplicity is “many”)
    • The typing rules follow Conor McBride’s paper “I Got Plenty o’ Nuttin'”
    • This is highly experimental, unfinished, not at all polished. and there are still lots of details to sort out. Some features don’t quite work properly yet. But it is there to play with for the brave!

Library Updates

  • Terminating programs has been improved with more appropriate functions (exitWith, exitFailure, and exitSuccess) and a data structure (ExitCode) to capture a program’s return code.
  • Casting a String to an Int, Integer or a Double now ignores leading and trailing whitespace. Previously only leading whitespace was ignored.
  • RTS functions openFile, do_popen, and ARGV are now properly encoded using UTF-8 on Windows.
  • New module Control.ST in contrib for implementing and combining state transition systems

Tool Updates

  • Idris’ output has been updated to more accurately reflect its progress through the compiler i.e. Type Checking; Totality Checking; IBC Generation; Compiling; and Code Generation. To control the loudness of the reporting three verbosity levels are introduced: --V0, --V1, and --V2. The old aliases of -V and --verbose persist.
  • New REPL command :! that runs an external shell command.
  • The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS) on Windows, which previously did not occur due to a bug.
  • Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many Unicode-rendering issues on Windows (e.g., error messages stating commitBuffer: invalid argument (invalid character)).
  • Idris now has a --warnipkg flag to enable auditing of Idris packages during build time. Currently auditing check’s the list of modules specified in the iPKG file with those presented in the package directory.

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