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](https://github.com/agda/agda/issues/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: ```agda 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 ```agda ? : RawMonoid (Maybe (List A)) ``` will consider the candidates {`rawMonoidList`, `rawMonoidMaybe`}, fail to unify the first one, succeeding with the second one ```agda ? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A)) ``` and continue with goal ```agda ?m : RawMonoid (List A) ``` This will then find ```agda ?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](https://github.com/agda/agda/issues/899)). - Instances of the following form are allowed: ```agda 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. ```agda 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. ```agda 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). ```agda 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 ```agda {-# BUILTIN QNAME QName #-} {-# BUILTIN ARG Arg #-} {-# BUILTIN AGDATERM Term #-} {-# BUILTIN AGDATYPE Type #-} {-# BUILTIN AGDALITERAL Literal #-} ``` ). ```agda 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 ```agda 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 ```agda 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: ```agda postulate [_] : A -> B module M (b : B) where module N (a : A) = M [ a ] ``` [See Issue [#1245](https://github.com/agda/agda/issues/1245)] * Minor change in module application semantics. [Issue [#892](https://github.com/agda/agda/issues/892)] Previously re-exported functions were not redefined when instantiating a module. For instance ```agda 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](https://github.com/agda/agda/issues/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: ```agda 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. ```agda 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.: ```latex \usepackage[references]{agda} ``` a new command called `\AgdaRef` is provided, which lets you reference previously typeset commands, e.g.: Let us postulate `\AgdaRef{apa}`. ```agda \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}`.