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

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

There’s just a small number of changes since version 0.99.1, mostly bug fixes and small improvements in a final push towards version 1.0 (Real Soon Now :)). Changes since version 0.99.1 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.

Library Updates

  • Added Data.Buffer to base. This allows basic manipulation of mutable buffers of Bits8, including reading from and writing to files.

Tool Updates

  • Idris now checks the list of packages specified at the command line against those installed. If there is a mismatch Idris will complain.

Miscellaneous Updates

  • Documentation updates for the new Control.ST library
  • Various stability/efficiency fixes

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

A new version of Idris, 0.99, 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.12 are detailed below.

This is an important step towards releasing version 1.0, with the language more or less stable now. Between now and releasing 1.0, we’ll be focussing on fixing up the most important issues, and on efficiency and robustness.

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

  • record syntax now allows updating fields, including nested fields, by applying a function using the $= operator. For example:
  record Score where
         constructor MkScore
         correct : Nat
         attempted : Nat

  record GameState where
         constructor MkGameState
         score : Score
         difficulty : Nat

  correct : GameState -> GameState
  correct st = record { score->correct $= (+1),
                        score->attempted $= (+1) } st
  • Implicit parameter to interfaces are now allowed. For example:
interface Shows (ts : Vect k Type) where
    shows : HVect ts -> Vect k String

In this interface, k is an implicit parameter, but previously needed to be explicit

Library updates

  • The File Effect has been updated to take into account changes in Prelude.File and to provide a ‘better’ API.
  • natEnumFromThen and natEnumFromTo have been updated to correctly calculate reverse ranges. Range syntax [a,b..c] now can be used again to generate reverse ranges.
  • divBN and modBN now can only be used for unsigned numbers.
  • return, which has been an alias for pure for many releases, is now deprecated.
  • Replace instance with implementation:

    • InstanceN is deprecated, use ImplementationN instead.
    • InstanceCtorN is deprecated, use ImplementationCtorN instead.
    • addInstance is deprecated, use addImplementation instead.
    • %instance keyword is deprecated, use %implementation instead.
  • Idris packages are now installed within a sub-directory libs of Idris’ data directory, before they were installed in the directory’s root.

Tool updates

  • Idris’ documentation system now displays the documentation for auto implicits in the output of :doc.
  • New command line flag --info that displays information about the installation.
  • New command line flag --sourcepath <dir> that allows adding directories to the source search path.
  • Allow ‘installation’ of a package’s IdrisDoc documentation into a central location. The default location is the subdirectory docs of Idris’ data directory.
    • New flag --installdoc <ipkg> provided to install documentation
    • New flag --docdir provided to show default documentation installation location.
    • New environment variable IDRIS_DOC_PATH to allow specification of an alternative installation path for documentation.
  • Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.
  • Interface parameter constraints are now printed in the output of :doc.

Miscellaneous updates

  • New, faster, better, implementation of the coverage checker
  • The test suite now uses [tasty-golden (https://hackage.haskell.org/package/tasty-golden). New tests must be registered in test/TestData.hs, as explained in the relevant README.md.
  • Added OSX and Windows continuous integration with Travis and Appveyor.

UI Changes

  • The :e command can now handle an $EDITOR with arguments in it, like “emacs -nw”

Towards Version 1.0

Now that the language is getting stable, and that the Idris book, Type-driven Development with Idris is nearing publication, it’s getting close to time to release version 1.0.

We’ll shortly be releasing Idris version 0.99, which is essentially an alpha release of 1.0, and we’ll keep releasing updates until 1.0 is ready, probably around February 2017. There’s still plenty to do, which we’ll be working on over the next few weeks, mostly relating to stability and efficiency, fixing as many issues as we reasonably can, and committing to various minor decisions that we’ve been putting off.

What do we mean by “1.0”?

Mostly, what we mean by calling a release “1.0” is that there are large parts of the language and libraries that we now consider stable, and we promise not to change them without also changing the version number appropriately. In particular, if you have a program which compiles with Idris 1.0 and its Prelude and Base libraries, you should also expect it to compile with any version 1.x. (Assuming you aren’t relying on the behaviour of a bug, at least :))

Specifically, when we release version 1.0, the following will be stable:

  • All of the language, except those parts which require a %language pragma to use
  • Everything in prelude, except Language.Reflection
  • Everything in base, except modules in the Language.Reflection part of the hierarchy

In version 1.0, a %language pragma will be required to access: reflection mechanisms (that is, error reflection, elaboration reflection and reflection functions), uniqueness types and dsl notation.

The other packages distributed with Idris, contrib, effects, and pruviloj, may yet change. In particular, contrib remains a place for new modules to be tested, and effects is likely to be deprecated in favour of a new library at some point.

Furthermore, the IDE protocol will remain backwards compatible throughout 1.0.x releases.

Will version 1.0 be “Production Ready”?

Idris remains primarily a research tool, with the goals of exploring the possibilities of software development with dependent types, and particularly aiming to make theorem proving and verification techniques accessible to software developers in general. We’re not an Apple or a Google or [insert large software company here] so we can’t commit to supporting the language in the long term, or make any guarantees about the quality of the implementation. There’s certainly still plenty of things we’d like to do to make it better.

All that said, if you’re willing to get your hands dirty, or have any resources which you think can help us, please do get in touch!

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.