• Mar 8, 2017


    New in 0.99.1:
    Language updates
    * Language pragmas 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`
    * 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!
    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`
    + 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.
    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.
  • Nov 28, 2016


    * `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
    * 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.
    * Idris' documentation system now displays the documentation for auto
      implicits in the output of `:doc`. This is tested for in `docs005`.
    * 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`. This
      is tested for in `docs006`.
    * 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 continous integration with Travis and Appveyor.
    * The :e command can now handle an $EDITOR with arguments in it, like "emacs -nw"
  • Sep 18, 2016


    Patch release (for Chapter 15 of TypeDD book)
  • Aug 3, 2016


    Patch release
    (Fixes for draft of Chapter 13 of TypeDD book)
  • Jul 26, 2016


    Patch release 0.12.1
    Fixes build for GHC 8 and adds record update syntax
  • Jun 21, 2016


    * `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 a
      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.
    * `Control.WellFounded` module removed, and added to the Prelude as
    * 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
    * 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.
    * 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"``.
    * The implicit coercion from String to TTName was removed.
    * Decidable equality for TTName is available.
  • May 18, 2016


    Patch release 0.11.2
  • May 2, 2016


    Patch release for Chapter 10 of TypeDD
  • Mar 25, 2016


    New in 0.11:
    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.
    * 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)
    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.
    Minor language changes
    * 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)
    * `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.
    * 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)
    * Idris will give a warning if an implicit is bound automatically, but would
      otherwise be a valid expressio if the name was used as a global
    External Dependencies
    * Curses has been removed as an external dependancy.
  • Mar 19, 2016


    Patch release 0.10.3