1Release notes for Agda 2 version 2.2.6
2======================================
3
4Language
5--------
6
7* Universe polymorphism (experimental extension).
8
9  To enable universe polymorphism give the flag
10  `--universe-polymorphism` on the command line or (recommended) as an
11  `OPTIONS` pragma.
12
13  When universe polymorphism is enabled `Set` takes an argument which is
14  the universe level. For instance, the type of universe polymorphic
15  identity is
16
17  ```agda
18  id : {a : Level} {A : Set a} → A → A.
19  ```
20
21  The type Level is isomorphic to the unary natural numbers and should
22  be specified using the BUILTINs `LEVEL`, `LEVELZERO`, and
23  `LEVELSUC`:
24
25  ```agda
26  data Level : Set where
27    zero : Level
28    suc  : Level → Level
29
30  {-# BUILTIN LEVEL     Level #-}
31  {-# BUILTIN LEVELZERO zero  #-}
32  {-# BUILTIN LEVELSUC  suc   #-}
33  ```
34
35  There is an additional BUILTIN `LEVELMAX` for taking the maximum of two
36  levels:
37
38  ```agda
39  max : Level → Level → Level
40  max  zero    m      = m
41  max (suc n)  zero   = suc n
42  max (suc n) (suc m) = suc (max n m)
43
44  {-# BUILTIN LEVELMAX max #-}
45  ```
46
47  The non-polymorphic universe levels `Set`, `Set₁` and so on are
48  sugar for `Set zero`, `Set (suc zero)`, etc.
49
50  At present there is no automatic lifting of types from one level to
51  another. It can still be done (rather clumsily) by defining types
52  like the following one:
53
54  ```agda
55  data Lifted {a} (A : Set a) : Set (suc a) where
56    lift : A → Lifted A
57  ```
58
59  However, it is likely that automatic lifting is introduced at some
60  point in the future.
61
62* Multiple constructors, record fields, postulates or primitives can
63  be declared using a single type signature:
64
65  ```agda
66  data Bool : Set where
67    false true : Bool
68
69  postulate
70    A B : Set
71  ```
72
73* Record fields can be implicit:
74
75  ```agda
76  record R : Set₁ where
77    field
78      {A}         : Set
79      f           : A → A
80      {B C} D {E} : Set
81      g           : B → C → E
82  ```
83
84  By default implicit fields are not printed.
85
86* Record constructors can be defined:
87
88  ```agda
89  record Σ (A : Set) (B : A → Set) : Set where
90    constructor _,_
91    field
92      proj₁ : A
93      proj₂ : B proj₁
94  ```
95
96  In this example `_,_` gets the type
97
98  ```agda
99   (proj₁ : A) → B proj₁ → Σ A B.
100  ```
101
102  For implicit fields the corresponding constructor arguments become
103  implicit.
104
105  Note that the constructor is defined in the *outer* scope, so any
106  fixity declaration has to be given outside the record definition.
107  The constructor is not in scope inside the record module.
108
109  Note also that pattern matching for records has not been implemented
110  yet.
111
112* BUILTIN hooks for equality.
113
114  The data type
115
116  ```agda
117  data _≡_ {A : Set} (x : A) : A → Set where
118    refl : x ≡ x
119  ```
120
121  can be specified as the builtin equality type using the following
122  pragmas:
123
124  ```agda
125  {-# BUILTIN EQUALITY _≡_  #-}
126  {-# BUILTIN REFL     refl #-}
127  ```
128
129  The builtin equality is used for the new rewrite construct and
130  the `primTrustMe` primitive described below.
131
132* New `rewrite` construct.
133
134  If `eqn : a ≡ b`, where `_≡_` is the builtin equality (see above) you
135  can now write
136
137  ```agda
138  f ps rewrite eqn = rhs
139  ```
140
141  instead of
142
143  ```agda
144    f ps with a | eqn
145    ... | ._ | refl = rhs
146  ```
147
148  The `rewrite` construct has the effect of rewriting the goal and the
149  context by the given equation (left to right).
150
151  You can rewrite using several equations (in sequence) by separating
152  them with vertical bars (|):
153
154  ```agda
155  f ps rewrite eqn₁ | eqn₂ | … = rhs
156  ```
157
158  It is also possible to add `with`-clauses after rewriting:
159
160  ```agda
161  f ps rewrite eqns with e
162  ... | p = rhs
163  ```
164
165  Note that pattern matching happens before rewriting—if you want to
166  rewrite and then do pattern matching you can use a with after the
167  rewrite.
168
169  See `test/Succeed/Rewrite.agda` for some examples.
170
171* A new primitive, `primTrustMe`, has been added:
172
173  ```agda
174    primTrustMe : {A : Set} {x y : A} → x ≡ y
175  ```
176
177  Here `_≡_` is the builtin equality (see BUILTIN hooks for equality,
178  above).
179
180  If `x` and `y` are definitionally equal, then
181  `primTrustMe {x = x} {y = y}` reduces to `refl`.
182
183  Note that the compiler replaces all uses of `primTrustMe` with the
184  `REFL` builtin, without any check for definitional
185  equality. Incorrect uses of `primTrustMe` can potentially lead to
186  segfaults or similar problems.
187
188  For an example of the use of `primTrustMe`, see `Data.String` in
189  version 0.3 of the standard library, where it is used to implement
190  decidable equality on strings using the primitive boolean equality.
191
192* Changes to the syntax and semantics of IMPORT pragmas, which are
193  used by the Haskell FFI. Such pragmas must now have the following
194  form:
195
196  ```agda
197  {-# IMPORT <module name> #-}
198  ```
199
200  These pragmas are interpreted as *qualified* imports, so Haskell
201  names need to be given qualified (unless they come from the Haskell
202  prelude).
203
204* The horizontal tab character (U+0009) is no longer treated as white
205  space.
206
207* Line pragmas are no longer supported.
208
209* The `--include-path` flag can no longer be used as a pragma.
210
211* The experimental and incomplete support for proof irrelevance has
212  been disabled.
213
214Tools
215-----
216
217* New `intro` command in the Emacs mode. When there is a canonical way
218  of building something of the goal type (for instance, if the goal
219  type is a pair), the goal can be refined in this way. The command
220  works for the following goal types:
221
222    - A data type where only one of its constructors can be used to
223      construct an element of the goal type. (For instance, if the
224      goal is a non-empty vector, a `cons` will be introduced.)
225
226    - A record type. A record value will be introduced. Implicit
227      fields will not be included unless showing of implicit arguments
228      is switched on.
229
230    - A function type. A lambda binding as many variables as possible
231      will be introduced. The variable names will be chosen from the
232      goal type if its normal form is a dependent function type,
233      otherwise they will be variations on `x`. Implicit lambdas will
234      only be inserted if showing of implicit arguments is switched
235      on.
236
237  This command can be invoked by using the `refine` command
238  (`C-c C-r`) when the goal is empty. (The old behaviour of the refine
239  command in this situation was to ask for an expression using the
240  minibuffer.)
241
242* The Emacs mode displays `Checked` in the mode line if the current
243  file type checked successfully without any warnings.
244
245* If a file `F` is loaded, and this file defines the module `M`, it is
246  an error if `F` is not the file which defines `M` according to the
247  include path.
248
249  Note that the command-line tool and the Emacs mode define the
250  meaning of relative include paths differently: the command-line tool
251  interprets them relative to the current working directory, whereas
252  the Emacs mode interprets them relative to the root directory of the
253  current project. (As an example, if the module `A.B.C` is loaded
254  from the file `<some-path>/A/B/C.agda`, then the root directory is
255  `<some-path>`.)
256
257* It is an error if there are several files on the include path which
258  match a given module name.
259
260* Interface files are relocatable. You can move around source trees as
261  long as the include path is updated in a corresponding way. Note
262  that a module `M` may be re-typechecked if its time stamp is
263  strictly newer than that of the corresponding interface file
264  (`M.agdai`).
265
266* Type-checking is no longer done when an up-to-date interface exists.
267  (Previously the initial module was always type-checked.)
268
269* Syntax highlighting files for Emacs (`.agda.el`) are no longer used.
270  The `--emacs` flag has been removed. (Syntax highlighting
271  information is cached in the interface files.)
272
273* The Agate and Alonzo compilers have been retired. The options
274  `--agate`, `--alonzo` and `--malonzo` have been removed.
275
276* The default directory for MAlonzo output is the project's root
277  directory. The `--malonzo-dir` flag has been renamed to
278  `--compile-dir`.
279
280* Emacs mode: `C-c C-x C-d` no longer resets the type checking state.
281  `C-c C-x C-r` can be used for a more complete reset. `C-c C-x C-s`
282  (which used to reload the syntax highlighting information) has been
283  removed. `C-c C-l` can be used instead.
284
285* The Emacs mode used to define some "abbrevs", unless the user
286  explicitly turned this feature off. The new default is *not* to add
287  any abbrevs. The old default can be obtained by customising
288  `agda2-mode-abbrevs-use-defaults` (a customisation buffer can be
289  obtained by typing `M-x customize-group agda2 RET` after an Agda
290  file has been loaded).
291