Release notes for Agda version 2.5.1 ==================================== Documentation ------------- * There is now an official Agda User Manual: https://agda.readthedocs.io/ Installation and infrastructure ------------------------------- * Builtins and primitives are now defined in a new set of modules available to all users, independent of any particular library. The modules are ```agda Agda.Builtin.Bool Agda.Builtin.Char Agda.Builtin.Coinduction Agda.Builtin.Equality Agda.Builtin.Float Agda.Builtin.FromNat Agda.Builtin.FromNeg Agda.Builtin.FromString Agda.Builtin.IO Agda.Builtin.Int Agda.Builtin.List Agda.Builtin.Nat Agda.Builtin.Reflection Agda.Builtin.Size Agda.Builtin.Strict Agda.Builtin.String Agda.Builtin.TrustMe Agda.Builtin.Unit ``` The standard library reexports the primitives from the new modules. The `Agda.Builtin` modules are installed in the same way as `Agda.Primitive`, but unlike `Agda.Primitive` they are not loaded automatically. Pragmas and options ------------------- * Library management There is a new 'library' concept for managing include paths. A library consists of - a name, - a set of libraries it depends on, and - a set of include paths. A library is defined in a `.agda-lib` file using the following format: ``` name: LIBRARY-NAME -- Comment depend: LIB1 LIB2 LIB3 LIB4 include: PATH1 PATH2 PATH3 ``` Dependencies are library names, not paths to `.agda-lib` files, and include paths are relative to the location of the library-file. To be useable, a library file has to be listed (with its full path) in `AGDA_DIR/libraries` (or `AGDA_DIR/libraries-VERSION`, for a given Agda version). `AGDA_DIR` defaults to `~/.agda` on Unix-like systems and `C:/Users/USERNAME/AppData/Roaming/agda` or similar on Windows, and can be overridden by setting the `AGDA_DIR` environment variable. Environment variables in the paths (of the form `$VAR` or `${VAR}`) are expanded. The location of the libraries file used can be overridden using the `--library-file=FILE` flag, although this is not expected to be very useful. You can find out the precise location of the 'libraries' file by calling `agda -l fjdsk Dummy.agda` and looking at the error message (assuming you don't have a library called fjdsk installed). There are three ways a library gets used: - You supply the `--library=LIB` (or `-l LIB`) option to Agda. This is equivalent to adding a `-iPATH` for each of the include paths of `LIB` and its (transitive) dependencies. - No explicit `--library` flag is given, and the current project root (of the Agda file that is being loaded) or one of its parent directories contains a `.agda-lib` file defining a library `LIB`. This library is used as if a `--librarary=LIB` option had been given, except that it is not necessary for the library to be listed in the `AGDA_DIR/libraries` file. - No explicit `--library` flag, and no `.agda-lib` file in the project root. In this case the file `AGDA_DIR/defaults` is read and all libraries listed are added to the path. The defaults file should contain a list of library names, each on a separate line. In this case the current directory is also added to the path. To disable default libraries, you can give the flag `--no-default-libraries`. Library names can end with a version number (for instance, `mylib-1.2.3`). When resolving a library name (given in a `--library` flag, or listed as a default library or library dependency) the following rules are followed: - If you don't give a version number, any version will do. - If you give a version number an exact match is required. - When there are multiple matches an exact match is preferred, and otherwise the latest matching version is chosen. For example, suppose you have the following libraries installed: `mylib`, `mylib-1.0`, `otherlib-2.1`, and `otherlib-2.3`. In this case, aside from the exact matches you can also say `--library=otherlib` to get `otherlib-2.3`. * New Pragma `COMPILED_DECLARE_DATA` for binding recursively defined Haskell data types to recursively defined Agda data types. If you have a Haskell type like ```haskell {-# LANGUAGE GADTs #-} module Issue223 where data A where BA :: B -> A data B where AB :: A -> B BB :: B ``` You can now bind it to corresponding mutual Agda inductive data types as follows: ```agda {-# IMPORT Issue223 #-} data A : Set {-# COMPILED_DECLARE_DATA A Issue223.A #-} data B : Set {-# COMPILED_DECLARE_DATA B Issue223.B #-} data A where BA : B → A {-# COMPILED_DATA A Issue223.A Issue223.BA #-} data B where AB : A → B BB : B {-# COMPILED_DATA B Issue223.B Issue223.AB Issue223.BB #-} ``` This fixes Issue [#223](https://github.com/agda/agda/issues/223). * New pragma `HASKELL` for adding inline Haskell code (GHC backend only) Arbitrary Haskell code can be added to a module using the `HASKELL` pragma. For instance, ```agda {-# HASKELL echo :: IO () echo = getLine >>= putStrLn #-} postulate echo : IO ⊤ {-# COMPILED echo echo #-} ``` * New option `--exact-split`. The `--exact-split` flag causes Agda to raise an error whenever a clause in a definition by pattern matching cannot be made to hold definitionally (i.e. as a reduction rule). Specific clauses can be excluded from this check by means of the `{-# CATCHALL #-}` pragma. For instance, the following definition will be rejected as the second clause cannot be made to hold definitionally: ```agda min : Nat → Nat → Nat min zero y = zero min x zero = zero min (suc x) (suc y) = suc (min x y ``` Catchall clauses have to be marked as such, for instance: ```agda eq : Nat → Nat → Bool eq zero zero = true eq (suc m) (suc n) = eq m n {-# CATCHALL #-} eq _ _ = false ``` * New option: `--no-exact-split`. This option can be used to override a global `--exact-split` in a file, by adding a pragma `{-# OPTIONS --no-exact-split #-}`. * New options: `--sharing` and `--no-sharing`. These options are used to enable/disable sharing and call-by-need evaluation. The default is `--no-sharing`. Note that they cannot appear in an `OPTIONS` pragma, but have to be given as command line arguments or added to the Agda Program Args from Emacs with `M-x customize-group agda2`. * New pragma `DISPLAY`. ```agda {-# DISPLAY f e1 .. en = e #-} ``` This causes `f e1 .. en` to be printed in the same way as `e`, where `ei` can bind variables used in `e`. The expressions `ei` and `e` are scope checked, but not type checked. For example this can be used to print overloaded (instance) functions with the overloaded name: ```agda instance NumNat : Num Nat NumNat = record { ..; _+_ = natPlus } {-# DISPLAY natPlus a b = a + b #-} ``` Limitations - Left-hand sides are restricted to variables, constructors, defined functions or types, and literals. In particular, lambdas are not allowed in left-hand sides. - Since `DISPLAY` pragmas are not type checked implicit argument insertion may not work properly if the type of `f` computes to an implicit function space after pattern matching. * Removed pragma `{-# ETA R #-}` The pragma `{-# ETA R #-}` is replaced by the `eta-equality` directive inside record declarations. * New option `--no-eta-equality`. The `--no-eta-equality` flag disables eta rules for declared record types. It has the same effect as `no-eta-equality` inside each declaration of a record type `R`. If used with the `OPTIONS` pragma it will not affect records defined in other modules. * The semantics of `{-# REWRITE r #-}` pragmas in parametrized modules has changed (see Issue [#1652](https://github.com/agda/agda/issues/1652)). Rewrite rules are no longer lifted to the top context. Instead, they now only apply to terms in (extensions of) the module context. If you want the old behaviour, you should put the `{-# REWRITE r #-}` pragma outside of the module (i.e. unindent it). * New pragma `{-# INLINE f #-}` causes `f` to be inlined during compilation. * The `STATIC` pragma is now taken into account during compilation. Calls to a function marked `STATIC` are normalised before compilation. The typical use case for this is to mark the interpreter of an embedded language as `STATIC`. * Option `--type-in-type` no longer implies `--no-universe-polymorphism`, thus, it can be used with explicit universe levels. [Issue [#1764](https://github.com/agda/agda/issues/1764)] It simply turns off error reporting for any level mismatch now. Examples: ```agda {-# OPTIONS --type-in-type #-} Type : Set Type = Set data D {α} (A : Set α) : Set where d : A → D A data E α β : Set β where e : Set α → E α β ``` * New `NO_POSITIVITY_CHECK` pragma to switch off the positivity checker for data/record definitions and mutual blocks. The pragma must precede a data/record definition or a mutual block. The pragma cannot be used in `--safe` mode. Examples (see `Issue1614*.agda` and `Issue1760*.agda` in `test/Succeed/`): 1. Skipping a single data definition. ```agda {-# NO_POSITIVITY_CHECK #-} data D : Set where lam : (D → D) → D ``` 2. Skipping a single record definition. ```agda {-# NO_POSITIVITY_CHECK #-} record U : Set where field ap : U → U ``` 3. Skipping an old-style mutual block: Somewhere within a `mutual` block before a data/record definition. ```agda mutual data D : Set where lam : (D → D) → D {-# NO_POSITIVITY_CHECK #-} record U : Set where field ap : U → U ``` 4. Skipping an old-style mutual block: Before the `mutual` keyword. ```agda {-# NO_POSITIVITY_CHECK #-} mutual data D : Set where lam : (D → D) → D record U : Set where field ap : U → U ``` 5. Skipping a new-style mutual block: Anywhere before the declaration or the definition of data/record in the block. ```agda record U : Set data D : Set record U where field ap : U → U {-# NO_POSITIVITY_CHECK #-} data D where lam : (D → D) → D ``` * Removed `--no-coverage-check` option. [Issue [#1918](https://github.com/agda/agda/issues/1918)] Language -------- ### Operator syntax * The default fixity for syntax declarations has changed from -666 to 20. * Sections. Operators can be sectioned by replacing arguments with underscores. There must not be any whitespace between these underscores and the adjacent nameparts. Examples: ```agda pred : ℕ → ℕ pred = _∸ 1 T : Bool → Set T = if_then ⊤ else ⊥ if : {A : Set} (b : Bool) → A → A → A if b = if b then_else_ ``` Sections are translated into lambda expressions. Examples: ```agda _∸ 1 ↦ λ section → section ∸ 1 if_then ⊤ else ⊥ ↦ λ section → if section then ⊤ else ⊥ if b then_else_ ↦ λ section section₁ → if b then section else section₁ ``` Operator sections have the same fixity as the underlying operator (except in cases like `if b then_else_`, in which the section is "closed", but the operator is not). Operator sections are not supported in patterns (with the exception of dot patterns), and notations coming from syntax declarations cannot be sectioned. * A long-standing operator fixity bug has been fixed. As a consequence some programs that used to parse no longer do. Previously each precedence level was (incorrectly) split up into five separate ones, ordered as follows, with the earlier ones binding less tightly than the later ones: - Non-associative operators. - Left associative operators. - Right associative operators. - Prefix operators. - Postfix operators. Now this problem has been addressed. It is no longer possible to mix operators of a given precedence level but different associativity. However, prefix and right associative operators are seen as having the same associativity, and similarly for postfix and left associative operators. Examples -------- The following code is no longer accepted: ```agda infixl 6 _+_ infix 6 _∸_ rejected : ℕ rejected = 1 + 0 ∸ 1 ``` However, the following previously rejected code is accepted: ```agda infixr 4 _,_ infix 4 ,_ ,_ : {A : Set} {B : A → Set} {x : A} → B x → Σ A B , y = _ , y accepted : Σ ℕ λ i → Σ ℕ λ j → Σ (i ≡ j) λ _ → Σ ℕ λ k → j ≡ k accepted = 5 , , refl , , refl ``` * The classification of notations with binders into the categories infix, prefix, postfix or closed has changed. [Issue [#1450](https://github.com/agda/agda/issues/1450)] The difference is that, when classifying the notation, only *regular* holes are taken into account, not *binding* ones. Example: The notation ```agda syntax m >>= (λ x → f) = x <- m , f ``` was previously treated as infix, but is now treated as prefix. * Notation can now include wildcard binders. Example: `syntax Σ A (λ _ → B) = A × B` * If an overloaded operator is in scope with several distinct precedence levels, then several instances of this operator will be included in the operator grammar, possibly leading to ambiguity. Previously the operator was given the default fixity [Issue [#1436](https://github.com/agda/agda/issues/1436)]. There is an exception to this rule: If there are multiple precedences, but at most one is explicitly declared, then only one instance will be included in the grammar. If there are no explicitly declared precedences, then this instance will get the default precedence, and otherwise it will get the declared precedence. If multiple occurrences of an operator are "merged" in the grammar, and they have distinct associativities, then they are treated as being non-associative. The three paragraphs above also apply to identical notations (coming from syntax declarations) for a given overloaded name. Examples: ```agda module A where infixr 5 _∷_ infixr 5 _∙_ infixl 3 _+_ infix 1 bind syntax bind c (λ x → d) = x ← c , d module B where infix 5 _∷_ infixr 4 _∙_ -- No fixity declaration for _+_. infixl 2 bind syntax bind c d = c ∙ d module C where infixr 2 bind syntax bind c d = c ∙ d open A open B open C -- _∷_ is infix 5. -- _∙_ has two fixities: infixr 4 and infixr 5. -- _+_ is infixl 3. -- A.bind's notation is infix 1. -- B.bind and C.bind's notations are infix 2. -- There is one instance of "_ ∷ _" in the grammar, and one -- instance of "_ + _". -- There are three instances of "_ ∙ _" in the grammar, one -- corresponding to A._∙_, one corresponding to B._∙_, and one -- corresponding to both B.bind and C.bind. ``` ### Reflection * The reflection framework has received a massive overhaul. A new type of reflected type checking computations supplants most of the old reflection primitives. The `quoteGoal`, `quoteContext` and tactic primitives are deprecated and will be removed in the future, and the `unquoteDecl` and `unquote` primitives have changed behaviour. Furthermore the following primitive functions have been replaced by builtin type checking computations: ```agda - primQNameType --> AGDATCMGETTYPE - primQNameDefinition --> AGDATCMGETDEFINITION - primDataConstructors --> subsumed by AGDATCMGETDEFINITION - primDataNumberOfParameters --> subsumed by AGDATCMGETDEFINITION ``` See below for details. * Types are no longer packaged with a sort. The `AGDATYPE` and `AGDATYPEEL` built-ins have been removed. Reflected types are now simply terms. * Reflected definitions have more information. The type for reflected definitions has changed to ```agda data Definition : Set where fun-def : List Clause → Definition data-type : Nat → List Name → Definition -- parameters and constructors record-type : Name → Definition -- name of the data/record type data-con : Name → Definition -- name of the constructor axiom : Definition prim-fun : Definition ``` Correspondingly the built-ins for function, data and record definitions (`AGDAFUNDEF`, `AGDAFUNDEFCON`, `AGDADATADEF`, `AGDARECORDDEF`) have been removed. * Reflected type checking computations. There is a primitive `TC` monad representing type checking computations. The `unquote`, `unquoteDecl`, and the new `unquoteDef` all expect computations in this monad (see below). The interface to the monad is the following ```agda -- Error messages can contain embedded names and terms. data ErrorPart : Set where strErr : String → ErrorPart termErr : Term → ErrorPart nameErr : Name → ErrorPart {-# BUILTIN AGDAERRORPART ErrorPart #-} {-# BUILTIN AGDAERRORPARTSTRING strErr #-} {-# BUILTIN AGDAERRORPARTTERM termErr #-} {-# BUILTIN AGDAERRORPARTNAME nameErr #-} postulate TC : ∀ {a} → Set a → Set a returnTC : ∀ {a} {A : Set a} → A → TC A bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B -- Unify two terms, potentially solving metavariables in the process. unify : Term → Term → TC ⊤ -- Throw a type error. Can be caught by catchTC. typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A -- Block a type checking computation on a metavariable. This will abort -- the computation and restart it (from the beginning) when the -- metavariable is solved. blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A -- Backtrack and try the second argument if the first argument throws a -- type error. catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A -- Infer the type of a given term inferType : Term → TC Type -- Check a term against a given type. This may resolve implicit arguments -- in the term, so a new refined term is returned. Can be used to create -- new metavariables: newMeta t = checkType unknown t checkType : Term → Type → TC Term -- Compute the normal form of a term. normalise : Term → TC Term -- Get the current context. getContext : TC (List (Arg Type)) -- Extend the current context with a variable of the given type. extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A -- Set the current context. inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A -- Quote a value, returning the corresponding Term. quoteTC : ∀ {a} {A : Set a} → A → TC Term -- Unquote a Term, returning the corresponding value. unquoteTC : ∀ {a} {A : Set a} → Term → TC A -- Create a fresh name. freshName : String → TC QName -- Declare a new function of the given type. The function must be defined -- later using 'defineFun'. Takes an Arg Name to allow declaring instances -- and irrelevant functions. The Visibility of the Arg must not be hidden. declareDef : Arg QName → Type → TC ⊤ -- Define a declared function. The function may have been declared using -- 'declareDef' or with an explicit type signature in the program. defineFun : QName → List Clause → TC ⊤ -- Get the type of a defined name. Replaces 'primQNameType'. getType : QName → TC Type -- Get the definition of a defined name. Replaces 'primQNameDefinition'. getDefinition : QName → TC Definition {-# BUILTIN AGDATCM TC #-} {-# BUILTIN AGDATCMRETURN returnTC #-} {-# BUILTIN AGDATCMBIND bindTC #-} {-# BUILTIN AGDATCMUNIFY unify #-} {-# BUILTIN AGDATCMNEWMETA newMeta #-} {-# BUILTIN AGDATCMTYPEERROR typeError #-} {-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-} {-# BUILTIN AGDATCMCATCHERROR catchTC #-} {-# BUILTIN AGDATCMINFERTYPE inferType #-} {-# BUILTIN AGDATCMCHECKTYPE checkType #-} {-# BUILTIN AGDATCMNORMALISE normalise #-} {-# BUILTIN AGDATCMGETCONTEXT getContext #-} {-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-} {-# BUILTIN AGDATCMINCONTEXT inContext #-} {-# BUILTIN AGDATCMQUOTETERM quoteTC #-} {-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-} {-# BUILTIN AGDATCMFRESHNAME freshName #-} {-# BUILTIN AGDATCMDECLAREDEF declareDef #-} {-# BUILTIN AGDATCMDEFINEFUN defineFun #-} {-# BUILTIN AGDATCMGETTYPE getType #-} {-# BUILTIN AGDATCMGETDEFINITION getDefinition #-} ``` * Builtin type for metavariables There is a new builtin type for metavariables used by the new reflection framework. It is declared as follows and comes with primitive equality, ordering and show. ```agda postulate Meta : Set {-# BUILTIN AGDAMETA Meta #-} primitive primMetaEquality : Meta → Meta → Bool primitive primMetaLess : Meta → Meta → Bool primitive primShowMeta : Meta → String ``` There are corresponding new constructors in the `Term` and `Literal` data types: ```agda data Term : Set where ... meta : Meta → List (Arg Term) → Term {-# BUILTIN AGDATERMMETA meta #-} data Literal : Set where ... meta : Meta → Literal {-# BUILTIN AGDALITMETA meta #-} ``` * Builtin unit type The type checker needs to know about the unit type, which you can allow by ```agda record ⊤ : Set where {-# BUILTIN UNIT ⊤ #-} ``` * Changed behaviour of `unquote` The `unquote` primitive now expects a type checking computation instead of a pure term. In particular `unquote e` requires ```agda e : Term → TC ⊤ ``` where the argument is the representation of the hole in which the result should go. The old `unquote` behaviour (where `unquote` expected a `Term` argument) can be recovered by ```agda OLD: unquote v NEW: unquote λ hole → unify hole v ``` * Changed behaviour of `unquoteDecl` The `unquoteDecl` primitive now expects a type checking computation instead of a pure function definition. It is possible to define multiple (mutually recursive) functions at the same time. More specifically ```agda unquoteDecl x₁ .. xₙ = m ``` requires `m : TC ⊤` and that `x₁ .. xₙ` are defined (using `declareDef` and `defineFun`) after executing `m`. As before `x₁ .. xₙ : QName` in `m`, but have their declared types outside the `unquoteDecl`. * New primitive `unquoteDef` There is a new declaration ```agda unquoteDef x₁ .. xₙ = m ``` This works exactly as `unquoteDecl` (see above) with the exception that `x₁ .. xₙ` are required to already be declared. The main advantage of `unquoteDef` over `unquoteDecl` is that `unquoteDef` is allowed in mutual blocks, allowing mutually recursion between generated definitions and hand-written definitions. * The reflection interface now exposes the name hint (as a string) for variables. As before, the actual binding structure is with de Bruijn indices. The String value is just a hint used as a prefix to help display the variable. The type `Abs` is a new builtin type used for the constructors `Term.lam`, `Term.pi`, `Pattern.var` (bultins `AGDATERMLAM`, `AGDATERMPI` and `AGDAPATVAR`). ```agda data Abs (A : Set) : Set where abs : (s : String) (x : A) → Abs A {-# BUILTIN ABS Abs #-} {-# BUILTIN ABSABS abs #-} ``` Updated constructor types: ```agda Term.lam : Hiding → Abs Term → Term Term.pi : Arg Type → Abs Type → Term Pattern.var : String → Pattern ``` * Reflection-based macros Macros are functions of type `t1 → t2 → .. → Term → TC ⊤` that are defined in a `macro` block. Macro application is guided by the type of the macro, where `Term` arguments desugar into the `quoteTerm` syntax and `Name` arguments into the `quote` syntax. Arguments of any other type are preserved as-is. The last `Term` argument is the hole term given to `unquote` computation (see above). For example, the macro application `f u v w` where the macro `f` has the type `Term → Name → Bool → Term → TC ⊤` desugars into `unquote (f (quoteTerm u) (quote v) w)` Limitations: - Macros cannot be recursive. This can be worked around by defining the recursive function outside the macro block and have the macro call the recursive function. Silly example: ```agda macro plus-to-times : Term → Term → TC ⊤ plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ [])) plus-to-times v hole = unify hole v thm : (a b : Nat) → plus-to-times (a + b) ≡ a * b thm a b = refl ``` Macros are most useful when writing tactics, since they let you hide the reflection machinery. For instance, suppose you have a solver ```agda magic : Type → Term ``` that takes a reflected goal and outputs a proof (when successful). You can then define the following macro ```agda macro by-magic : Term → TC ⊤ by-magic hole = bindTC (inferType hole) λ goal → unify hole (magic goal) ``` This lets you apply the magic tactic without any syntactic noise at all: ```agda thm : ¬ P ≡ NP thm = by-magic ``` ### Literals and built-ins * Overloaded number literals. You can now overload natural number literals using the new builtin `FROMNAT`: ```agda {-# BUILTIN FROMNAT fromNat #-} ``` The target of the builtin should be a defined name. Typically you would do something like ```agda record Number (A : Set) : Set where field fromNat : Nat → A open Number {{...}} public {-# BUILTIN FROMNAT fromNat #-} ``` This will cause number literals `n` to be desugared to `fromNat n` before type checking. * Negative number literals. Number literals can now be negative. For floating point literals it works as expected. For integer literals there is a new builtin `FROMNEG` that enables negative integer literals: ```agda {-# BUILTIN FROMNEG fromNeg #-} ``` This causes negative literals `-n` to be desugared to `fromNeg n`. * Overloaded string literals. String literals can be overladed using the `FROMSTRING` builtin: ```agda {-# BUILTIN FROMSTRING fromString #-} ``` The will cause string literals `s` to be desugared to `fromString s` before type checking. * Change to builtin integers. The `INTEGER` builtin now needs to be bound to a datatype with two constructors that should be bound to the new builtins `INTEGERPOS` and `INTEGERNEGSUC` as follows: ```agda data Int : Set where pos : Nat -> Int negsuc : Nat -> Int {-# BUILTIN INTEGER Int #-} {-# BUILTIN INTEGERPOS pos #-} {-# BUILTIN INTEGERNEGSUC negsuc #-} ``` where `negsuc n` represents the integer `-n - 1`. For instance, `-5` is represented as `negsuc 4`. All primitive functions on integers except `primShowInteger` have been removed, since these can be defined without too much trouble on the above representation using the corresponding functions on natural numbers. The primitives that have been removed are ```agda primIntegerPlus primIntegerMinus primIntegerTimes primIntegerDiv primIntegerMod primIntegerEquality primIntegerLess primIntegerAbs primNatToInteger ``` * New primitives for strict evaluation ```agda primitive primForce : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x ``` `primForce x f` evaluates to `f x` if x is in weak head normal form, and `primForceLemma x f` evaluates to `refl` in the same situation. The following values are considered to be in weak head normal form: - constructor applications - literals - lambda abstractions - type constructor (data/record types) applications - function types - Set a ### Modules * Modules in import directives When you use `using`/`hiding`/`renaming` on a name it now automatically applies to any module of the same name, unless you explicitly mention the module. For instance, ```agda open M using (D) ``` is equivalent to ```agda open M using (D; module D) ``` if `M` defines a module `D`. This is most useful for record and data types where you always get a module of the same name as the type. With this feature there is no longer useful to be able to qualify a constructor (or field) by the name of the data type even when it differs from the name of the corresponding module. The follow (weird) code used to work, but doesn't work anymore: ```agda module M where data D where c : D open M using (D) renaming (module D to MD) foo : D foo = D.c ``` If you want to import only the type name and not the module you have to hide it explicitly: ```agda open M using (D) hiding (module D) ``` See discussion on Issue [#836](https://github.com/agda/agda/issues/836). * Private definitions of a module are no longer in scope at the Emacs mode top-level. The reason for this change is that `.agdai-files` are stripped of unused private definitions (which can yield significant performance improvements for module-heavy code). To test private definitions you can create a hole at the bottom of the module, in which private definitions will be visible. ### Records * New record directives `eta-equality`/`no-eta-equality` The keywords `eta-equality`/`no-eta-equality` enable/disable eta rules for the (inductive) record type being declared. ```agda record Σ (A : Set) (B : A -> Set) : Set where no-eta-equality constructor _,_ field fst : A snd : B fst open Σ -- fail : ∀ {A : Set}{B : A -> Set} → (x : Σ A B) → x ≡ (fst x , snd x) -- fail x = refl -- -- x != fst x , snd x of type Σ .A .B -- when checking that the expression refl has type x ≡ (fst x , snd x) ``` * Building records from modules. The `record { }` syntax is now extended to accept module names as well. Fields are thus defined using the corresponding definitions from the given module. For instance assuming this record type `R` and module `M`: ```agda record R : Set where field x : X y : Y z : Z module M where x = {! ... !} y = {! ... !} r : R r = record { M; z = {! ... !} } ``` Previously one had to write `record { x = M.x; y = M.y; z = {! ... !} }`. More precisely this construction now supports any combination of explicit field definitions and applied modules. If a field is both given explicitly and available in one of the modules, then the explicit one takes precedence. If a field is available in more than one module then this is ambiguous and therefore rejected. As a consequence the order of assignments does not matter. The modules can be both applied to arguments and have import directives such as `hiding`, `using`, and `renaming`. In particular this construct subsumes the record update construction. Here is an example of record update: ```agda -- Record update. Same as: record r { y = {! ... !} } r2 : R r2 = record { R r; y = {! ... !} } ``` A contrived example showing the use of `hiding`/`renaming`: ```agda module M2 (a : A) where w = {! ... !} z = {! ... !} r3 : A → R r3 a = record { M hiding (y); M2 a renaming (w to y) } ``` * Record patterns are now accepted. Examples: ```agda swap : {A B : Set} (p : A × B) → B × A swap record{ proj₁ = a; proj₂ = b } = record{ proj₁ = b; proj₂ = a } thd3 : ... thd3 record{ proj₂ = record { proj₂ = c }} = c ``` * Record modules now properly hide all their parameters [Issue [#1759](https://github.com/agda/agda/issues/1759)] Previously parameters to parent modules were not hidden in the record module, resulting in different behaviour between ```agda module M (A : Set) where record R (B : Set) : Set where ``` and ```agda module M where record R (A B : Set) : Set where ``` where in the former case, `A` would be an explicit argument to the module `M.R`, but implicit in the latter case. Now `A` is implicit in both cases. ### Instance search * Performance has been improved, recursive instance search which was previously exponential in the depth is now only quadratic. * Constructors of records and datatypes are not anymore automatically considered as instances, you have to do so explicitely, for instance: ```agda -- only [b] is an instance of D data D : Set where a : D instance b : D c : D -- the constructor is now an instance record tt : Set where instance constructor tt ``` * Lambda-bound variables are no longer automatically considered instances. Lambda-bound variables need to be bound as instance arguments to be considered for instance search. For example, ```agda _==_ : {A : Set} {{_ : Eq A}} → A → A → Bool fails : {A : Set} → Eq A → A → Bool fails eqA x = x == x works : {A : Set} {{_ : Eq A}} → A → Bool works x = x == x ``` * Let-bound variables are no longer automatically considered instances. To make a let-bound variable available as an instance it needs to be declared with the `instance` keyword, just like top-level instances. For example, ```agda mkEq : {A : Set} → (A → A → Bool) → Eq A fails : {A : Set} → (A → A → Bool) → A → Bool fails eq x = let eqA = mkEq eq in x == x works : {A : Set} → (A → A → Bool) → A → Bool works eq x = let instance eqA = mkEq eq in x == x ``` * Record fields can be declared instances. For example, ```agda record EqSet : Set₁ where field set : Set instance eq : Eq set ``` This causes the projection function `eq : (E : EqSet) → Eq (set E)` to be considered for instance search. * Instance search can now find arguments in variable types (but such candidates can only be lambda-bound variables, they can’t be declared as instances) ```agda module _ {A : Set} (P : A → Set) where postulate bla : {x : A} {{_ : P x}} → Set → Set -- Works, the instance argument is found in the context test : {x : A} {{_ : P x}} → Set → Set test B = bla B -- Still forbidden, because [P] could be instantiated later to anything instance postulate forbidden : {x : A} → P x ``` * Instance search now refuses to solve constraints with unconstrained metavariables, since this can lead to non-termination. See [Issue [#1532](https://github.com/agda/agda/issues/1523)] for an example. * Top-level instances are now only considered if they are in scope. [Issue [#1913](https://github.com/agda/agda/issues/1913)] Note that lambda-bound instances need not be in scope. ### Other changes * Unicode ellipsis character is allowed for the ellipsis token `...` in `with` expressions. * `Prop` is no longer a reserved word. Type checking ------------- * Large indices. Force constructor arguments no longer count towards the size of a datatype. For instance, the definition of equality below is accepted. ```agda data _≡_ {a} {A : Set a} : A → A → Set where refl : ∀ x → x ≡ x ``` This gets rid of the asymmetry that the version of equality which indexes only on the second argument could be small, but not the version above which indexes on both arguments. * Detection of datatypes that satisfy K (i.e. sets) Agda will now try to detect datatypes that satisfy K when `--without-K` is enabled. A datatype satisfies K when it follows these three rules: - The types of all non-recursive constructor arguments should satisfy K. - All recursive constructor arguments should be first-order. - The types of all indices should satisfy K. For example, the types `Nat`, `List Nat`, and `x ≡ x` (where `x : Nat`) are all recognized by Agda as satisfying K. * New unifier for case splitting The unifier used by Agda for case splitting has been completely rewritten. The new unifier takes a much more type-directed approach in order to avoid the problems in issues [#1406](https://github.com/agda/agda/issues/1406), [#1408](https://github.com/agda/agda/issues/1408), [#1427](https://github.com/agda/agda/issues/1427), and [#1435](https://github.com/agda/agda/issues/1435). The new unifier also has eta-equality for record types built-in. This should avoid unnecessary case splitting on record constructors and improve the performance of Agda on code that contains deeply nested record patterns (see issues [#473](https://github.com/agda/agda/issues/473), [#635](https://github.com/agda/agda/issues/635), [#1575](https://github.com/agda/agda/issues/1575), [#1603](https://github.com/agda/agda/issues/1603), [#1613](https://github.com/agda/agda/issues/1613), and [#1645](https://github.com/agda/agda/issues/1645)). In some cases, the locations of the dot patterns computed by the unifier did not correspond to the locations given by the user (see Issue [#1608](https://github.com/agda/agda/issues/1608)). This has now been fixed by adding an extra step after case splitting that checks whether the user-written patterns are compatible with the computed ones. In some rare cases, the new unifier is still too restrictive when `--without-K` is enabled because it cannot generalize over the datatype indices (yet). For example, the following code is rejected: ```agda data Bar : Set₁ where bar : Bar baz : (A : Set) → Bar data Foo : Bar → Set where foo : Foo bar test : foo ≡ foo → Set₁ test refl = Set ``` * The aggressive behaviour of `with` introduced in 2.4.2.5 has been rolled back [Issue [#1692](https://github.com/agda/agda/issues/1692)]. With no longer abstracts in the types of variables appearing in the with-expressions. [Issue [#745](https://github.com/agda/agda/issues/745)] This means that the following example no longer works: ```agda fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a fails f b with a | f b fails f b | .b | refl = f b ``` The `with` no longer abstracts the type of `f` over `a`, since `f` appears in the second with-expression `f b`. You can use a nested `with` to make this example work. This example does work again: ```agda test : ∀{A : Set}{a : A}{f : A → A} (p : f a ≡ a) → f (f a) ≡ a test p rewrite p = p ``` After `rewrite p` the goal has changed to `f a ≡ a`, but the type of `p` has not been rewritten, thus, the final `p` solves the goal. The following, which worked in 2.4.2.5, no longer works: ```agda fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a fails f b rewrite f b = f b ``` The rewrite with `f b : a ≡ b` is not applied to `f` as the latter is part of the rewrite expression `f b`. Thus, the type of `f` remains untouched, and the changed goal `b ≡ b` is not solved by `f b`. * When using `rewrite` on a term `eq` of type `lhs ≡ rhs`, the `lhs` is no longer abstracted in `rhs` [Issue [#520](https://github.com/agda/agda/issues/520)]. This means that ```agda f pats rewrite eq = body ``` is more than syntactic sugar for ```agda f pats with lhs | eq f pats | _ | refl = body ``` In particular, the following application of `rewrite` is now possible ```agda id : Bool → Bool id true = true id false = false is-id : ∀ x → x ≡ id x is-id true = refl is-id false = refl postulate P : Bool → Set b : Bool p : P (id b) proof : P b proof rewrite is-id b = p ``` Previously, this was desugared to ```agda proof with b | is-id b proof | _ | refl = p ``` which did not type check as `refl` does not have type `b ≡ id b`. Now, Agda gets the task of checking `refl : _ ≡ id b` leading to instantiation of `_` to `id b`. Compiler backends ----------------- * Major Bug Fixes: - Function clauses with different arities are now always compiled correctly by the GHC/UHC backends. (Issue [#727](https://github.com/agda/agda/issues/727)) * Co-patterns - The GHC/UHC backends now support co-patterns. (Issues [#1567](https://github.com/agda/agda/issues/1567), [#1632](https://github.com/agda/agda/issues/1632)) * Optimizations - Builtin naturals are now represented as arbitrary-precision Integers. See the user manual, section "Agda Compilers -> Optimizations" for details. * GHC Haskell backend (MAlonzo) - Pragmas Since builtin naturals are compiled to `Integer` you can no longer give a `{-# COMPILED_DATA #-}` pragma for `Nat`. The same goes for builtin booleans, integers, floats, characters and strings which are now hard-wired to appropriate Haskell types. * UHC compiler backend A new backend targeting the Utrecht Haskell Compiler (UHC) is available. It targets the UHC Core language, and it's design is inspired by the Epic backend. See the user manual, section "Agda Compilers -> UHC Backend" for installation instructions. - FFI The UHC backend has a FFI to Haskell similar to MAlonzo's. The target Haskell code also needs to be compilable using UHC, which does not support the Haskell base library version 4.*. FFI pragmas for the UHC backend are not checked in any way. If the pragmas are wrong, bad things will happen. - Imports Additional Haskell modules can be brought into scope with the `IMPORT_UHC` pragma: ```agda {-# IMPORT_UHC Data.Char #-} ``` The Haskell modules `UHC.Base` and `UHC.Agda.Builtins` are always in scope and don't need to be imported explicitly. - Datatypes Agda datatypes can be bound to Haskell datatypes as follows: Haskell: ```haskell data HsData a = HsCon1 | HsCon2 (HsData a) ``` Agda: ```agda data AgdaData (A : Set) : Set where AgdaCon1 : AgdaData A AgdaCon2 : AgdaData A -> AgdaData A {-# COMPILED_DATA_UHC AgdaData HsData HsCon1 HsCon2 #-} ``` The mapping has to cover all constructors of the used Haskell datatype, else runtime behavior is undefined! There are special reserved names to bind Agda datatypes to certain Haskell datatypes. For example, this binds an Agda datatype to Haskell's list datatype: Agda: ```agda data AgdaList (A : Set) : Set where Nil : AgdaList A Cons : A -> AgdaList A -> AgdaList A {-# COMPILED_DATA_UHC AgdaList __LIST__ __NIL__ __CONS__ #-} ``` The following "magic" datatypes are available: ``` HS Datatype | Datatype Pragma | HS Constructor | Constructor Pragma () __UNIT__ () __UNIT__ List __LIST__ (:) __CONS__ [] __NIL__ Bool __BOOL__ True __TRUE__ False __FALSE__ ``` - Functions Agda postulates can be bound to Haskell functions. Similar as in MAlonzo, all arguments of type `Set` need to be dropped before calling Haskell functions. An example calling the return function: Agda: ```agda postulate hs-return : {A : Set} -> A -> IO A {-# COMPILED_UHC hs-return (\_ -> UHC.Agda.Builtins.primReturn) #-} ``` Emacs mode and interaction -------------------------- * Module contents (`C-c C-o`) now also works for records. [See Issue [#1926](https://github.com/agda/agda/issues/1926) ] If you have an inferable expression of record type in an interaction point, you can invoke `C-c C-o` to see its fields and types. Example ```agda record R : Set where field f : A test : R → R test r = {!r!} -- C-c C-o here ``` * Less aggressive error notification. Previously Emacs could jump to the position of an error even if the type-checking process was not initiated in the current buffer. Now this no longer happens: If the type-checking process was initiated in another buffer, then the cursor is moved to the position of the error in the buffer visiting the file (if any) and in every window displaying the file, but focus should not change from one file to another. In the cases where focus does change from one file to another, one can now use the go-back functionality to return to the previous position. * Removed the `agda-include-dirs` customization parameter. Use `agda-program-args` with `-iDIR` or `-lLIB` instead, or add libraries to `~/.agda/defaults` (`C:/Users/USERNAME/AppData/Roaming/agda/defaults` or similar on Windows). See Library management, above, for more information. Tools ----- ### LaTeX-backend * The default font has been changed to XITS (which is part of TeX Live): http://www.ctan.org/tex-archive/fonts/xits/ This font is more complete with respect to Unicode. ### agda-ghc-names * New tool: The command ``` agda-ghc-names fixprof .prof ``` converts `*.prof` files obtained from profiling runs of MAlonzo-compiled code to `*.agdaIdents.prof`, with the original Agda identifiers replacing the MAlonzo-generated Haskell identifiers. For usage and more details, see `src/agda-ghc-names/README.txt`. Highlighting and textual backends --------------------------------- * Names in import directives are now highlighted and are clickable. [Issue [#1714](https://github.com/agda/agda/issues/1714)] This leads also to nicer printing in the LaTeX and html backends. Fixed issues ------------ See [bug tracker (milestone 2.5.1)](https://github.com/agda/agda/issues?q=milestone%3A2.5.1+is%3Aclosed)