1
1
------------------------------------------------------------------------
2
-- Release notes for Agda version 2.4.2.2
3
------------------------------------------------------------------------
5
Important changes since 2.4.2.1:
10
* Compilation on Windows fixed.
12
* Other issues fixed ( see https://code.google.com/p/agda/issues )
19
------------------------------------------------------------------------
20
-- Release notes for Agda version 2.4.2.1
21
------------------------------------------------------------------------
23
Important changes since 2.4.2:
28
* New pragma {-# TERMINATING #-} replacing {-# NO_TERMINATION_CHECK #-}
30
Complements the existing pragma {-# NON_TERMINATING #-}.
31
Skips termination check for the associated definitions and marks
32
them as terminating. Thus, it is a replacement for
33
{-# NO_TERMINATION_CHECK #-} with the same semantics.
35
You can no longer use pragma {-# NO_TERMINATION_CHECK #-} to skip
36
the termination check, but must label your definitions as either
37
{-# TERMINATING #-} or {-# NON_TERMINATING #-} instead.
39
Note: {-# OPTION --no-termination-check #-} labels all your
40
definitions as {-# TERMINATING #-}, putting you in the danger zone
41
of a loop in the type checker.
46
* Referring to a local variable shadowed by module opening is now
47
an error. Previous behavior was preferring the local over the
48
imported definitions. [Issue 1266]
50
Note that module parameters are locals as well as variables bound by
51
λ, dependent function type, patterns, and let.
58
test : (A : Set) → let open M in A
60
The last A produces an error, since it could refer to the local
61
variable A or to the definition imported from module M.
63
* `with` on a variable bound by a module telescope or a pattern of a
64
parent function is now forbidden. [Issue 1342]
69
id : (A : Set) → A → A
72
module M (x : Unit) where
79
g | unit = id (∀ u → unit ≡ dx u) ?
81
Even though this code looks right, Agda complains about the type
82
expression `∀ u → unit ≡ dx u`. If you ask Agda what should go
83
there instead, it happily tells you that it wants
84
`∀ u → unit ≡ dx u`. In fact what you do not see and Agda
85
will never show you is that the two expressions actually differ in
86
the invisible first argument to `dx`, which is visible only outside
87
module `M`. What Agda wants is an invisible `unit` after `dx`, but all
88
you can write is an invisible `x` (which is inserted behind the
91
To avoid those kinds of paradoxes, `with` is now outlawed on module
92
parameters. This should ensure that the invisible arguments are
93
always exactly the module parameters.
95
Since a `where` block is desugared as module with pattern variables
96
of the parent clause as module parameters, the same strikes you for
97
uses of `with` on pattern variables of the parent function.
107
g | unit = id ((u : Unit) → unit ≡ dx u) ?
109
The `with` on pattern variable `x` of the parent clause `f x = unit`
115
* Termination check failure is now a proper error.
117
We no longer continue type checking after termination check failures.
118
Use pragmas {-# NON_TERMINATING #-} and {-# NO_TERMINATION_CHECK #-}
119
near the offending definitions if you want to do so.
120
Or switch off the termination checker altogether with
121
{-# OPTIONS --no-termination-check #-} (at your own risk!).
123
* (Since Agda 2.4.2:) Termination checking --without-K restricts
124
structural descent to arguments ending in data types or `Size`.
125
Likewise, guardedness is only tracked when result type is data or
129
data WOne : Set where wrap : FOne → WOne
132
noo : (X : Set) → (WOne ≡ X) → X → ⊥
133
noo .WOne refl (wrap f) = noo FOne iso f
135
`noo` is rejected since at type `X` the structural descent
136
`f < wrap f` is discounted --without-K.
138
data Pandora : Set where
141
loop : (A : Set) → A ≡ Pandora → A
142
loop .Pandora refl = C (♯ (loop ⊥ foo))
144
`loop` is rejected since guardedness is not tracked at type `A`
147
See issues 1023, 1264, 1292.
152
* The termination checker can now recognize simple subterms in dot
155
data Subst : (d : Nat) → Set where
156
c₁ : ∀ {d} → Subst d → Subst d
157
c₂ : ∀ {d₁ d₂} → Subst d₁ → Subst d₂ → Subst (suc d₁ + d₂)
160
comp : ∀ {d₁ d₂} → Subst d₁ → Subst d₂ → Subst (d₁ + d₂)
162
lookup : ∀ d → Nat → Subst d → Set₁
163
lookup d zero (c₁ ρ) = Set
164
lookup d (suc v) (c₁ ρ) = lookup d v ρ
165
lookup .(suc d₁ + d₂) v (c₂ {d₁} {d₂} ρ σ) = lookup (d₁ + d₂) v (comp ρ σ)
167
The dot pattern here is actually normalized, so it is
171
and the corresponding recursive call argument is (d₁ + d₂).
172
In such simple cases, Agda can now recognize that the pattern is
173
constructor applied to call argument, which is valid descent.
175
Note however, that Agda only looks for syntactic equality when
176
identifying subterms, since it is not allowed to normalize terms on
177
the rhs during termination checking.
179
Actually writing the dot pattern has no effect, this works as well,
180
and looks pretty magical... ;-)
182
hidden : ∀{d} → Nat → Subst d → Set₁
183
hidden zero (c₁ ρ) = Set
184
hidden (suc v) (c₁ ρ) = hidden v ρ
185
hidden v (c₂ ρ σ) = hidden v (comp ρ σ)
193
* Fixed the issue of identifiers containing operators being typeset with
194
excessive math spacing.
201
* Issue 836: Fields and constructors can be qualified by the
202
record/data *type* as well as by their record/data module.
203
This now works also for record/data type imported from
204
parametrized modules:
206
module M (_ : Set₁) where
208
record R : Set₁ where
212
open M Set using (R) -- rather than using (module R)
217
------------------------------------------------------------------------
218
-- Release notes for Agda version 2.4.2
219
------------------------------------------------------------------------
221
Important changes since 2.4.0.2:
226
* New option: --with-K.
228
This can be used to override a global --without-K in a file, by
229
adding a pragma {-# OPTIONS --with-K #-}.
231
* New pragma {-# NON_TERMINATING #-}
233
This is a safer version of NO_TERMINATION_CHECK which doesn't treat the
234
affected functions as terminating. This means that NON_TERMINATING functions
235
do not reduce during type checking. They do reduce at run-time and when
236
invoking C-c C-n at top-level (but not in a hole).
241
* Instance search is now more efficient and recursive (see issue 938)
242
(but without termination check yet).
244
A new keyword `instance' has been introduced (in the style of
245
`abstract' and `private') which must now be used for every
246
definition/postulate that has to be taken into account during instance
247
resolution. For example:
249
record RawMonoid (A : Set) : Set where
254
open RawMonoid {{...}}
257
rawMonoidList : {A : Set} -> RawMonoid (List A)
258
rawMonoidList = record { nil = []; _++_ = List._++_ }
260
rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
261
rawMonoidMaybe {A} = record { nil = nothing ; _++_ = catMaybe }
263
catMaybe : Maybe A -> Maybe A -> Maybe A
264
catMaybe nothing mb = mb
265
catMaybe ma nothing = ma
266
catMaybe (just a) (just b) = just (a ++ b)
268
Moreover, each type of an instance must end in (something that reduces
269
to) a named type (e.g. a record, a datatype or a postulate). This
270
allows us to build a simple index structure
272
data/record name --> possible instances
274
that speeds up instance search.
276
Instance search takes into account all local bindings and all global
277
'instance' bindings and the search is recursive. For instance,
280
? : RawMonoid (Maybe (List A))
282
will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to
283
unify the first one, succeeding with the second one
285
? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))
287
and continue with goal
289
?m : RawMonoid (List A)
293
?m = rawMonoidList {A = A}
295
and putting together we have the solution.
297
Be careful that there is no termination check for now, you can easily
298
make Agda loop by declaring the identity function as an instance. But
299
it shouldn’t be possible to make Agda loop by only declaring
300
structurally recursive instances (whatever that means).
304
* Uniqueness of instances is up to definitional equality (see issue 899).
306
* Instances of the following form are allowed:
308
EqSigma : {A : Set} {B : A → Set} {{EqA : Eq A}}
309
{{EqB : {a : A} → Eq (B a)}}
312
When searching recursively for an instance of type
313
`{a : A} → Eq (B a)', a lambda will automatically be introduced and
314
instance search will search for something of type `Eq (B a)' in
315
the context extended by `a : A'. When searching for an instance, the
316
`a' argument does not have to be implicit, but in the definition of
317
EqSigma, instance search will only be able to use EqB if `a' is implicit.
319
* There is no longer any attempt to solve irrelevant metas by instance
322
* Constructors of records and datatypes are automatically added to the
325
* You can now use 'quote' in patterns.
327
For instance, here is a function that unquotes a (closed) natural number
330
unquoteNat : Term → Maybe Nat
331
unquoteNat (con (quote Nat.zero) []) = just zero
332
unquoteNat (con (quote Nat.suc) (arg _ n ∷ [])) = fmap suc (unquoteNat n)
333
unquoteNat _ = nothing
335
* The builtin constructors AGDATERMUNSUPPORTED and AGDASORTUNSUPPORTED are now
336
translated to meta variables when unquoting.
338
* New syntactic sugar 'tactic e' and 'tactic e | e1 | .. | en'.
340
It desugars as follows and makes it less unwieldy to call reflection-based
343
tactic e --> quoteGoal g in unquote (e g)
344
tactic e | e1 | .. | en --> quoteGoal g in unquote (e g) e1 .. en
346
Note that in the second form the tactic function should generate a function
347
from a number of new subgoals to the original goal. The type of e should be
348
Term -> Term in both cases.
350
* New reflection builtins for literals.
352
The Term data type AGDATERM now needs an additional constructor AGDATERMLIT
353
taking a reflected literal defined as follows (with appropriate builtin
354
bindings for the types Nat, Float, etc).
356
data Literal : Set where
358
float : Float → Literal
359
char : Char → Literal
360
string : String → Literal
361
qname : QName → Literal
363
{-# BUILTIN AGDALITERAL Literal #-}
364
{-# BUILTIN AGDALITNAT nat #-}
365
{-# BUILTIN AGDALITFLOAT float #-}
366
{-# BUILTIN AGDALITCHAR char #-}
367
{-# BUILTIN AGDALITSTRING string #-}
368
{-# BUILTIN AGDALITQNAME qname #-}
370
When quoting (quoteGoal or quoteTerm) literals will be mapped to the
371
AGDATERMLIT constructor. Previously natural number literals were quoted
372
to suc/zero application and other literals were quoted to
375
* New reflection builtins for function definitions.
377
AGDAFUNDEF should now map to a data type defined as follows
378
(with {-# BUILTIN QNAME QName #-}
379
{-# BUILTIN ARG Arg #-}
380
{-# BUILTIN AGDATERM Term #-}
381
{-# BUILTIN AGDATYPE Type #-}
382
{-# BUILTIN AGDALITERAL Literal #-}).
384
data Pattern : Set where
385
con : QName → List (Arg Pattern) → Pattern
388
lit : Literal → Pattern
389
proj : QName → Pattern
392
{-# BUILTIN AGDAPATTERN Pattern #-}
393
{-# BUILTIN AGDAPATCON con #-}
394
{-# BUILTIN AGDAPATDOT dot #-}
395
{-# BUILTIN AGDAPATVAR var #-}
396
{-# BUILTIN AGDAPATLIT lit #-}
397
{-# BUILTIN AGDAPATPROJ proj #-}
398
{-# BUILTIN AGDAPATABSURD absurd #-}
400
data Clause : Set where
401
clause : List (Arg Pattern) → Term → Clause
402
absurd-clause : List (Arg Pattern) → Clause
404
{-# BUILTIN AGDACLAUSE Clause #-}
405
{-# BUILTIN AGDACLAUSECLAUSE clause #-}
406
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
408
data FunDef : Set where
409
fun-def : Type → List Clause → FunDef
411
{-# BUILTIN AGDAFUNDEF FunDef #-}
412
{-# BUILTIN AGDAFUNDEFCON fun-def #-}
414
* New reflection builtins for extended (pattern-matching) lambda.
416
The AGDATERM data type has been augmented with a constructor
418
AGDATERMEXTLAM : List AGDACLAUSE → List (ARG AGDATERM) → AGDATERM
420
Absurd lambdas (λ ()) are quoted to extended lambdas with an absurd clause.
422
* Unquoting declarations.
424
You can now define (recursive) functions by reflection using the new
425
unquoteDecl declaration
429
Here e should have type AGDAFUNDEF and evaluate to a closed value. This value
430
is then spliced in as the definition of x. In the body e, x has type QNAME
431
which lets you splice in recursive definitions.
433
Standard modifiers, such as fixity declarations, can be applied to x as
438
Universe levels are now quoted properly instead of being quoted to
439
AGDASORTUNSUPPORTED. Setω still gets an unsupported sort, however.
441
* Module applicants can now be operator applications. Example:
446
module M (b : B) where
448
module N (a : A) = M [ a ]
452
* Minor change in module application semantics. [Issue 892]
454
Previously re-exported functions were not redefined when instantiating a
457
module A where f = ...
458
module B (X : Set) where
462
In this example C.f would be an alias for A.f, so if both A and C were opened
463
f would not be ambiguous. However, this behaviour is not correct when A and B
464
share some module parameters (issue 892). To fix this C now defines its own
465
copy of f (which evaluates to A.f), which means that opening A and C results
471
* Recursive records need to be declared as either inductive or coinductive.
472
'inductive' is no longer default for recursive records.
475
record _×_ (A B : Set) : Set where
481
record Tree (A : Set) : Set where
486
subtrees : List (Tree A)
488
record Stream (A : Set) : Set where
495
If you are using old-style (musical) coinduction, a record may have
496
to be declared as inductive, paradoxically.
498
record Stream (A : Set) : Set where
499
inductive -- YES, THIS IS INTENDED !
505
This is because the ``coinduction'' happens in the use of `∞' and not
506
in the use of `record'.
514
* A new menu option "Display" can be used to display the version of
515
the running Agda process.
520
* New experimental option ``references'' has been added. When specified,
523
\usepackage[references]{agda}
525
a new command called \AgdaRef is provided, which lets you reference
526
previously typeset commands, e.g.:
528
Let us postulate \AgdaRef{apa}.
535
Above ``apa'' will be typeset (highlighted) the same in the text as in
536
the code, provided that the LaTeX output is post-processed using
537
src/data/postprocess-latex.pl, e.g.:
539
cp $(dirname $(dirname $(agda-mode locate)))/postprocess-latex.pl .
540
agda -i. --latex Example.lagda
542
perl ../postprocess-latex.pl Example.tex > Example.processed
543
mv Example.processed Example.tex
546
Mix-fix and unicode should work as expected (unicode requires
547
XeLaTeX/LuaLaTeX), but there are limitations:
549
+ Overloading identifiers should be avoided, if multiples exist
550
\AgdaRef will typeset according to the first it finds.
552
+ Only the current module is used, should you need to reference
553
identifiers in other modules then you need to specify which other
554
module manually, i.e. \AgdaRef[module]{identifier}.
556
------------------------------------------------------------------------
2
557
-- Release notes for Agda 2 version 2.4.0.2
3
558
------------------------------------------------------------------------
added
removed
CHANGELOG
