[Agda] ANNOUNCE: Agda 2.2.10

[Nils Anders Danielsson]

Hi,

Agda 2.2.10 has now been released. Important changes since 2.2.8:

Language
--------

* New flag: --without-K.

   This flag makes pattern matching more restricted. If the flag is
   activated, then Agda only accepts certain case-splits. If the type
   of the variable to be split is D pars ixs, where D is a data (or
   record) type, pars stands for the parameters, and ixs the indices,
   then the following requirements must be satisfied:

   * The indices ixs must be applications of constructors to distinct
     variables.

   * These variables must not be free in pars.

   The intended purpose of --without-K is to enable experiments with a
   propositional equality without the K rule. Let us define
   propositional equality as follows:

     data _≡_ {A : Set} : A → A → Set where
       refl : ∀ x → x ≡ x

   Then the obvious implementation of the J rule is accepted:

     J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
         (∀ x → P (refl x)) →
         ∀ {x y} (x≡y : x ≡ y) → P x≡y
     J P p (refl x) = p x

   The same applies to Christine Paulin-Mohring's version of the J rule:

     J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) →
          P (refl x) →
          ∀ {y} (x≡y : x ≡ y) → P x≡y
     J′ P p (refl x) = p

   On the other hand, the obvious implementation of the K rule is not
   accepted:

     K : {A : Set} (P : {x : A} → x ≡ x → Set) →
         (∀ x → P (refl x)) →
         ∀ {x} (x≡x : x ≡ x) → P x≡x
     K P p (refl x) = p x

   However, we have /not/ proved that activation of --without-K ensures
   that the K rule cannot be proved in some other way.

* Irrelevant declarations.

   Postulates and functions can be marked as irrelevant by prefixing
   the name with a dot when the name is declared. Example:

     postulate
       .irrelevant : {A : Set} → .A → A

   Irrelevant names may only be used in irrelevant positions or in
   definitions of things which have been declared irrelevant.

   The axiom irrelevant above can be used to define a projection from
   an irrelevant record field:

     data Subset (A : Set) (P : A → Set) : Set where
       _#_ : (a : A) → .(P a) → Subset A P

     elem : ∀ {A P} → Subset A P → A
     elem (a # p) = a

     .certificate : ∀ {A P} (x : Subset A P) → P (elem x)
     certificate (a # p) = irrelevant p

   The right-hand side of certificate is relevant, so we cannot define

     certificate (a # p) = p

   (because p is irrelevant). However, certificate is declared to be
   irrelevant, so it can use the axiom irrelevant. Furthermore the
   first argument of the axiom is irrelevant, which means that
   irrelevant p is well-formed.

   As shown above the axiom irrelevant justifies irrelevant
   projections. Previously no projections were generated for irrelevant
   record fields, such as the field certificate in the following
   record type:

     record Subset (A : Set) (P : A → Set) : Set where
       constructor _#_
       field
         elem         : A
         .certificate : P elem

   Now projections are generated automatically for irrelevant fields
   (unless the flag --no-irrelevant-projections is used). Note that
   irrelevant projections are highly experimental.

* Termination checker recognises projections.

   Projections now preserve sizes, both in patterns and expressions.
   Example:

     record Wrap (A : Set) : Set where
       constructor wrap
       field
         unwrap : A

     open Wrap public

     data WNat : Set where
       zero : WNat
       suc  : Wrap WNat → WNat

     id : WNat → WNat
     id zero    = zero
     id (suc w) = suc (wrap (id (unwrap w)))

   In the structural ordering unwrap w ≤ w. This means that

     unwrap w ≤ w < suc w,

   and hence the recursive call to id is accepted.

   Projections also preserve guardedness.

Tools
-----

* Hyperlinks for top-level module names now point to the start of the
   module rather than to the declaration of the module name. This
   applies both to the Emacs mode and to the output of agda --html.

* Most occurrences of record field names are now highlighted as
   "fields". Previously many occurrences were highlighted as
   "functions".

* Emacs mode: It is no longer possible to change the behaviour of the
   TAB key by customising agda2-indentation.

* Epic compiler backend.

   A new compiler backend is being implemented. This backend makes use
   of Edwin Brady's language Epic
   (http://www.cs.st-andrews.ac.uk/~eb/epic.php) and its compiler. The
   backend should handle most Agda code, but is still at an
   experimental stage: more testing is needed, and some things written
   below may not be entirely true.

   The Epic compiler can be invoked from the command line using the
   flag --epic:

     agda --epic --epic-flag=<EPIC-FLAG> --compile-dir=<DIR> <FILE>.agda

   The --epic-flag flag can be given multiple times; each flag is given
   verbatim to the Epic compiler (in the given order). The resulting
   executable is named after the main module and placed in the
   directory specified by the --compile-dir flag (default: the project
   root). Intermediate files are placed in a subdirectory called Epic.

   The backend requires that there is a definition named main. This
   definition should be a value of type IO Unit, but at the moment this
   is not checked (so it is easy to produce a program which segfaults).
   Currently the backend represents actions of type IO A as functions
   from Unit to A, and main is applied to the unit value.

   The Epic compiler compiles via C, not Haskell, so the pragmas
   related to the Haskell FFI (IMPORT, COMPILED_DATA and COMPILED) are
   not used by the Epic backend. Instead there is a new pragma
   COMPILED_EPIC. This pragma is used to give Epic code for postulated
   definitions (Epic code can in turn call C code). The form of the
   pragma is {-# COMPILED_EPIC def code #-}, where def is the name of
   an Agda postulate and code is some Epic code which should include
   the function arguments, return type and function body. As an example
   the IO monad can be defined as follows:

     postulate
       IO     : Set → Set
       return : ∀ {A} → A → IO A
       _>>=_  : ∀ {A B} → IO A → (A → IO B) → IO B

     {-# COMPILED_EPIC return (u : Unit, a : Any) -> Any =
                         ioreturn(a) #-}
     {-# COMPILED_EPIC
           _>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -> Any =
             iobind(x,f) #-}

   Here ioreturn and iobind are Epic functions which are defined in the
   file AgdaPrelude.e which is always included.

   By default the backend will remove so-called forced constructor
   arguments (and case-splitting on forced variables will be
   rewritten). This optimisation can be disabled by using the flag
   --no-forcing.

   All data types which look like unary natural numbers after forced
   constructor arguments have been removed (i.e. types with two
   constructors, one nullary and one with a single recursive argument)
   will be represented as "BigInts". This applies to the standard Fin
   type, for instance.

   The backend supports Agda's primitive functions and the BUILTIN
   pragmas. If the BUILTIN pragmas for unary natural numbers are used,
   then some operations, like addition and multiplication, will use
   more efficient "BigInt" operations.

   If you want to make use of the Epic backend you need to install some
   dependencies, see the README.

* The Emacs mode can compile using either the MAlonzo or the Epic
   backend. The variable agda2-backend controls which backend is used.

-- 
/NAD