Release notes for Agda version 2.4.2

Pragmas and options

New option: --with-K

This can be used to override a global --without-K in a file, by adding a pragma {-# OPTIONS --with-K #-}.

New pragma {-# NON_TERMINATING #-}

This is a safer version of NO_TERMINATION_CHECK which doesn't treat the affected functions as terminating. This means that NON_TERMINATING functions do not reduce during type checking. They do reduce at run-time and when invoking C-c C-n at top-level (but not in a hole).

Language

Instance search is now more efficient and recursive (see Issue #938) (but without termination check yet).

A new keyword instance has been introduced (in the style of abstract and private) which must now be used for every definition/postulate that has to be taken into account during instance resolution. For example:

  record RawMonoid (A : Set) : Set where
    field
      nil  : A
      _++_ : A -> A -> A

  open RawMonoid {{...}}

  instance
    rawMonoidList : {A : Set} -> RawMonoid (List A)
    rawMonoidList = record { nil = []; _++_ = List._++_ }

    rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
    rawMonoidMaybe {A} = record { nil = nothing ; _++_ = catMaybe }
      where
        catMaybe : Maybe A -> Maybe A -> Maybe A
        catMaybe nothing mb = mb
        catMaybe ma nothing = ma
        catMaybe (just a) (just b) = just (a ++ b)

Moreover, each type of an instance must end in (something that reduces to) a named type (e.g. a record, a datatype or a postulate). This allows us to build a simple index structure

  data/record name  -->  possible instances

that speeds up instance search.

Instance search takes into account all local bindings and all global instance bindings and the search is recursive. For instance, searching for

  ? : RawMonoid (Maybe (List A))

will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to unify the first one, succeeding with the second one

  ? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))

and continue with goal

  ?m : RawMonoid (List A)

This will then find

  ?m = rawMonoidList {A = A}

and putting together we have the solution.

Be careful that there is no termination check for now, you can easily make Agda loop by declaring the identity function as an instance. But it shouldn’t be possible to make Agda loop by only declaring structurally recursive instances (whatever that means).

Additionally:

Uniqueness of instances is up to definitional equality (see Issue #899).
Instances of the following form are allowed:
```
EqSigma : {A : Set} {B : A → Set} {{EqA : Eq A}}
          {{EqB : {a : A} → Eq (B a)}}
          → Eq (Σ A B)
```
When searching recursively for an instance of type {a : A} → Eq (B a), a lambda will automatically be introduced and instance search will search for something of type Eq (B a) in the context extended by a : A. When searching for an instance, the a argument does not have to be implicit, but in the definition of EqSigma, instance search will only be able to use EqB if a is implicit.
There is no longer any attempt to solve irrelevant metas by instance search.
Constructors of records and datatypes are automatically added to the instance table.
You can now use quote in patterns.

For instance, here is a function that unquotes a (closed) natural number term.

  unquoteNat : Term → Maybe Nat
  unquoteNat (con (quote Nat.zero) [])            = just zero
  unquoteNat (con (quote Nat.suc) (arg _ n ∷ [])) = fmap suc (unquoteNat n)
  unquoteNat _                                    = nothing

The builtin constructors AGDATERMUNSUPPORTED and AGDASORTUNSUPPORTED are now translated to meta variables when unquoting.
New syntactic sugar tactic e and tactic e | e1 | .. | en.

It desugars as follows and makes it less unwieldy to call reflection-based tactics.

  tactic e                --> quoteGoal g in unquote (e g)
  tactic e | e1 | .. | en --> quoteGoal g in unquote (e g) e1 .. en

Note that in the second form the tactic function should generate a function from a number of new subgoals to the original goal. The type of e should be Term -> Term in both cases.

New reflection builtins for literals.

The term data type AGDATERM now needs an additional constructor AGDATERMLIT taking a reflected literal defined as follows (with appropriate builtin bindings for the types Nat, Float, etc).

  data Literal : Set where
    nat    : Nat    → Literal
    float  : Float  → Literal
    char   : Char   → Literal
    string : String → Literal
    qname  : QName  → Literal

  {-# BUILTIN AGDALITERAL   Literal #-}
  {-# BUILTIN AGDALITNAT    nat     #-}
  {-# BUILTIN AGDALITFLOAT  float   #-}
  {-# BUILTIN AGDALITCHAR   char    #-}
  {-# BUILTIN AGDALITSTRING string  #-}
  {-# BUILTIN AGDALITQNAME  qname   #-}

When quoting (quoteGoal or quoteTerm) literals will be mapped to the AGDATERMLIT constructor. Previously natural number literals were quoted to suc/zero application and other literals were quoted to AGDATERMUNSUPPORTED.

New reflection builtins for function definitions.

AGDAFUNDEF should now map to a data type defined as follows

(with

  {-# BUILTIN QNAME       QName   #-}
  {-# BUILTIN ARG         Arg     #-}
  {-# BUILTIN AGDATERM    Term    #-}
  {-# BUILTIN AGDATYPE    Type    #-}
  {-# BUILTIN AGDALITERAL Literal #-}

  data Pattern : Set where
    con    : QName → List (Arg Pattern) → Pattern
    dot    : Pattern
    var    : Pattern
    lit    : Literal → Pattern
    proj   : QName → Pattern
    absurd : Pattern

  {-# BUILTIN AGDAPATTERN   Pattern #-}
  {-# BUILTIN AGDAPATCON    con     #-}
  {-# BUILTIN AGDAPATDOT    dot     #-}
  {-# BUILTIN AGDAPATVAR    var     #-}
  {-# BUILTIN AGDAPATLIT    lit     #-}
  {-# BUILTIN AGDAPATPROJ   proj    #-}
  {-# BUILTIN AGDAPATABSURD absurd  #-}

  data Clause : Set where
    clause        : List (Arg Pattern) → Term → Clause
    absurd-clause : List (Arg Pattern) → Clause

  {-# BUILTIN AGDACLAUSE       Clause        #-}
  {-# BUILTIN AGDACLAUSECLAUSE clause        #-}
  {-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}

  data FunDef : Set where
    fun-def : Type → List Clause → FunDef

  {-# BUILTIN AGDAFUNDEF    FunDef  #-}
  {-# BUILTIN AGDAFUNDEFCON fun-def #-}

New reflection builtins for extended (pattern-matching) lambda.

The AGDATERM data type has been augmented with a constructor

  AGDATERMEXTLAM : List AGDACLAUSE → List (ARG AGDATERM) → AGDATERM

Absurd lambdas (λ ()) are quoted to extended lambdas with an absurd clause.

Unquoting declarations.

You can now define (recursive) functions by reflection using the new unquoteDecl declaration

  unquoteDecl x = e

Here e should have type AGDAFUNDEF and evaluate to a closed value. This value is then spliced in as the definition of x. In the body e, x has type QNAME which lets you splice in recursive definitions.

Standard modifiers, such as fixity declarations, can be applied to x as expected.

Quoted levels

Universe levels are now quoted properly instead of being quoted to AGDASORTUNSUPPORTED. Setω still gets an unsupported sort, however.

Module applicants can now be operator applications.

Example:

  postulate
    [_] : A -> B

  module M (b : B) where

  module N (a : A) = M [ a ]

[See Issue #1245]

Minor change in module application semantics. [Issue #892]

Previously re-exported functions were not redefined when instantiating a module. For instance

  module A where f = ...
  module B (X : Set) where
    open A public
  module C = B Nat

In this example C.f would be an alias for A.f, so if both A and C were opened f would not be ambiguous. However, this behaviour is not correct when A and B share some module parameters (Issue #892). To fix this C now defines its own copy of f (which evaluates to A.f), which means that opening A and C results in an ambiguous f.

Type checking

Recursive records need to be declared as either inductive or coinductive. inductive is no longer default for recursive records. Examples:

  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

  record Tree (A : Set) : Set where
    inductive
    constructor tree
    field
      elem     : A
      subtrees : List (Tree A)

  record Stream (A : Set) : Set where
    coinductive
    constructor _::_
    field
      head : A
      tail : Stream A

If you are using old-style (musical) coinduction, a record may have to be declared as inductive, paradoxically.

  record Stream (A : Set) : Set where
    inductive -- YES, THIS IS INTENDED !
    constructor _∷_
    field
      head : A
      tail : ∞ (Stream A)

This is because the "coinduction" happens in the use of ∞ and not in the use of record.

Tools

Emacs mode

A new menu option Display can be used to display the version of the running Agda process.

LaTeX-backend

New experimental option references has been added. When specified, i.e.:

  \usepackage[references]{agda}

a new command called \AgdaRef is provided, which lets you reference previously typeset commands, e.g.:

Let us postulate \AgdaRef{apa}.

  \begin{code}
  postulate
    apa : Set
  \end{code}

Above apa will be typeset (highlighted) the same in the text as in the code, provided that the LaTeX output is post-processed using src/data/postprocess-latex.pl, e.g.:

  cp $(dirname $(dirname $(agda-mode locate)))/postprocess-latex.pl .
  agda -i. --latex Example.lagda
  cd latex/
  perl ../postprocess-latex.pl Example.tex > Example.processed
  mv Example.processed Example.tex
  xelatex Example.tex

Mix-fix and Unicode should work as expected (Unicode requires XeLaTeX/LuaLaTeX), but there are limitations:

Overloading identifiers should be avoided, if multiples exist \AgdaRef will typeset according to the first it finds.
Only the current module is used, should you need to reference identifiers in other modules then you need to specify which other module manually, i.e. \AgdaRef[module]{identifier}.

2.4.2.md 11 KB Permalink History Raw