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.
@-patterns such as
xis now in scope on the right-hand side of any definitions in
whereclauses, provided the left-hand side of the definition does not shadow it.
LinearTypeslanguage 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.
- 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 uninhabltbto 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.
- 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
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
[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
doblocks in addition to
do … let Just x = expr | Nothing => empty …
This means that a
|) cannot be used in that position anymore.
Text.Literate, a module for working with literate source files.
Data.IORef, for working with mutable references in
constructtactics to Pruviloj.
Prelude, which proves that a
Natis a successor.
Data.IOArray, containing primitives for mutable arrays.
Language.JSON, for total serialization/deserialization of JSON data.
- Reworked operator fixity for many operators.
||to be right-associative. Increased precedence of
&&to be higher than that of
- Removed associativity from Boolean comparison operators
>=. Increased precedence of
==to match the others.
- Swapped precedence of
<*>(and its related operators,
<|>has a lower precedence.
- Lowered the precedence of
>>=to be below that of
- Added some useful string manipulation functions to
Control.Delayed, a module for conditionally making a type
Data.Fuel, which implements the
Fueldata type and the partial
Data.Bool.Extra, a module with properties of boolean operations.
- Moved core of
Text.Lexer.Core. Added several new combinators and lexers to
- Moved core of
Text.Parser.Core. Added several new combinators to
Text.Parser. Made the following changes.
- Flipped argument order of
optionand flip argument order.
- Generalised many combinators to use an unknown
commitflag where possible.
- Flipped argument order of
Prelude.Doubles.atan2is now implemented as a primitive instead of being coded in Idris.
contribfor simple unit testing.
- Removed several deprecated items from the libraries shipped with Idris.
Neginterface into its own
abs = id.
Control.ST.File, an ST based implementation of the same behaviour implemented by
Effect.Filein the effects package.
- 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
- 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_LDFLAGSare now set with the correct C flags.