1
------------------------------------------------------------------------
2
-- Release notes for Agda 2 version 2.4.0.2
3
------------------------------------------------------------------------
5
Important changes since 2.4.0.1:
7
* The Agda input mode now supports alphabetical super and subscripts,
8
in addition to the numerical ones that were already present.
11
* New feature: Interactively split result.
13
Make case (C-c C-c) with no variables given tries to split on the
14
result to introduce projection patterns. The hole needs to be of
15
record type, of course.
17
test : {A B : Set} (a : A) (b : B) → A × B
20
Result-splitting ? will produce the new clauses:
25
If hole is of function type ending in a record type, the necessary
26
pattern variables will be introduced before the split. Thus, the
27
same result can be obtained by starting from:
29
test : {A B : Set} (a : A) (b : B) → A × B
32
* The so far undocumented ETA pragma now throws an error if applied to
33
definitions that are not records.
35
ETA can be used to force eta-equality at recursive record types,
36
for which eta is not enabled automatically by Agda.
37
Here is such an example:
40
data Colist (A : Set) : Set where
42
_∷_ : A → ∞Colist A → Colist A
44
record ∞Colist (A : Set) : Set where
47
field force : Colist A
53
test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)
56
Note: Unsafe use of ETA can make Agda loop, e.g. by triggering
57
infinite eta expansion!
59
* Bugs fixed (see https://code.google.com/p/agda/issues):
74
------------------------------------------------------------------------
75
-- Release notes for Agda 2 version 2.4.0.1
76
------------------------------------------------------------------------
78
Important changes since 2.4.0:
80
* The option --compile-no-main has been renamed to --no-main.
82
* COMPILED_DATA pragmas can now be given for records.
86
------------------------------------------------------------------------
87
-- Release notes for Agda 2 version 2.4.0
88
------------------------------------------------------------------------
90
Important changes since 2.3.2:
92
Installation and Infrastructure
93
===============================
95
* A new module called Agda.Primitive has been introduced. This module
96
is available to all users, even if the standard library is not used.
97
Currently the module contains level primitives and their
98
representation in Haskell when compiling with MAlonzo:
105
lsuc : (ℓ : Level) → Level
106
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level
108
{-# COMPILED_TYPE Level () #-}
109
{-# COMPILED lzero () #-}
110
{-# COMPILED lsuc (\_ -> ()) #-}
111
{-# COMPILED _⊔_ (\_ _ -> ()) #-}
113
{-# BUILTIN LEVEL Level #-}
114
{-# BUILTIN LEVELZERO lzero #-}
115
{-# BUILTIN LEVELSUC lsuc #-}
116
{-# BUILTIN LEVELMAX _⊔_ #-}
118
To bring these declarations into scope you can use a declaration
119
like the following one:
121
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
123
The standard library reexports these primitives (using the names
124
zero and suc instead of lzero and lsuc) from the Level module.
126
Existing developments using universe polymorphism might now trigger
127
the following error message:
129
Duplicate binding for built-in thing LEVEL, previous binding to
130
.Agda.Primitive.Level
132
To fix this problem, please remove the duplicate bindings.
134
Technical details (perhaps relevant to those who build Agda
137
The include path now always contains a directory <DATADIR>/lib/prim,
138
and this directory is supposed to contain a subdirectory Agda
139
containing a file Primitive.agda.
141
The standard location of <DATADIR> is system- and
142
installation-specific. E.g., in a cabal --user installation of
143
Agda-2.3.4 on a standard single-ghc Linux system it would be
144
$HOME/.cabal/share/Agda-2.3.4 or something similar.
146
The location of the <DATADIR> directory can be configured at
147
compile-time using Cabal flags (--datadir and --datasubdir).
148
The location can also be set at run-time, using the Agda_datadir
149
environment variable.
155
* Pragma NO_TERMINATION_CHECK placed within a mutual block is now
156
applied to the whole mutual block (rather than being discarded
157
silently). Adding to the uses 1.-4. outlined in the release notes
160
3a. Skipping an old-style mutual block: Somewhere within 'mutual'
161
block before a type signature or first function clause.
164
{-# NO_TERMINATION_CHECK #-}
171
* New option --no-pattern-matching
173
Disables all forms of pattern matching (for the current file).
174
You can still import files that use pattern matching.
176
* New option -v profile:7
178
Prints some stats on which phases Agda spends how much time.
179
(Number might not be very reliable, due to garbage collection
180
interruptions, and maybe due to laziness of Haskell.)
182
* New option --no-sized-types
184
Option --sized-types is now default.
185
--no-sized-types will turn off an extra (inexpensive) analysis on
186
data types used for subtyping of sized types.
193
* Experimental feature: quoteContext
195
There is a new keyword 'quoteContext' that gives users access to the
196
list of names in the current local context. For instance:
199
open import Data.List
200
open import Reflection
204
foo (suc n) m = quoteContext xs in ?
206
In the remaining goal, the list xs will consist of two names, n and
207
m, corresponding to the two local variables. At the moment it is not
208
possible to access let bound variables -- this feature may be added
211
* Experimental feature: Varying arity.
212
Function clauses may now have different arity, e.g.,
216
Sum (suc n) = ℕ → Sum n
218
sum : (n : ℕ) → ℕ → Sum n
220
sum (suc n) acc m = sum n (m + acc)
226
T false = Bool → Bool
233
This feature is experimental. Yet unsupported:
234
* Varying arity and 'with'.
235
* Compilation of functions with varying arity to Haskell, JS, or Epic.
237
* Experimental feature: copatterns. (Activated with option --copatterns)
239
We can now define a record by explaining what happens if you project
240
the record. For instance:
242
{-# OPTIONS --copatterns #-}
244
record _×_ (A B : Set) : Set where
251
pair : {A B : Set} → A → B → A × B
255
swap : {A B : Set} → A × B → B × A
259
swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
260
fst (swap3 t) = snd (snd t)
261
fst (snd (swap3 t)) = fst (snd t)
262
snd (snd (swap3 t)) = fst t
264
Taking a projection on the left hand side (lhs) is called a
265
projection pattern, applying to a pattern is called an application
266
pattern. (Alternative terms: projection/application copattern.)
268
In the first example, the symbol 'pair', if applied to variable
269
patterns a and b and then projected via fst, reduces to a.
270
'pair' by itself does not reduce.
272
A typical application are coinductive records such as streams:
274
record Stream (A : Set) : Set where
281
repeat : {A : Set} (a : A) -> Stream A
283
tail (repeat a) = repeat a
285
Again, 'repeat a' by itself will not reduce, but you can take
286
a projection (head or tail) and then it will reduce to the
287
respective rhs. This way, we get the lazy reduction behavior
288
necessary to avoid looping corecursive programs.
290
Application patterns do not need to be trivial (i.e., variable
291
patterns), if we mix with projection patterns. E.g., we can have
293
nats : Nat -> Stream Nat
294
head (nats zero) = zero
295
tail (nats zero) = nats zero
296
head (nats (suc x)) = x
297
tail (nats (suc x)) = nats x
299
Here is an example (not involving coinduction) which demostrates
300
records with fields of function type:
304
record State (S A : Set) : Set where
310
-- The Monad type class
312
record Monad (M : Set → Set) : Set1 where
315
return : {A : Set} → A → M A
316
_>>=_ : {A B : Set} → M A → (A → M B) → M B
319
-- State is an instance of Monad
320
-- Demonstrates the interleaving of projection and application patterns
322
stateMonad : {S : Set} → Monad (State S)
323
runState (Monad.return stateMonad a ) s = a , s
324
runState (Monad._>>=_ stateMonad m k) s₀ =
325
let a , s₁ = runState m s₀
328
module MonadLawsForState {S : Set} where
330
open Monad (stateMonad {S})
332
leftId : {A B : Set}(a : A)(k : A → State S B) →
333
(return a >>= k) ≡ k a
336
rightId : {A B : Set}(m : State S A) →
340
assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
341
((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
344
Copatterns are yet experimental and the following does not work:
346
* Copatterns and 'with' clauses.
348
* Compilation of copatterns to Haskell, JS, or Epic.
350
* Projections generated by
352
are not handled properly on lhss yet.
354
* Conversion checking is slower in the presence of copatterns,
355
since stuck definitions of record type do no longer count
356
as neutral, since they can become unstuck by applying a projection.
357
Thus, comparing two neutrals currently requires comparing all
358
they projections, which repeats a lot of work.
360
* Top-level module no longer required.
362
The top-level module can be omitted from an Agda file. The module name is
363
then inferred from the file name by dropping the path and the .agda
364
extension. So, a module defined in /A/B/C.agda would get the name C.
366
You can also suppress only the module name of the top-level module by writing
370
This works also for parameterised modules.
372
* Module parameters are now always hidden arguments in projections.
375
module M (A : Set) where
377
record Prod (B : Set) : Set where
386
Now, the types of fst and snd are
388
fst : {A : Set}{B : Set} → Prod A B → A
389
snd : {A : Set}{B : Set} → Prod A B → B
391
Until 2.3.2, they were
393
fst : (A : Set){B : Set} → Prod A B → A
394
snd : (A : Set){B : Set} → Prod A B → B
396
This change is a step towards symmetry of constructors and projections.
397
(Constructors always took the module parameters as hidden arguments).
399
* Telescoping lets: Local bindings are now accepted in telescopes
400
of modules, function types, and lambda-abstractions.
402
The syntax of telescopes as been extended to support 'let':
404
id : (let ★ = Set) (A : ★) → A → A
407
In particular one can now 'open' modules inside telescopes:
413
module MEndo (let open Star) (A : ★) where
417
Finally a shortcut is provided for opening modules:
419
module N (open Star) (A : ★) (open MEndo A) (f : Endo) where
422
The semantics of the latter is
426
module _ (A : ★) where
428
module N (f : Endo) where
431
The semantics of telescoping lets in function types and lambda
432
abstractions is just expanding them into ordinary lets.
434
* More liberal left-hand sides in lets [Issue 1028]:
436
You can now write left-hand sides with arguments also for let bindings
437
without a type signature. For instance,
439
let f x = suc x in f zero
441
Let bound functions still can't do pattern matching though.
443
* Ambiguous names in patterns are now optimistically resolved in favor
444
of constructors. [Issue 822] In particular, the following succeeds now:
451
postulate [_] : Set → Set
458
* Anonymous where-modules are opened public. [Issue 848]
462
module _ telescope where
466
means the following (not proper Agda code, since you cannot put a
467
module in-between clauses)
470
module _ {arg-telescope} telescope where
486
* Builtin ZERO and SUC have been merged with NATURAL.
488
When binding the NATURAL builtin, ZERO and SUC are bound to the appropriate
489
constructors automatically. This means that instead of writing
491
{-# BUILTIN NATURAL Nat #-}
492
{-# BUILTIN ZERO zero #-}
493
{-# BUILTIN SUC suc #-}
497
{-# BUILTIN NATURAL Nat #-}
499
* Pattern synonym can now have implicit arguments. [Issue 860]
503
pattern tail=_ {x} xs = x ∷ xs
505
len : ∀ {A} → List A → Nat
507
len (tail= xs) = 1 + len xs
509
* Syntax declarations can now have implicit arguments. [Issue 400]
513
id : ∀ {a}{A : Set a} -> A -> A
516
syntax id {A} x = x ∈ A
518
* Minor syntax changes
520
* -} is now parsed as end-comment even if no comment was begun.
521
As a consequence, the following definition gives a parse error
523
f : {A- : Set} -> Set
526
because Agda now sees ID(f) LBRACE ID(A) END-COMMENT, and no
527
longer ID(f) LBRACE ID(A-) RBRACE.
529
The rational is that the previous lexing was to context-sensitive,
530
attempting to comment-out f using {- and -} lead to a parse error.
532
* Fixities (binding strengths) can now be negative numbers as
537
* Postulates are now allowed in mutual blocks. [Issue 977]
539
* Empty where blocks are now allowed. [Issue 947]
541
* Pattern synonyms are now allowed in parameterised modules. [Issue 941]
543
* Empty hiding and renaming lists in module directives are now allowed.
545
* Module directives using, hiding, renaming and public can now appear in
546
arbitrary order. Multiple using/hiding/renaming directives are allowed, but
547
you still cannot have both using and hiding (because that doesn't make
550
Goal and error display
551
======================
553
* The error message "Refuse to construct infinite term" has been
554
removed, instead one gets unsolved meta variables. Reason: the
555
error was thrown over-eagerly. [Issue 795]
557
* If an interactive case split fails with message
559
Since goal is solved, further case distinction is not supported;
560
try `Solve constraints' instead
562
then the associated interaction meta is assigned to a solution.
563
Press C-c C-= (Show constraints) to view the solution and C-c C-s
564
(Solve constraints) to apply it. [Issue 289]
570
* [ issue 376 ] Implemented expansion of bound record variables during meta assignment.
571
Now Agda can solve for metas X that are applied to projected variables, e.g.:
573
X (fst z) (snd z) = z
577
Technically, this is realized by substituting (x , y) for z with fresh
578
bound variables x and y. Here the full code for the examples:
580
record Sigma (A : Set)(B : A -> Set) : Set where
587
test : (A : Set) (B : A -> Set) ->
588
let X : (x : A) (y : B x) -> Sigma A B
590
in (z : Sigma A B) -> X (fst z) (snd z) ≡ z
593
test' : (A : Set) (B : A -> Set) ->
596
in (z : Sigma A B) -> X (fst z) ≡ fst z
599
The fresh bound variables are named fst(z) and snd(z) and can appear
600
in error messages, e.g.:
602
fail : (A : Set) (B : A -> Set) ->
603
let X : A -> Sigma A B
605
in (z : Sigma A B) -> X (fst z) ≡ z
610
Cannot instantiate the metavariable _7 to solution fst(z) , snd(z)
611
since it contains the variable snd(z) which is not in scope of the
612
metavariable or irrelevant in the metavariable but relevant in the
614
when checking that the expression refl has type _7 A B (fst z) ≡ z
616
* Dependent record types and definitions by copatterns require
617
reduction with previous function clauses while checking the
618
current clause. [Issue 907]
620
For a simple example, consider
622
test : ∀ {A} → Σ Nat λ n → Vec A n
626
For the second clause, the lhs and rhs are typed as
628
proj₂ test : Vec A (proj₁ test)
631
In order for these types to match, we have to reduce the lhs type
632
with the first function clause.
634
Note that termination checking comes after type checking, so be
635
careful to avoid non-termination! Otherwise, the type checker
636
might get into an infinite loop.
638
* The implementation of the primitive primTrustMe has changed.
639
It now only reduces to REFL if the two arguments x and y have
640
the same computational normal form. Before, it reduced when
641
x and y were definitionally equal, which included type-directed
642
equality laws such as eta-equality. Yet because reduction is
643
untyped, calling conversion from reduction lead to Agda crashes
646
The amended description of primTrustMe is (cf. release notes for 2.2.6):
648
primTrustMe : {A : Set} {x y : A} → x ≡ y
650
Here _≡_ is the builtin equality (see BUILTIN hooks for equality,
653
If x and y have the same computational normal form, then
654
primTrustMe {x = x} {y = y} reduces to refl.
656
A note on primTrustMe's runtime behavior:
657
The MAlonzo compiler replaces all uses of primTrustMe with the
658
REFL builtin, without any check for definitional equality. Incorrect
659
uses of primTrustMe can potentially lead to segfaults or similar
660
problems of the compiled code.
662
* Implicit patterns of record type are now only eta-expanded if there
663
is a record constructor. [Issues 473, 635]
668
data P : D → Set where
671
record Rc : Set where
675
works : {r : Rc} → P (Rc.f r) → Set
678
This works since the implicit pattern {r} is eta-expanded to
679
{c x} which allows the type of p to reduce to P x and x to be
680
unified with d. The corresponding explicit version is:
682
works' : (r : Rc) → P (Rc.f r) → Set
685
However, if the record constructor is removed, the same example will
691
fails : {r : R} → P (R.f r) → Set
694
-- d != R.f r of type D
695
-- when checking that the pattern p has type P (R.f r)
697
The error is justified since there is no pattern we could write down
698
for r. It would have to look like
702
but anonymous record patterns are not part of the language.
704
* Absurd lambdas at different source locations are no longer
705
different. [Issue 857]
706
In particular, the following code type-checks now:
708
absurd-equality : _≡_ {A = ⊥ → ⊥} (λ()) λ()
709
absurd-equality = refl
711
Which is a good thing!
713
* Printing of named implicit function types.
715
When printing terms in a context with bound variables Agda renames new
716
bindings to avoid clashes with the previously bound names. For instance, if A
717
is in scope, the type (A : Set) → A is printed as (A₁ : Set) → A₁. However,
718
for implicit function types the name of the binding matters, since it can be
719
used when giving implicit arguments.
721
For this situation, the following new syntax has been introduced:
722
{x = y : A} → B is an implicit function type whose bound variable (in scope
723
in B) is y, but where the name of the argument is x for the purposes of
724
giving it explicitly. For instance, with A in scope, the type {A : Set} → A
725
is now printed as {A = A₁ : Set} → A₁.
727
This syntax is only used when printing and is currently not being parsed.
729
* Changed the semantics of --without-K. [Issue 712, Issue 865, Issue 1025]
731
New specification of --without-K:
733
When --without-K is enabled, the unification of indices for pattern matching
734
is restricted in two ways:
736
1. Reflexive equations of the form x == x are no longer solved, instead Agda
737
gives an error when such an equation is encountered.
739
2. When unifying two same-headed constructor forms 'c us' and 'c vs' of type
740
'D pars ixs', the datatype indices ixs (but not the parameters) have to
741
be *self-unifiable*, i.e. unification of ixs with itself should succeed
742
positively. This is a nontrivial requirement because of point 1.
746
* The J rule is accepted.
748
J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
750
∀ {x y} (x≡y : x ≡ y) → P x≡y
753
This definition is accepted since unification of x with y doesn't require
754
deletion or injectivity.
756
* The K rule is rejected.
758
K : {A : Set} (P : {x : A} → x ≡ x → Set) →
759
(∀ x → P (refl {x = x})) →
760
∀ {x} (x≡x : x ≡ x) → P x≡x
763
Definition is rejected with the following error:
765
Cannot eliminate reflexive equation x = x of type A because K has
767
when checking that the pattern refl has type x ≡ x
769
* Symmetry of the new criterion.
771
test₁ : {k l m : ℕ} → k + l ≡ m → ℕ
774
test₂ : {k l m : ℕ} → k ≡ l + m → ℕ
777
Both versions are now accepted (previously only the first one was).
779
* Handling of parameters.
781
cons-injective : {A : Set} (x y : A) → (x ∷ []) ≡ (y ∷ []) → x ≡ y
782
cons-injective x .x refl = refl
784
Parameters are not unified, so they are ignored by the new criterion.
786
* A larger example: antisymmetry of ≤.
788
data _≤_ : ℕ → ℕ → Set where
789
lz : (n : ℕ) → zero ≤ n
790
ls : (m n : ℕ) → m ≤ n → suc m ≤ suc n
792
≤-antisym : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n
793
≤-antisym .zero .zero (lz .zero) (lz .zero) = refl
794
≤-antisym .(suc m) .(suc n) (ls m n p) (ls .n .m q) =
795
cong suc (≤-antisym m n p q)
799
postulate mySpace : Set
800
postulate myPoint : mySpace
802
data Foo : myPoint ≡ myPoint → Set where
805
test : (i : foo ≡ foo) → i ≡ refl
808
When applying injectivity to the equation "foo ≡ foo" of type "Foo refl",
809
it is checked that the index refl of type "myPoint ≡ myPoint" is
810
self-unifiable. The equation "refl ≡ refl" again requires injectivity, so
811
now the index myPoint is checked for self-unifiability, hence the error:
813
Cannot eliminate reflexive equation myPoint = myPoint of type
814
mySpace because K has been disabled.
815
when checking that the pattern refl has type foo ≡ foo
820
* A buggy facility coined "matrix-shaped orders" that supported
821
uncurried functions (which take tuples of arguments instead of one
822
argument after another) has been removed from the termination
825
* Definitions which fail the termination checker are not unfolded any
826
longer to avoid loops or stack overflows in Agda. However, the
827
termination checker for a mutual block is only invoked after
828
type-checking, so there can still be loops if you define a
829
non-terminating function. But termination checking now happens
830
before the other supplementary checks: positivity, polarity,
831
injectivity and projection-likeness.
832
Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
833
Agda treat any function as terminating.
835
* Termination checking of functions defined by 'with' has been improved.
837
Cases which previously required --termination-depth
838
to pass the termination checker (due to use of 'with') no longer
839
need the flag. For example
841
merge : List A → List A → List A
844
merge (x ∷ xs) (y ∷ ys) with x ≤ y
845
merge (x ∷ xs) (y ∷ ys) | false = y ∷ merge (x ∷ xs) ys
846
merge (x ∷ xs) (y ∷ ys) | true = x ∷ merge xs (y ∷ ys)
848
This failed to termination check previously, since the 'with' expands to an
849
auxiliary function merge-aux:
851
merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
852
merge-aux x y xs ys true = x ∷ merge xs (y ∷ ys)
854
This function makes a call to merge in which the size of one of the arguments
855
is increasing. To make this pass the termination checker now inlines the
856
definition of merge-aux before checking, thus effectively termination
857
checking the original source program.
859
As a result of this transformation doing 'with' on a variable no longer
860
preserves termination. For instance, this does not termination check:
867
* The performance of the termination checker has been improved. For
868
higher --termination-depth the improvement is significant.
869
While the default --termination-depth is still 1, checking with
870
higher --termination-depth should now be feasible.
875
* The MAlonzo compiler backend now has support for compiling modules
876
that are not full programs (i.e. don't have a main function). The
877
goal is that you can write part of a program in Agda and the rest in
878
Haskell, and invoke the Agda functions from the Haskell code. The
879
following features were added for this reason:
881
* A new command-line option --compile-no-main: the command
883
agda --compile-no-main Test.agda
885
will compile Test.agda and all its dependencies to Haskell and
886
compile the resulting Haskell files with --make, but (unlike
887
--compile) not tell GHC to treat Test.hs as the main module. This
888
type of compilation can be invoked from emacs by customizing the
889
agda2-backend variable to value MAlonzoNoMain and then calling
890
"C-c C-x C-c" as before.
892
* A new pragma COMPILED_EXPORT was added as part of the MAlonzo FFI.
893
If we have an agda file containing the following:
898
test = someImplementation
900
{-# COMPILED_EXPORT test someHaskellId #-}
902
then test will be compiled to a Haskell function called
903
someHaskellId in module MAlonzo.Code.A.B that can be invoked from
904
other Haskell code. Its type will be translated according to the
905
normal MAlonzo rules.
913
* A new goal command "Helper Function Type" (C-c C-h) has been added.
915
If you write an application of an undefined function in a goal, the Helper
916
Function Type command will print the type that the function needs to have in
917
order for it to fit the goal. The type is also added to the Emacs kill-ring
918
and can be pasted into the buffer using C-y.
920
The application must be of the form "f args" where f is the name of the
921
helper function you want to create. The arguments can use all the normal
922
features like named implicits or instance arguments.
926
Here's a start on a naive reverse on vectors:
928
reverse : ∀ {A n} → Vec A n → Vec A n
930
reverse (x ∷ xs) = {!snoc (reverse xs) x!}
932
Calling C-c C-h in the goal prints
934
snoc : ∀ {A} {n} → Vec A n → A → Vec A (suc n)
936
* A new command "Explain why a particular name is in scope" (C-c C-w) has been
939
This command can be called from a goal or from the top-level and will as the
940
name suggests explain why a particular name is in scope.
942
For each definition or module that the given name can refer to a trace is
943
printed of all open statements and module applications leading back to the
944
original definition of the name.
948
module A (X : Set₁) where
951
module B (Y : Set₁) where
956
Calling C-c C-w on mkFoo at the top-level prints
959
* a constructor Issue207.C._.Foo.mkFoo brought into scope by
960
- the opening of C at Issue207.agda:13,6-7
961
- the application of B at Issue207.agda:11,12-13
962
- the application of A at Issue207.agda:9,8-9
963
- its definition at Issue207.agda:6,5-10
965
This command is useful if Agda complains about an ambiguous name and you need
966
to figure out how to hide the undesired interpretations.
968
* Improvements to the "make case" command (C-c C-c)
970
- One can now also split on hidden variables, using the name
971
(starting with .) with which they are printed.
972
Use C-c C-, to see all variables in context.
974
- Concerning the printing of generated clauses:
976
* Uses named implicit arguments to improve readability.
978
* Picks explicit occurrences over implicit ones when there is a choice of
979
binding site for a variable.
981
* Avoids binding variables in implicit positions by replacing dot patterns
982
that uses them by wildcards (._).
984
* Key bindings for lots of "mathematical" characters (examples: 𝐴𝑨𝒜𝓐𝔄)
985
have been added to the Agda input method.
986
Example: type \MiA\MIA\McA\MCA\MfA to get 𝐴𝑨𝒜𝓐𝔄.
988
Note: \McB does not exist in unicode (as well as others in that style),
989
but the \MC (bold) alphabet is complete.
991
* Key bindings for "blackboard bold" B (𝔹) and 0-9 (𝟘-𝟡) have been added
992
to the Agda input method (\bb and \b[0-9]).
994
* Key bindings for controlling simplification/normalisation:
996
[TODO: Simplification should be explained somewhere.]
998
Commands like "Goal type and context" (C-c C-,) could previously be
999
invoked in two ways. By default the output was normalised, but if a
1000
prefix argument was used (for instance via C-u C-c C-,), then no
1001
explicit normalisation was performed. Now there are three options:
1003
* By default (C-c C-,) the output is simplified.
1005
* If C-u is used exactly once (C-u C-c C-,), then the result is
1006
neither (explicitly) normalised nor simplified.
1008
* If C-u is used twice (C-u C-u C-c C-,), then the result is
1011
[TODO: As part of the release of Agda 2.3.4 the key binding page on
1012
the wiki should be updated.]
1017
* Two new color scheme options were added to agda.sty:
1019
\usepackage[bw]{agda}, which highlights in black and white;
1020
\usepackage[conor]{agda}, which highlights using Conor's colors.
1022
The default (no options passed) is to use the standard colors.
1024
* If agda.sty cannot be found by the latex environment, it is now
1025
copied into the latex output directory ('latex' by default) instead
1026
of the working directory. This means that the commands needed to
1027
produce a PDF now is
1029
agda --latex -i . <file>.lagda
1033
* The LaTeX-backend has been made more tool agnostic, in particular
1034
XeLaTeX and LuaLaTeX should now work. Here is a small example
1035
(test/latex-backend/succeed/UnicodeInput.lagda):
1037
\documentclass{article}
1042
data αβγδεζθικλμνξρστυφχψω : Set₁ where
1049
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
1053
Compiled as follows, it should produce a nice looking PDF (tested with
1056
agda --latex <file>.lagda
1058
xelatex <file>.tex (or lualatex <file>.tex)
1060
If symbols are missing or xelatex/lualatex complains about the font
1061
missing, try setting a different font using:
1063
\setmathfont{<math-font>}
1065
Use the fc-list tool to list available fonts.
1067
* Add experimental support for hyperlinks to identifiers
1069
If the hyperref latex package is loaded before the agda package and
1070
the links option is passed to the agda package, then the agda package
1071
provides a function called \AgdaTarget. Identifiers which have been
1072
declared targets, by the user, will become clickable hyperlinks in the
1073
rest of the document. Here is a small example
1074
(test/latex-backend/succeed/Links.lagda):
1076
\documentclass{article}
1077
\usepackage{hyperref}
1078
\usepackage[links]{agda}
1089
See next page for how to define \AgdaFunction{two} (doesn't turn into a
1090
link because the target hasn't been defined yet). We could do it
1091
manually though; \hyperlink{two}{\AgdaDatatype{two}}.
1099
two = suc (suc zero)
1102
\AgdaInductiveConstructor{zero} is of type
1103
\AgdaDatatype{ℕ}. \AgdaInductiveConstructor{suc} has not been defined to
1104
be a target so it doesn't turn into a link.
1108
Now that the target for \AgdaFunction{two} has been defined the link
1109
works automatically.
1112
data Bool : Set where
1116
The AgdaTarget command takes a list as input, enabling several
1117
targets to be specified as follows:
1119
\AgdaTarget{if, then, else, if\_then\_else\_}
1121
if_then_else_ : {A : Set} → Bool → A → A → A
1122
if true then t else f = t
1123
if false then t else f = f
1128
Mixfix identifier need their underscores escaped:
1129
\AgdaFunction{if\_then\_else\_}.
1133
The boarders around the links can be suppressed using hyperref's
1136
\usepackage[hidelinks]{hyperref}
1138
Note that the current approach to links does not keep track of scoping
1139
or types, and hence overloaded names might create links which point to
1140
the wrong place. Therefore it is recommended to not overload names
1141
when using the links option at the moment, this might get fixed in the
1144
------------------------------------------------------------------------
1145
-- Release notes for Agda 2 version 2.3.2.2
1146
------------------------------------------------------------------------
1148
Important changes since 2.3.2.1:
1150
* Fixed a bug that sometimes made it tricky to use the Emacs mode on
1151
Windows [issue 757].
1153
* Made Agda build with newer versions of some libraries.
1155
* Fixed a bug that caused ambiguous parse error messages [issue 147].
1157
------------------------------------------------------------------------
1158
-- Release notes for Agda 2 version 2.3.2.1
1159
------------------------------------------------------------------------
1161
Important changes since 2.3.2:
1166
* Made it possible to compile Agda with more recent versions of
1167
hashable, QuickCheck and Win32.
1174
* Fixed bug in the termination checker (issue 754).
1176
------------------------------------------------------------------------
1177
-- Release notes for Agda 2 version 2.3.2
1178
------------------------------------------------------------------------
1180
Important changes since 2.3.0:
1185
* The Agda-executable package has been removed.
1187
The executable is now provided as part of the Agda package.
1189
* The Emacs mode no longer depends on haskell-mode or GHCi.
1191
* Compilation of Emacs mode Lisp files.
1193
You can now compile the Emacs mode Lisp files by running "agda-mode
1194
compile". This command is run by "make install".
1196
Compilation can, in some cases, give a noticeable speedup.
1198
WARNING: If you reinstall the Agda mode without recompiling the
1199
Emacs Lisp files, then Emacs may continue using the old, compiled
1205
* The --without-K check now reconstructs constructor parameters.
1207
New specification of --without-K:
1209
If the flag is activated, then Agda only accepts certain
1210
case-splits. If the type of the variable to be split is D pars ixs,
1211
where D is a data (or record) type, pars stands for the parameters,
1212
and ixs the indices, then the following requirements must be
1215
* The indices ixs must be applications of constructors (or literals)
1216
to distinct variables. Constructors are usually not applied to
1217
parameters, but for the purposes of this check constructor
1218
parameters are treated as other arguments.
1220
* These distinct variables must not be free in pars.
1222
* Irrelevant arguments are printed as _ by default now. To turn on
1223
printing of irrelevant arguments, use option
1227
* New: Pragma NO_TERMINATION_CHECK to switch off termination checker
1228
for individual function definitions and mutual blocks.
1230
The pragma must precede a function definition or a mutual block.
1231
Examples (see test/succeed/NoTerminationCheck.agda):
1233
1. Skipping a single definition: before type signature.
1235
{-# NO_TERMINATION_CHECK #-}
1239
2. Skipping a single definition: before first clause.
1242
{-# NO_TERMINATION_CHECK #-}
1245
3. Skipping an old-style mutual block: Before 'mutual' keyword.
1247
{-# NO_TERMINATION_CHECK #-}
1255
4. Skipping a new-style mutual block: Anywhere before a type
1256
signature or first function clause in the block
1262
{-# NO_TERMINATION_CHECK #-}
1265
The pragma cannot be used in --safe mode.
1270
* Let binding record patterns
1272
record _×_ (A B : Set) : Set where
1279
let (x , (y , z)) = t
1282
will now be interpreted as
1289
Note that the type of t needs to be inferable. If you need to provide
1290
a type signature, you can write the following:
1299
A pattern synonym is a declaration that can be used on the left hand
1300
side (when pattern matching) as well as the right hand side (in
1301
expressions). For example:
1304
pattern ss x = suc (suc x)
1311
Pattern synonyms are implemented by substitution on the abstract
1312
syntax, so definitions are scope-checked but not type-checked. They
1313
are particularly useful for universe constructions.
1315
* Qualified mixfix operators
1317
It is now possible to use a qualified mixfix operator by qualifying the first
1318
part of the name. For instance
1320
import Data.Nat as Nat
1321
import Data.Bool as Bool
1323
two = Bool.if true then 1 Nat.+ 1 else 0
1325
* Sections [Issue 735]. Agda now parses anonymous modules as sections:
1327
module _ {a} (A : Set a) where
1329
data List : Set a where
1331
_∷_ : (x : A) (xs : List) → List
1333
module _ {a} {A : Set a} where
1335
_++_ : List A → List A → List A
1337
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
1340
test = (5 ∷ []) ++ (3 ∷ [])
1342
In general, now the syntax
1344
module _ parameters where
1347
is accepted and has the same effect as
1350
module M parameters where
1356
* Instantiating a module in an open import statement [Issue 481]. Now accepted:
1358
open import Path.Module args [using/hiding/renaming (...)]
1360
This only brings the imported identifiers from Path.Module into scope,
1361
not the module itself! Consequently, the following is pointless, and raises
1364
import Path.Module args [using/hiding/renaming (...)]
1366
You can give a private name M to the instantiated module via
1368
import Path.Module args as M [using/hiding/renaming (...)]
1369
open import Path.Module args as M [using/hiding/renaming (...)]
1371
Try to avoid 'as' as part of the arguments. 'as' is not a keyword;
1372
the following can be legal, although slightly obfuscated Agda code:
1374
open import as as as as as as
1376
* Implicit module parameters can be given by name. E.g.
1378
open M {namedArg = bla}
1380
This feature has been introduced in Agda 2.3.0 already.
1382
* Multiple type signatures sharing a same type can now be written as a single
1389
Goal and error display
1390
======================
1392
* Meta-variables that were introduced by hidden argument `arg' are now
1393
printed as _arg_number instead of just _number. [Issue 526]
1395
* Agda expands identifiers in anonymous modules when printing.
1396
Should make some goals nicer to read. [Issue 721]
1398
* When a module identifier is ambiguous, Agda tells you if one
1399
of them is a data type module. [Issues 318, 705]
1404
* Improved coverage checker. The coverage checker splits on
1405
arguments that have constructor or literal pattern, committing
1406
to the left-most split that makes progress.
1407
Consider the lookup function for vectors:
1409
data Fin : Nat → Set where
1410
zero : {n : Nat} → Fin (suc n)
1411
suc : {n : Nat} → Fin n → Fin (suc n)
1413
data Vec (A : Set) : Nat → Set where
1415
_∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
1417
_!!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A
1418
(x ∷ xs) !! zero = x
1419
(x ∷ xs) !! suc i = xs !! i
1421
In Agda up to 2.3.0, this definition is rejected unless we add
1426
This is because the coverage checker committed on splitting
1427
on the vector argument, even though this inevitably lead to
1428
failed coverage, because a case for the empty vector [] is missing.
1430
The improvement to the coverage checker consists on committing
1431
only on splits that have a chance of covering, since all possible
1432
constructor patterns are present. Thus, Agda will now split
1433
first on the Fin argument, since cases for both zero and suc are
1434
present. Then, it can split on the Vec argument, since the
1435
empty vector is already ruled out by instantiating n to a suc _.
1437
* Instance arguments resolution will now consider candidates which
1438
still expect hidden arguments. For example:
1440
record Eq (A : Set) : Set where
1441
field eq : A → A → Bool
1445
eqFin : {n : ℕ} → Eq (Fin n)
1446
eqFin = record { eq = primEqFin }
1449
testFin = eq fin1 fin2
1451
The type-checker will now resolve the instance argument of the eq
1452
function to eqFin {_}. This is only done for hidden arguments, not
1453
instance arguments, so that the instance search stays non-recursive.
1455
* Constraint solving: Upgraded Miller patterns to record patterns. [Issue 456]
1457
Agda now solves meta-variables that are applied to record patterns.
1458
A typical (but here, artificial) case is:
1460
record Sigma (A : Set)(B : A -> Set) : Set where
1466
test : (A : Set)(B : A -> Set) ->
1467
let X : Sigma A B -> Sigma A B
1469
in (x : A)(y : B x) -> X (x , y) ≡ (x , y)
1472
This yields a constraint of the form
1474
_X A B (x , y) := t[x,y]
1476
(with t[x,y] = (x, y)) which is not a Miller pattern.
1477
However, Agda now solves this as
1479
_X A B z := t[fst z,snd z].
1481
* Changed: solving recursive constraints. [Issue 585]
1483
Until 2.3.0, Agda sometimes inferred values that did not pass the
1484
termination checker later, or would even make Agda loop. To prevent this,
1485
the occurs check now also looks into the definitions of the current mutual
1486
block, to avoid constructing recursive solutions. As a consequence, also
1487
terminating recursive solutions are no longer found automatically.
1489
This effects a programming pattern where the recursively computed
1490
type of a recursive function is left to Agda to solve.
1502
This might no longer work from now on.
1503
See examples test/fail/Issue585*.agda
1505
* Less eager introduction of implicit parameters. [Issue 679]
1507
Until Agda 2.3.0, trailing hidden parameters were introduced eagerly
1508
on the left hand side of a definition. For instance, one could not
1511
test : {A : Set} -> Set
1514
because internally, the hidden argument {A : Set} was added to the
1515
left-hand side, yielding
1517
test {_} = \ {A} -> A
1519
which raised a type error. Now, Agda only introduces the trailing
1520
implicit parameters it has to, in order to maintain uniform function
1521
arity. For instance, in
1523
test : Bool -> {A B C : Set} -> Set
1525
test false {B = B} = B
1527
Agda will introduce parameters A and B in all clauses, but not C,
1530
test : Bool -> {A B C : Set} -> Set
1531
test true {A} {_} = A
1532
test false {_} {B = B} = B
1534
Note that for checking where-clauses, still all hidden trailing
1535
parameters are in scope. For instance:
1537
id : {i : Level}{A : Set i} -> A -> A
1539
where myId : forall {A} -> A -> A
1542
To be able to fill in the meta variable _1 in
1544
myId : {A : Set _1} -> A -> A
1546
the hidden parameter {i : Level} needs to be in scope.
1548
As a result of this more lazy introduction of implicit parameters,
1549
the following code now passes.
1551
data Unit : Set where
1555
T unit = {u : Unit} → Unit
1557
test : (u : Unit) → T u
1561
Before, Agda would eagerly introduce the hidden parameter {v} as
1562
unnamed left-hand side parameter, leaving no way to refer to it.
1564
The related issue 655 has also been addressed. It is now possible
1565
to make `synonym' definitions
1569
even when the type of expression begins with a hidden quantifier.
1574
That resulted in unsolved metas until 2.3.0.
1576
* Agda detects unused arguments and ignores them during equality
1577
checking. [Issue 691, solves also issue 44.]
1579
Agda's polarity checker now assigns 'Nonvariant' to arguments
1580
that are not actually used (except for absurd matches). If
1581
f's first argument is Nonvariant, then f x is definitionally equal
1582
to f y regardless of x and y. It is similar to irrelevance, but
1583
does not require user annotation.
1585
For instance, unused module parameters do no longer get in the way:
1587
module M (x : Bool) where
1594
open M false renaming (not to not′)
1596
test : (y : Bool) → not y ≡ not′ y
1599
Matching against record or absurd patterns does not count as `use',
1600
so we get some form of proof irrelevance:
1603
record ⊤ : Set where
1606
data Bool : Set where
1613
fun : (b : Bool) → True b → Bool
1614
fun true trivial = true
1617
test : (b : Bool) → (x y : True b) → fun b x ≡ fun b y
1620
More examples in test/succeed/NonvariantPolarity.agda.
1622
Phantom arguments: Parameters of record and data types are considered
1623
`used' even if they are not actually used. Consider:
1627
False (suc n) = False n
1629
module Invariant where
1630
record Bla (n : Nat)(p : False n) : Set where
1632
module Nonvariant where
1633
Bla : (n : Nat) → False n → Set
1636
Even though record `Bla' does not use its parameters n and p, they
1637
are considered as used, allowing "phantom type" techniques.
1639
In contrast, the arguments of function `Bla' are recognized as unused.
1640
The following code type-checks if we open Invariant but leaves unsolved
1641
metas if we open Nonvariant.
1643
drop-suc : {n : Nat}{p : False n} → Bla (suc n) p → Bla n p
1646
bla : (n : Nat) → {p : False n} → Bla n p → ⊥
1648
bla (suc n) b = bla n (drop-suc b)
1650
If `Bla' is considered invariant, the hidden argument in the recursive
1651
call can be inferred to be `p'. If it is considered non-variant, then
1652
`Bla n X = Bla n p' does not entail `X = p' and the hidden argument
1653
remains unsolved. Since `bla' does not actually use its hidden argument,
1654
its value is not important and it could be searched for.
1655
Unfortunately, polarity analysis of `bla' happens only after type
1656
checking, thus, the information that `bla' is non-variant in `p' is
1657
not available yet when meta-variables are solved.
1658
(See test/fail/BrokenInferenceDueToNonvariantPolarity.agda)
1660
* Agda now expands simple definitions (one clause, terminating)
1661
to check whether a function is constructor headed. [Issue 747]
1662
For instance, the following now also works:
1664
MyPair : Set -> Set -> Set
1665
MyPair A B = Pair A B
1667
Vec : Set -> Nat -> Set
1669
Vec A (suc n) = MyPair A (Vec A n)
1671
Here, Unit and Pair are data or record types.
1676
* -Werror is now overridable.
1678
To enable compilation of Haskell modules containing warnings, the
1679
-Werror flag for the MAlonzo backend has been made overridable. If,
1680
for example, --ghc-flag=-Wwarn is passed when compiling, one can get
1681
away with things like:
1683
data PartialBool : Set where
1686
{-# COMPILED_DATA PartialBool Bool True #-}
1688
The default behavior remains as it used to be and rejects the above
1697
* Asynchronous Emacs mode.
1699
One can now use Emacs while a buffer is type-checked. If the buffer
1700
is edited while the type-checker runs, then syntax highlighting will
1701
not be updated when type-checking is complete.
1703
* Interactive syntax highlighting.
1705
The syntax highlighting is updated while a buffer is type-checked:
1707
• At first the buffer is highlighted in a somewhat crude way
1708
(without go-to-definition information for overloaded
1711
• If the highlighting level is "interactive", then the piece of code
1712
that is currently being type-checked is highlighted as such. (The
1713
default is "non-interactive".)
1715
• When a mutual block has been type-checked it is highlighted
1716
properly (this highlighting includes warnings for potential
1719
The highlighting level can be controlled via the new configuration
1720
variable agda2-highlight-level.
1722
* Multiple case-splits can now be performed in one go.
1724
Consider the following example:
1726
_==_ : Bool → Bool → Bool
1729
If you split on "b₁ b₂", then you get the following code:
1731
_==_ : Bool → Bool → Bool
1733
true == false = {!!}
1734
false == true = {!!}
1735
false == false = {!!}
1737
The order of the variables matters. Consider the following code:
1739
lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
1742
If you split on "xs i", then you get the following code:
1744
lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
1746
lookup (x ∷ xs) zero = {!!}
1747
lookup (x ∷ xs) (suc i) = {!!}
1749
However, if you split on "i xs", then you get the following code
1752
lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
1753
lookup (x ∷ xs) zero = ?
1754
lookup (x ∷ xs) (suc i) = ?
1756
This code is rejected by Agda 2.3.0, but accepted by 2.3.2 thanks
1757
to improved coverage checking (see above).
1759
* The Emacs mode now presents information about which module is
1760
currently being type-checked.
1762
* New global menu entry: Information about the character at point.
1764
If this entry is selected, then information about the character at
1765
point is displayed, including (in many cases) information about how
1766
to type the character.
1768
* Commenting/uncommenting the rest of the buffer.
1770
One can now comment or uncomment the rest of the buffer by typing
1771
C-c C-x M-; or by selecting the menu entry "Comment/uncomment the
1772
rest of the buffer".
1774
* The Emacs mode now uses the Agda executable instead of GHCi.
1776
The *ghci* buffer has been renamed to *agda2*.
1778
A new configuration variable has been introduced:
1779
agda2-program-name, the name of the Agda executable (by default
1782
The variable agda2-ghci-options has been replaced by
1783
agda2-program-args: extra arguments given to the Agda executable (by
1786
If you want to limit Agda's memory consumption you can add some
1787
arguments to agda2-program-args, for instance +RTS -M1.5G -RTS.
1789
* The Emacs mode no longer depends on haskell-mode.
1791
Users who have customised certain haskell-mode variables (such as
1792
haskell-ghci-program-args) may want to update their configuration.
1797
An experimental LaTeX-backend which does precise highlighting a la the
1798
HTML-backend and code alignment a la lhs2TeX has been added.
1800
Here is a sample input literate Agda file:
1802
\documentclass{article}
1808
The following module declaration will be hidden in the output.
1816
Two or more spaces can be used to make the backend align stuff.
1825
suc m + n = suc (m + n)
1830
To produce an output PDF issue the following commands:
1832
agda --latex -i . <file>.lagda
1833
pdflatex latex/<file>.tex
1835
Only the top-most module is processed, like with lhs2tex and unlike with
1836
the HTML-backend. If you want to process imported modules you have to
1837
call agda --latex manually on each of those modules.
1839
There are still issues related to formatting, see the bug tracker for
1842
https://code.google.com/p/agda/issues/detail?id=697
1844
The default agda.sty might therefore change in backwards-incompatible
1845
ways, as work proceeds in trying to resolve those problems.
1848
Implemented features:
1850
* Two or more spaces can be used to force alignment of things, like
1851
with lhs2tex. See example above.
1853
* The highlighting information produced by the type checker is used to
1854
generate the output. For example, the data declaration in the example
1857
\AgdaKeyword{data} \AgdaDatatype{ℕ} \AgdaSymbol{:}
1858
\AgdaPrimitiveType{Set} \AgdaKeyword{where}
1860
These latex commands are defined in agda.sty (which is imported by
1861
\usepackage{agda}) and cause the highlighting.
1863
* The latex-backend checks if agda.sty is found by the latex
1864
environment, if it isn't a default agda.sty is copied from Agda's
1865
data-dir into the working directory (and thus made available to the
1868
If the default agda.sty isn't satisfactory (colors, fonts, spacing,
1869
etc) then the user can modify it and make put it somewhere where the
1870
latex environment can find it. Hopefully most aspects should be
1871
modifiable via agda.sty rather than having to tweak the
1874
* --latex-dir can be used to change the default output directory.
1876
------------------------------------------------------------------------
1877
-- Release notes for Agda 2 version 2.3.0
1878
------------------------------------------------------------------------
1880
Important changes since 2.2.10:
1885
* New more liberal syntax for mutually recursive definitions.
1887
It is no longer necessary to use the 'mutual' keyword to define
1888
mutually recursive functions or datatypes. Instead, it is enough to
1889
declare things before they are used. Instead of
1905
With the new style you have more freedom in choosing the order in
1906
which things are type checked (previously type signatures were
1907
always checked before definitions). Furthermore you can mix
1908
arbitrary declarations, such as modules and postulates, with
1909
mutually recursive definitions.
1911
For data types and records the following new syntax is used to
1912
separate the declaration from the definition:
1915
data Vec (A : Set) : Nat → Set -- Note the absence of 'where'.
1920
_::_ : {n : Nat} → A → Vec A n → Vec A (suc n)
1923
record Sigma (A : Set) (B : A → Set) : Set
1926
record Sigma A B where
1931
When making separated declarations/definitions private or abstract
1932
you should attach the 'private' keyword to the declaration and the
1933
'abstract' keyword to the definition. For instance, a private,
1934
abstract function can be defined as
1941
Finally it may be worth noting that the old style of mutually
1942
recursive definitions is still supported (it basically desugars into
1945
* Pattern matching lambdas.
1947
Anonymous pattern matching functions can be defined using the syntax
1949
\ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }
1951
(where, as usual, \ and -> can be replaced by λ and →). Internally
1952
this is translated into a function definition of the following form:
1954
.extlam p11 .. p1n = e1
1956
.extlam pm1 .. pmn = em
1958
This means that anonymous pattern matching functions are generative.
1959
For instance, refl will not be accepted as an inhabitant of the type
1961
(λ { true → true ; false → false }) ≡
1962
(λ { true → true ; false → false }),
1964
because this is equivalent to extlam1 ≡ extlam2 for some distinct
1965
fresh names extlam1 and extlam2.
1967
Currently the 'where' and 'with' constructions are not allowed in
1968
(the top-level clauses of) anonymous pattern matching functions.
1972
and : Bool → Bool → Bool
1973
and = λ { true x → x ; false _ → false }
1975
xor : Bool → Bool → Bool
1976
xor = λ { true true → false
1977
; false false → false
1981
fst : {A : Set} {B : A → Set} → Σ A B → A
1982
fst = λ { (a , b) → a }
1984
snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
1985
snd = λ { (a , b) → b }
1987
* Record update syntax.
1989
Assume that we have a record type and a corresponding value:
1991
record MyRecord : Set where
1996
old = record { a = 1; b = 2; c = 3 }
1998
Then we can update (some of) the record value's fields in the
2002
new = record old { a = 0; c = 5 }
2004
Here new normalises to record { a = 0; b = 2; c = 5 }. Any
2005
expression yielding a value of type MyRecord can be used instead of
2008
Record updating is not allowed to change types: the resulting value
2009
must have the same type as the original one, including the record
2010
parameters. Thus, the type of a record update can be inferred if the type
2011
of the original record can be inferred.
2013
The record update syntax is expanded before type checking. When the
2016
record old { upd-fields }
2018
is checked against a record type R, it is expanded to
2020
let r = old in record { new-fields },
2022
where old is required to have type R and new-fields is defined as
2023
follows: for each field x in R,
2025
- if x = e is contained in upd-fields then x = e is included in
2026
new-fields, and otherwise
2027
- if x is an explicit field then x = R.x r is included in
2029
- if x is an implicit or instance field, then it is omitted from
2032
(Instance arguments are explained below.) The reason for treating
2033
implicit and instance fields specially is to allow code like the
2036
record R : Set where
2043
xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }
2045
ys = record xs { vec = 0 ∷ [] }
2047
Without the special treatment the last expression would need to
2048
include a new binding for length (for instance "length = _").
2050
* Record patterns which do not contain data type patterns, but which
2051
do contain dot patterns, are no longer rejected.
2053
* When the --without-K flag is used literals are now treated as
2056
* Under-applied functions can now reduce.
2058
Consider the following definition:
2060
id : {A : Set} → A → A
2063
Previously the expression id would not reduce. This has been changed
2064
so that it now reduces to λ x → x. Usually this makes little
2065
difference, but it can be important in conjunction with 'with'. See
2066
issue 365 for an example.
2068
* Unused AgdaLight legacy syntax (x y : A; z v : B) for telescopes has
2071
Universe polymorphism
2072
---------------------
2074
* Universe polymorphism is now enabled by default.
2075
Use --no-universe-polymorphism to disable it.
2077
* Universe levels are no longer defined as a data type.
2079
The basic level combinators can be introduced in the following way:
2085
max : Level → Level → Level
2087
{-# BUILTIN LEVEL Level #-}
2088
{-# BUILTIN LEVELZERO zero #-}
2089
{-# BUILTIN LEVELSUC suc #-}
2090
{-# BUILTIN LEVELMAX max #-}
2092
* The BUILTIN equality is now required to be universe-polymorphic.
2094
* trustMe is now universe-polymorphic.
2096
Meta-variables and unification
2097
------------------------------
2099
* Unsolved meta-variables are now frozen after every mutual block.
2100
This means that they cannot be instantiated by subsequent code. For
2106
bla : one ≡ suc zero
2109
leads to an error now, whereas previously it lead to the
2110
instantiation of _ with "suc zero". If you want to make use of the
2111
old behaviour, put the two definitions in a mutual block.
2113
All meta-variables are unfrozen during interactive editing, so that
2114
the user can fill holes interactively. Note that type-checking of
2115
interactively given terms is not perfect: Agda sometimes refuses to
2116
load a file, even though no complaints were raised during the
2117
interactive construction of the file. This is because certain checks
2118
(for instance, positivity) are only invoked when a file is loaded.
2120
* Record types can now be inferred.
2122
If there is a unique known record type with fields matching the
2123
fields in a record expression, then the type of the expression will
2124
be inferred to be the record type applied to unknown parameters.
2126
If there is no known record type with the given fields the type
2127
checker will give an error instead of producing lots of unsolved
2130
Note that "known record type" refers to any record type in any
2131
imported module, not just types which are in scope.
2133
* The occurrence checker distinguishes rigid and strongly rigid
2134
occurrences [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011].
2136
The completeness checker now accepts the following code:
2138
h : (n : Nat) → n ≡ suc n → Nat
2141
Internally this generates a constraint _n = suc _n where the
2142
meta-variable _n occurs strongly rigidly, i.e. on a constructor path
2143
from the root, in its own defining term tree. This is never
2146
Weakly rigid recursive occurrences may have a solution [Jason Reed's
2147
PhD thesis, page 106]:
2150
let X : (Nat → Nat) → Nat
2153
(f : Nat → Nat) → X f ≡ suc (f (X (λ x → k)))
2156
The constraint _X k f = suc (f (_X k (λ x → k))) has the solution
2157
_X k f = suc (f (suc k)), despite the recursive occurrence of _X.
2158
Here _X is not strongly rigid, because it occurs under the bound
2159
variable f. Previously Agda rejected this code; now it instead
2160
complains about an unsolved meta-variable.
2162
* Equation constraints involving the same meta-variable in the head
2163
now trigger pruning [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA
2166
same : let X : A → A → A → A × A
2168
in {x y z : A} → X x y y ≡ (x , y)
2172
The second equation implies that X cannot depend on its second
2173
argument. After pruning the first equation is linear and can be
2176
* Instance arguments.
2178
A new type of hidden function arguments has been added: instance
2179
arguments. This new feature is based on influences from Scala's
2180
implicits and Agda's existing implicit arguments.
2182
Plain implicit arguments are marked by single braces: {…}. Instance
2183
arguments are instead marked by double braces: {{…}}. Example:
2191
Instead of the double braces you can use the symbols ⦃ and ⦄, but
2192
these symbols must in many cases be surrounded by whitespace. (If
2193
you are using Emacs and the Agda input method, then you can conjure
2194
up the symbols by typing "\{{" and "\}}", respectively.)
2196
Instance arguments behave as ordinary implicit arguments, except for
2197
one important aspect: resolution of arguments which are not provided
2198
explicitly. For instance, consider the following code:
2202
Here Agda will notice that f's instance argument was not provided
2203
explicitly, and try to infer it. All definitions in scope at f's
2204
call site, as well as all variables in the context, are considered.
2205
If exactly one of these names has the required type (A), then the
2206
instance argument will be instantiated to this name.
2208
This feature can be used as an alternative to Haskell type classes.
2211
record Eq (A : Set) : Set where
2212
field equal : A → A → Bool,
2214
then we can define the following projection:
2216
equal : {A : Set} {{eq : Eq A}} → A → A → Bool
2217
equal {{eq}} = Eq.equal eq
2219
Now consider the following expression:
2221
equal false false ∨ equal 3 4
2223
If the following Eq "instances" for Bool and ℕ are in scope, and no
2224
others, then the expression is accepted:
2227
eq-Bool = record { equal = … }
2230
eq-ℕ = record { equal = … }
2232
A shorthand notation is provided to avoid the need to define
2233
projection functions manually:
2235
module Eq-with-implicits = Eq {{...}}
2237
This notation creates a variant of Eq's record module, where the
2238
main Eq argument is an instance argument instead of an explicit one.
2239
It is equivalent to the following definition:
2241
module Eq-with-implicits {A : Set} {{eq : Eq A}} = Eq eq
2243
Note that the short-hand notation allows you to avoid naming the
2244
"-with-implicits" module:
2249
Instance argument resolution is not recursive. As an example,
2250
consider the following "parametrised instance":
2252
eq-List : {A : Set} → Eq A → Eq (List A)
2253
eq-List {A} eq = record { equal = eq-List-A }
2255
eq-List-A : List A → List A → Bool
2256
eq-List-A [] [] = true
2257
eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs
2258
eq-List-A _ _ = false
2260
Assume that the only Eq instances in scope are eq-List and eq-ℕ.
2261
Then the following code does not type-check:
2263
test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
2265
However, we can make the code work by constructing a suitable
2268
test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
2269
where eq-List-ℕ = eq-List eq-ℕ
2271
By restricting the "instance search" to be non-recursive we avoid
2272
introducing a new, compile-time-only evaluation model to Agda.
2274
For more information about instance arguments, see Devriese &
2275
Piessens [ICFP 2011]. Some examples are also available in the
2276
examples/instance-arguments subdirectory of the Agda distribution.
2281
* Dependent irrelevant function types.
2283
Some examples illustrating the syntax of dependent irrelevant
2286
.(x y : A) → B .{x y z : A} → B
2287
∀ x .y → B ∀ x .{y} {z} .v → B
2294
requires that x is irrelevant both in t[x] and in B[x]. This is
2295
possible if, for instance, B[x] = B′ x, with B′ : .A → Set.
2297
Dependent irrelevance allows us to define the eliminator for the
2300
record Squash (A : Set) : Set where
2305
elim-Squash : {A : Set} (P : Squash A → Set)
2306
(ih : .(a : A) → P (squash a)) →
2307
(a⁻ : Squash A) → P a⁻
2308
elim-Squash P ih (squash a) = ih a
2310
Note that this would not type-check with
2311
(ih : (a : A) -> P (squash a)).
2313
* Records with only irrelevant fields.
2315
The following now works:
2317
record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where
2319
.refl : Reflexive _≈_
2320
.sym : Symmetric _≈_
2321
.trans : Transitive _≈_
2323
record Setoid : Set₁ where
2327
_≈_ : Carrier → Carrier → Set
2328
.isEquivalence : IsEquivalence _≈_
2330
open IsEquivalence isEquivalence public
2332
Previously Agda complained about the application
2333
IsEquivalence isEquivalence, because isEquivalence is irrelevant and
2334
the IsEquivalence module expected a relevant argument. Now, when
2335
record modules are generated for records consisting solely of
2336
irrelevant arguments, the record parameter is made irrelevant:
2338
module IsEquivalence {A : Set} {_≈_ : A → A → Set}
2339
.(r : IsEquivalence {A = A} _≈_) where
2342
* Irrelevant things are no longer erased internally. This means that
2343
they are printed as ordinary terms, not as "_" as before.
2345
* The new flag --experimental-irrelevance enables irrelevant universe
2346
levels and matching on irrelevant data when only one constructor is
2347
available. These features are very experimental and likely to change
2353
* The reflection API has been extended to mirror features like
2354
irrelevance, instance arguments and universe polymorphism, and to
2355
give (limited) access to definitions. For completeness all the
2356
builtins and primitives are listed below:
2360
postulate Name : Set
2362
{-# BUILTIN QNAME Name #-}
2365
-- Equality of names.
2366
primQNameEquality : Name → Name → Bool
2368
-- Is the argument visible (explicit), hidden (implicit), or an
2369
-- instance argument?
2371
data Visibility : Set where
2372
visible hidden instance : Visibility
2374
{-# BUILTIN HIDING Visibility #-}
2375
{-# BUILTIN VISIBLE visible #-}
2376
{-# BUILTIN HIDDEN hidden #-}
2377
{-# BUILTIN INSTANCE instance #-}
2379
-- Arguments can be relevant or irrelevant.
2381
data Relevance : Set where
2382
relevant irrelevant : Relevance
2384
{-# BUILTIN RELEVANCE Relevance #-}
2385
{-# BUILTIN RELEVANT relevant #-}
2386
{-# BUILTIN IRRELEVANT irrelevant #-}
2390
data Arg A : Set where
2391
arg : (v : Visibility) (r : Relevance) (x : A) → Arg A
2393
{-# BUILTIN ARG Arg #-}
2394
{-# BUILTIN ARGARG arg #-}
2399
data Term : Set where
2400
-- Variable applied to arguments.
2401
var : (x : ℕ) (args : List (Arg Term)) → Term
2402
-- Constructor applied to arguments.
2403
con : (c : Name) (args : List (Arg Term)) → Term
2404
-- Identifier applied to arguments.
2405
def : (f : Name) (args : List (Arg Term)) → Term
2406
-- Different kinds of λ-abstraction.
2407
lam : (v : Visibility) (t : Term) → Term
2409
pi : (t₁ : Arg Type) (t₂ : Type) → Term
2415
data Type : Set where
2416
el : (s : Sort) (t : Term) → Type
2418
data Sort : Set where
2419
-- A Set of a given (possibly neutral) level.
2420
set : (t : Term) → Sort
2421
-- A Set of a given concrete level.
2422
lit : (n : ℕ) → Sort
2426
{-# BUILTIN AGDASORT Sort #-}
2427
{-# BUILTIN AGDATYPE Type #-}
2428
{-# BUILTIN AGDATERM Term #-}
2429
{-# BUILTIN AGDATERMVAR var #-}
2430
{-# BUILTIN AGDATERMCON con #-}
2431
{-# BUILTIN AGDATERMDEF def #-}
2432
{-# BUILTIN AGDATERMLAM lam #-}
2433
{-# BUILTIN AGDATERMPI pi #-}
2434
{-# BUILTIN AGDATERMSORT sort #-}
2435
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
2436
{-# BUILTIN AGDATYPEEL el #-}
2437
{-# BUILTIN AGDASORTSET set #-}
2438
{-# BUILTIN AGDASORTLIT lit #-}
2439
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
2442
-- Function definition.
2444
-- Data type definition.
2446
-- Record type definition.
2449
{-# BUILTIN AGDAFUNDEF Function #-}
2450
{-# BUILTIN AGDADATADEF Data-type #-}
2451
{-# BUILTIN AGDARECORDDEF Record #-}
2455
data Definition : Set where
2456
function : Function → Definition
2457
data-type : Data-type → Definition
2458
record′ : Record → Definition
2459
constructor′ : Definition
2461
primitive′ : Definition
2463
{-# BUILTIN AGDADEFINITION Definition #-}
2464
{-# BUILTIN AGDADEFINITIONFUNDEF function #-}
2465
{-# BUILTIN AGDADEFINITIONDATADEF data-type #-}
2466
{-# BUILTIN AGDADEFINITIONRECORDDEF record′ #-}
2467
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-}
2468
{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}
2469
{-# BUILTIN AGDADEFINITIONPRIMITIVE primitive′ #-}
2472
-- The type of the thing with the given name.
2473
primQNameType : Name → Type
2474
-- The definition of the thing with the given name.
2475
primQNameDefinition : Name → Definition
2476
-- The constructors of the given data type.
2477
primDataConstructors : Data-type → List Name
2479
As an example the expression
2481
primQNameType (quote zero)
2483
is definitionally equal to
2485
el (lit 0) (def (quote ℕ) [])
2487
(if zero is a constructor of the data type ℕ).
2489
* New keyword: unquote.
2491
The construction "unquote t" converts a representation of an Agda term
2492
to actual Agda code in the following way:
2494
1. The argument t must have type Term (see the reflection API above).
2496
2. The argument is normalised.
2498
3. The entire construction is replaced by the normal form, which is
2499
treated as syntax written by the user and type-checked in the
2504
test : unquote (def (quote ℕ) []) ≡ ℕ
2507
id : (A : Set) → A → A
2508
id = unquote (lam visible (lam visible (var 0 [])))
2510
id-ok : id ≡ (λ A (x : A) → x)
2513
* New keyword: quoteTerm.
2515
The construction "quoteTerm t" is similar to "quote n", but whereas
2516
quote is restricted to names n, quoteTerm accepts terms t. The
2517
construction is handled in the following way:
2519
1. The type of t is inferred. The term t must be type-correct.
2521
2. The term t is normalised.
2523
3. The construction is replaced by the Term representation (see the
2524
reflection API above) of the normal form. Any unsolved metavariables
2525
in the term are represented by the "unknown" term constructor.
2529
test₁ : quoteTerm (λ {A : Set} (x : A) → x) ≡
2530
lam hidden (lam visible (var 0 []))
2533
-- Local variables are represented as de Bruijn indices.
2534
test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])
2537
-- Terms are normalised before being quoted.
2538
test₃ : quoteTerm (0 + 0) ≡ con (quote zero) []
2547
* The MAlonzo backend's FFI now handles universe polymorphism in a
2550
The translation of Agda types and kinds into Haskell now supports
2551
universe-polymorphic postulates. The core changes are that the
2552
translation of function types has been changed from
2554
T[[ Pi (x : A) B ]] =
2555
if A has a Haskell kind then
2556
forall x. () -> T[[ B ]]
2557
else if x in fv B then
2560
T[[ A ]] -> T[[ B ]]
2564
T[[ Pi (x : A) B ]] =
2566
forall x. T[[ A ]] -> T[[ B ]] -- Note: T[[A]] not Unit.
2568
T[[ A ]] -> T[[ B ]],
2570
and that the translation of constants (postulates, constructors and
2571
literals) has been changed from
2574
if COMPILED_TYPE k T then
2582
if COMPILED_TYPE k T then
2584
else if COMPILED k E then
2589
For instance, assuming a Haskell definition
2591
type AgdaIO a b = IO b,
2593
we can set up universe-polymorphic IO in the following way:
2596
IO : ∀ {ℓ} → Set ℓ → Set ℓ
2597
return : ∀ {a} {A : Set a} → A → IO A
2598
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} →
2599
IO A → (A → IO B) → IO B
2601
{-# COMPILED_TYPE IO AgdaIO #-}
2602
{-# COMPILED return (\_ _ -> return) #-}
2603
{-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-}
2605
This is accepted because (assuming that the universe level type is
2606
translated to the Haskell unit type "()")
2609
: forall a. () -> forall b. () -> b -> AgdaIO a b
2610
= T [[ ∀ {a} {A : Set a} → A → IO A ]]
2615
: forall a. () -> forall b. () ->
2616
forall c. () -> forall d. () ->
2617
AgdaIO a c -> (c -> AgdaIO b d) -> AgdaIO b d
2618
= T [[ ∀ {a b} {A : Set a} {B : Set b} →
2619
IO A → (A → IO B) → IO B ]].
2624
* New Epic backend pragma: STATIC.
2626
In the Epic backend, functions marked with the STATIC pragma will be
2627
normalised before compilation. Example usage:
2629
{-# STATIC power #-}
2634
power (suc n) x = power n x * x
2636
Occurrences of "power 4 x" will be replaced by "((x * x) * x) * x".
2638
* Some new optimisations have been implemented in the Epic backend:
2640
- Removal of unused arguments.
2642
A worker/wrapper transformation is performed so that unused
2643
arguments can be removed by Epic's inliner. For instance, the map
2644
function is transformed in the following way:
2646
map_wrap : (A B : Set) → (A → B) → List A → List B
2647
map_wrap A B f xs = map_work f xs
2650
map_work f (x ∷ xs) = f x ∷ map_work f xs
2652
If map_wrap is inlined (which it will be in any saturated call),
2653
then A and B disappear in the generated code.
2655
Unused arguments are found using abstract interpretation. The bodies
2656
of all functions in a module are inspected to decide which variables
2657
are used. The behaviour of postulates is approximated based on their
2658
types. Consider return, for instance:
2660
postulate return : {A : Set} → A → IO A
2662
The first argument of return can be removed, because it is of type
2663
Set and thus cannot affect the outcome of a program at runtime.
2665
- Injection detection.
2667
At runtime many functions may turn out to be inefficient variants of
2668
the identity function. This is especially true after forcing.
2669
Injection detection replaces some of these functions with more
2670
efficient versions. Example:
2672
inject : {n : ℕ} → Fin n → Fin (1 + n)
2673
inject {suc n} zero = zero
2674
inject {suc n} (suc i) = suc (inject {n} i)
2676
Forcing removes the Fin constructors' ℕ arguments, so this function
2677
is an inefficient identity function that can be replaced by the
2682
To actually find this function, we make the induction hypothesis
2683
that inject is an identity function in its second argument and look
2684
at the branches of the function to decide if this holds.
2686
Injection detection also works over data type barriers. Example:
2688
forget : {A : Set} {n : ℕ} → Vec A n → List A
2690
forget (x ∷ xs) = x ∷ forget xs
2692
Given that the constructor tags (in the compiled Epic code) for
2693
Vec.[] and List.[] are the same, and that the tags for Vec._∷_ and
2694
List._∷_ are also the same, this is also an identity function. We
2695
can hence replace the definition with the following one:
2699
To get this to apply as often as possible, constructor tags are
2700
chosen /after/ injection detection has been run, in a way to make as
2701
many functions as possible injections.
2703
Constructor tags are chosen once per source file, so it may be
2704
advantageous to define conversion functions like forget in the same
2705
module as one of the data types. For instance, if Vec.agda imports
2706
List.agda, then the forget function should be put in Vec.agda to
2707
ensure that vectors and lists get the same tags (unless some other
2708
injection function, which puts different constraints on the tags, is
2713
This optimisation finds types whose values are inferable at runtime:
2715
* A data type with only one constructor where all fields are
2716
inferable is itself inferable.
2717
* Set ℓ is inferable (as it has no runtime representation).
2719
A function returning an inferable data type can be smashed, which
2720
means that it is replaced by a function which simply returns the
2723
An important example of an inferable type is the usual propositional
2724
equality type (_≡_). Any function returning a propositional equality
2725
can simply return the reflexivity constructor directly without
2728
This optimisation makes more arguments unused. It also makes the
2729
Epic code size smaller, which in turn speeds up compilation.
2734
* ECMAScript compiler backend.
2736
A new compiler backend is being implemented, targetting ECMAScript
2737
(also known as JavaScript), with the goal of allowing Agda programs
2738
to be run in browsers or other ECMAScript environments.
2740
The backend is still at an experimental stage: the core language is
2741
implemented, but many features are still missing.
2743
The ECMAScript compiler can be invoked from the command line using
2746
agda --js --compile-dir=<DIR> <FILE>.agda
2748
Each source <FILE>.agda is compiled into an ECMAScript target
2749
<DIR>/jAgda.<TOP-LEVEL MODULE NAME>.js. The compiler can also be
2750
invoked using the Emacs mode (the variable agda2-backend controls
2751
which backend is used).
2753
Note that ECMAScript is a strict rather than lazy language. Since
2754
Agda programs are total, this should not impact program semantics,
2755
but it may impact their space or time usage.
2757
ECMAScript does not support algebraic datatypes or pattern-matching.
2758
These features are translated to a use of the visitor pattern. For
2759
instance, the standard library's List data type and null function
2760
are translated into the following code:
2762
exports["List"] = {};
2763
exports["List"]["[]"] = function (x0) {
2766
exports["List"]["_∷_"] = function (x0) {
2767
return function (x1) {
2768
return function (x2) {
2769
return x2["_∷_"](x0, x1);
2774
exports["null"] = function (x0) {
2775
return function (x1) {
2776
return function (x2) {
2779
return jAgda_Data_Bool["Bool"]["true"];
2781
"_∷_": function (x3, x4) {
2782
return jAgda_Data_Bool["Bool"]["false"];
2789
Agda records are translated to ECMAScript objects, preserving field
2792
Top-level Agda modules are translated to ECMAScript modules,
2793
following the common.js module specification. A top-level Agda
2794
module "Foo.Bar" is translated to an ECMAScript module
2797
The ECMAScript compiler does not compile to Haskell, so the pragmas
2798
related to the Haskell FFI (IMPORT, COMPILED_DATA and COMPILED) are
2799
not used by the ECMAScript backend. Instead, there is a COMPILED_JS
2800
pragma which may be applied to any declaration. For postulates,
2801
primitives, functions and values, it gives the ECMAScript code to be
2802
emitted by the compiler. For data types, it gives a function which
2803
is applied to a value of that type, and a visitor object. For
2804
instance, a binding of natural numbers to ECMAScript integers
2805
(ignoring overflow errors) is:
2811
{-# COMPILED_JS ℕ function (x,v) {
2812
if (x < 1) { return v.zero(); } else { return v.suc(x-1); }
2814
{-# COMPILED_JS zero 0 #-}
2815
{-# COMPILED_JS suc function (x) { return x+1; } #-}
2819
suc m + n = suc (m + n)
2821
{-# COMPILED_JS _+_ function (x) { return function (y) {
2825
To allow FFI code to be optimised, the ECMAScript in a COMPILED_JS
2826
declaration is parsed, using a simple parser that recognises a pure
2827
functional subset of ECMAScript, consisting of functions, function
2828
applications, return, if-statements, if-expressions,
2829
side-effect-free binary operators (no precedence, left associative),
2830
side-effect-free prefix operators, objects (where all member names
2831
are quoted), field accesses, and string and integer literals.
2832
Modules may be imported using the require("<module-id>") syntax: any
2833
impure code, or code outside the supported fragment, can be placed
2834
in a module and imported.
2839
* New flag --safe, which can be used to type-check untrusted code.
2841
This flag disables postulates, primTrustMe, and "unsafe" OPTION
2842
pragmas, some of which are known to make Agda inconsistent.
2846
--allow-unsolved-metas
2847
--experimental-irrelevance
2848
--guardedness-preserving-type-construtors
2849
--injective-type-constructors
2851
--no-positivity-check
2852
--no-termination-check
2856
Note that, at the moment, it is not possible to define the universe
2857
level or coinduction primitives when --safe is used (because they
2858
must be introduced as postulates). This can be worked around by
2859
type-checking trusted files in a first pass, without using --safe,
2860
and then using --safe in a second pass. Modules which have already
2861
been type-checked are not re-type-checked just because --safe is
2864
* Dependency graphs.
2866
The new flag --dependency-graph=FILE can be used to generate a DOT
2867
file containing a module dependency graph. The generated file (FILE)
2868
can be rendered using a tool like dot.
2870
* The --no-unreachable-check flag has been removed.
2872
* Projection functions are highlighted as functions instead of as
2873
fields. Field names (in record definitions and record values) are
2874
still highlighted as fields.
2876
* Support for jumping to positions mentioned in the information
2877
buffer has been added.
2879
* The "make install" command no longer installs Agda globally (by
2882
------------------------------------------------------------------------
2883
-- Release notes for Agda 2 version 2.2.10
2884
------------------------------------------------------------------------
2886
Important changes since 2.2.8:
2891
* New flag: --without-K.
2893
This flag makes pattern matching more restricted. If the flag is
2894
activated, then Agda only accepts certain case-splits. If the type
2895
of the variable to be split is D pars ixs, where D is a data (or
2896
record) type, pars stands for the parameters, and ixs the indices,
2897
then the following requirements must be satisfied:
2899
* The indices ixs must be applications of constructors to distinct
2902
* These variables must not be free in pars.
2904
The intended purpose of --without-K is to enable experiments with a
2905
propositional equality without the K rule. Let us define
2906
propositional equality as follows:
2908
data _≡_ {A : Set} : A → A → Set where
2911
Then the obvious implementation of the J rule is accepted:
2913
J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
2914
(∀ x → P (refl x)) →
2915
∀ {x y} (x≡y : x ≡ y) → P x≡y
2916
J P p (refl x) = p x
2918
The same applies to Christine Paulin-Mohring's version of the J rule:
2920
J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) →
2922
∀ {y} (x≡y : x ≡ y) → P x≡y
2925
On the other hand, the obvious implementation of the K rule is not
2928
K : {A : Set} (P : {x : A} → x ≡ x → Set) →
2929
(∀ x → P (refl x)) →
2930
∀ {x} (x≡x : x ≡ x) → P x≡x
2931
K P p (refl x) = p x
2933
However, we have /not/ proved that activation of --without-K ensures
2934
that the K rule cannot be proved in some other way.
2936
* Irrelevant declarations.
2938
Postulates and functions can be marked as irrelevant by prefixing
2939
the name with a dot when the name is declared. Example:
2942
.irrelevant : {A : Set} → .A → A
2944
Irrelevant names may only be used in irrelevant positions or in
2945
definitions of things which have been declared irrelevant.
2947
The axiom irrelevant above can be used to define a projection from
2948
an irrelevant record field:
2950
data Subset (A : Set) (P : A → Set) : Set where
2951
_#_ : (a : A) → .(P a) → Subset A P
2953
elem : ∀ {A P} → Subset A P → A
2956
.certificate : ∀ {A P} (x : Subset A P) → P (elem x)
2957
certificate (a # p) = irrelevant p
2959
The right-hand side of certificate is relevant, so we cannot define
2961
certificate (a # p) = p
2963
(because p is irrelevant). However, certificate is declared to be
2964
irrelevant, so it can use the axiom irrelevant. Furthermore the
2965
first argument of the axiom is irrelevant, which means that
2966
irrelevant p is well-formed.
2968
As shown above the axiom irrelevant justifies irrelevant
2969
projections. Previously no projections were generated for irrelevant
2970
record fields, such as the field certificate in the following
2973
record Subset (A : Set) (P : A → Set) : Set where
2977
.certificate : P elem
2979
Now projections are generated automatically for irrelevant fields
2980
(unless the flag --no-irrelevant-projections is used). Note that
2981
irrelevant projections are highly experimental.
2983
* Termination checker recognises projections.
2985
Projections now preserve sizes, both in patterns and expressions.
2988
record Wrap (A : Set) : Set where
2995
data WNat : Set where
2997
suc : Wrap WNat → WNat
3001
id (suc w) = suc (wrap (id (unwrap w)))
3003
In the structural ordering unwrap w ≤ w. This means that
3005
unwrap w ≤ w < suc w,
3007
and hence the recursive call to id is accepted.
3009
Projections also preserve guardedness.
3014
* Hyperlinks for top-level module names now point to the start of the
3015
module rather than to the declaration of the module name. This
3016
applies both to the Emacs mode and to the output of agda --html.
3018
* Most occurrences of record field names are now highlighted as
3019
"fields". Previously many occurrences were highlighted as
3022
* Emacs mode: It is no longer possible to change the behaviour of the
3023
TAB key by customising agda2-indentation.
3025
* Epic compiler backend.
3027
A new compiler backend is being implemented. This backend makes use
3028
of Edwin Brady's language Epic
3029
(http://www.cs.st-andrews.ac.uk/~eb/epic.php) and its compiler. The
3030
backend should handle most Agda code, but is still at an
3031
experimental stage: more testing is needed, and some things written
3032
below may not be entirely true.
3034
The Epic compiler can be invoked from the command line using the
3037
agda --epic --epic-flag=<EPIC-FLAG> --compile-dir=<DIR> <FILE>.agda
3039
The --epic-flag flag can be given multiple times; each flag is given
3040
verbatim to the Epic compiler (in the given order). The resulting
3041
executable is named after the main module and placed in the
3042
directory specified by the --compile-dir flag (default: the project
3043
root). Intermediate files are placed in a subdirectory called Epic.
3045
The backend requires that there is a definition named main. This
3046
definition should be a value of type IO Unit, but at the moment this
3047
is not checked (so it is easy to produce a program which segfaults).
3048
Currently the backend represents actions of type IO A as functions
3049
from Unit to A, and main is applied to the unit value.
3051
The Epic compiler compiles via C, not Haskell, so the pragmas
3052
related to the Haskell FFI (IMPORT, COMPILED_DATA and COMPILED) are
3053
not used by the Epic backend. Instead there is a new pragma
3054
COMPILED_EPIC. This pragma is used to give Epic code for postulated
3055
definitions (Epic code can in turn call C code). The form of the
3056
pragma is {-# COMPILED_EPIC def code #-}, where def is the name of
3057
an Agda postulate and code is some Epic code which should include
3058
the function arguments, return type and function body. As an example
3059
the IO monad can be defined as follows:
3063
return : ∀ {A} → A → IO A
3064
_>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B
3066
{-# COMPILED_EPIC return (u : Unit, a : Any) -> Any =
3069
_>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -> Any =
3072
Here ioreturn and iobind are Epic functions which are defined in the
3073
file AgdaPrelude.e which is always included.
3075
By default the backend will remove so-called forced constructor
3076
arguments (and case-splitting on forced variables will be
3077
rewritten). This optimisation can be disabled by using the flag
3080
All data types which look like unary natural numbers after forced
3081
constructor arguments have been removed (i.e. types with two
3082
constructors, one nullary and one with a single recursive argument)
3083
will be represented as "BigInts". This applies to the standard Fin
3086
The backend supports Agda's primitive functions and the BUILTIN
3087
pragmas. If the BUILTIN pragmas for unary natural numbers are used,
3088
then some operations, like addition and multiplication, will use
3089
more efficient "BigInt" operations.
3091
If you want to make use of the Epic backend you need to install some
3092
dependencies, see the README.
3094
* The Emacs mode can compile using either the MAlonzo or the Epic
3095
backend. The variable agda2-backend controls which backend is used.
3097
------------------------------------------------------------------------
3098
-- Release notes for Agda 2 version 2.2.8
3099
------------------------------------------------------------------------
3101
Important changes since 2.2.6:
3106
* Record pattern matching.
3108
It is now possible to pattern match on named record constructors.
3111
record Σ (A : Set) (B : A → Set) : Set where
3117
map : {A B : Set} {P : A → Set} {Q : B → Set}
3118
(f : A → B) → (∀ {x} → P x → Q (f x)) →
3120
map f g (x , y) = (f x , g y)
3122
The clause above is internally translated into the following one:
3124
map f g p = (f (Σ.proj₁ p) , g (Σ.proj₂ p))
3126
Record patterns containing data type patterns are not translated.
3131
add (suc m , n) = suc (add (m , n))
3133
Record patterns which do not contain data type patterns, but which
3134
do contain dot patterns, are currently rejected. Example:
3136
Foo : {A : Set} (p₁ p₂ : A × A) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
3137
Foo (x , y) (.x , y′) refl = Set
3139
* Proof irrelevant function types.
3141
Agda now supports irrelevant non-dependent function types:
3145
This type implies that f does not depend computationally on its
3146
argument. One intended use case is data structures with embedded
3147
proofs, like sorted lists:
3154
data SList (bound : ℕ) : Set where
3156
scons : (head : ℕ) →
3158
(tail : SList head) →
3161
The effect of the irrelevant type in the signature of scons is that
3162
scons's second argument is never inspected after Agda has ensured
3163
that it has the right type. It is even thrown away, leading to
3164
smaller term sizes and hopefully some gain in efficiency. The
3165
type-checker ignores irrelevant arguments when checking equality, so
3166
two lists can be equal even if they contain different proofs:
3177
Irrelevant arguments can only be used in irrelevant contexts.
3178
Consider the following subset type:
3180
data Subset (A : Set) (P : A → Set) : Set where
3181
_#_ : (elem : A) → .(P elem) → Subset A P
3183
The following two uses are fine:
3185
elimSubset : ∀ {A C : Set} {P} →
3186
Subset A P → ((a : A) → .(P a) → C) → C
3187
elimSubset (a # p) k = k a p
3189
elem : {A : Set} {P : A → Set} → Subset A P → A
3192
However, if we try to project out the proof component, then Agda
3193
complains that "variable p is declared irrelevant, so it cannot be
3196
prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
3197
prjProof (a # p) = p
3199
Matching against irrelevant arguments is also forbidden, except in
3200
the case of irrefutable matches (record constructor patterns which
3201
have been translated away). For instance, the match against the
3202
pattern (p , q) here is accepted:
3204
elim₂ : ∀ {A C : Set} {P Q : A → Set} →
3205
Subset A (λ x → Σ (P x) (λ _ → Q x)) →
3206
((a : A) → .(P a) → .(Q a) → C) → C
3207
elim₂ (a # (p , q)) k = k a p q
3209
Absurd matches () are also allowed.
3211
Note that record fields can also be irrelevant. Example:
3213
record Subset (A : Set) (P : A → Set) : Set where
3219
Irrelevant fields are never in scope, neither inside nor outside the
3220
record. This means that no record field can depend on an irrelevant
3221
field, and furthermore projections are not defined for such fields.
3222
Irrelevant fields can only be accessed using pattern matching, as in
3225
Irrelevant function types were added very recently, and have not
3226
been subjected to much experimentation yet, so do not be surprised
3227
if something is changed before the next release. For instance,
3228
dependent irrelevant function spaces (.(x : A) → B) might be added
3233
It is now possible to declare user-defined syntax that binds
3234
identifiers. Example:
3237
State : Set → Set → Set
3238
put : ∀ {S} → S → State S ⊤
3239
get : ∀ {S} → State S S
3240
return : ∀ {A S} → A → State S A
3241
bind : ∀ {A B S} → State S B → (B → State S A) → State S A
3243
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
3245
increment : State ℕ ⊤
3246
increment = x ← get ,
3249
The syntax declaration for bind implies that x is in scope in e₂,
3252
You can give fixity declarations along with syntax declarations:
3255
syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂
3257
The fixity applies to the syntax, not the name; syntax declarations
3258
are also restricted to ordinary, non-operator names. The following
3259
declaration is disallowed:
3261
syntax _==_ x y = x === y
3263
Syntax declarations must also be linear; the following declaration
3266
syntax wrong x = x + x
3268
Syntax declarations were added very recently, and have not been
3269
subjected to much experimentation yet, so do not be surprised if
3270
something is changed before the next release.
3272
* Prop has been removed from the language.
3274
The experimental sort Prop has been disabled. Any program using Prop
3275
should typecheck if Prop is replaced by Set₀. Note that Prop is still
3278
* Injective type constructors off by default.
3280
Automatic injectivity of type constructors has been disabled (by
3281
default). To enable it, use the flag --injective-type-constructors,
3282
either on the command line or in an OPTIONS pragma. Note that this
3283
flag makes Agda anti-classical and possibly inconsistent:
3285
Agda with excluded middle is inconsistent
3286
http://thread.gmane.org/gmane.comp.lang.agda/1367
3288
See test/succeed/InjectiveTypeConstructors.agda for an example.
3290
* Termination checker can count.
3292
There is a new flag --termination-depth=N accepting values N >= 1
3293
(with N = 1 being the default) which influences the behavior of the
3294
termination checker. So far, the termination checker has only
3295
distinguished three cases when comparing the argument of a recursive
3296
call with the formal parameter of the callee.
3298
< : the argument is structurally smaller than the parameter
3300
? : the argument is bigger or unrelated to the parameter
3302
This behavior, which is still the default (N = 1), will not
3303
recognise the following functions as terminating.
3310
f (suc (suc n)) = aux n
3317
f --(<)--> aux --(?)--> f
3319
yields a recursive call from f to f via aux where the relation of
3320
call argument to callee parameter is computed as "unrelated"
3321
(composition of < and ?).
3323
Setting N >= 2 allows a finer analysis: n has two constructors less
3324
than suc (suc n), and suc m has one more than m, so we get the call
3327
f --(-2)--> aux --(+1)--> f
3329
The indirect call f --> f is now labeled with (-1), and the
3330
termination checker can recognise that the call argument is
3331
decreasing on this path.
3333
Setting the termination depth to N means that the termination
3334
checker counts decrease up to N and increase up to N-1. The default,
3335
N=1, means that no increase is counted, every increase turns to
3338
In practice, examples like the one above sometimes arise when "with"
3339
is used. As an example, the program
3344
f (suc (suc n)) with zero
3347
is internally represented as
3354
f (suc (suc n)) = aux n zero
3359
Thus, by default, the definition of f using "with" is not accepted
3360
by the termination checker, even though it looks structural (suc n
3361
is a subterm of suc suc n). Now, the termination checker is
3362
satisfied if the option "--termination-depth=2" is used.
3366
- This is an experimental feature, hopefully being replaced by
3367
something smarter in the near future.
3369
- Increasing the termination depth will quickly lead to very long
3370
termination checking times. So, use with care. Setting termination
3371
depth to 100 by habit, just to be on the safe side, is not a good
3374
- Increasing termination depth only makes sense for linear data
3375
types such as ℕ and Size. For other types, increase cannot be
3376
recognised. For instance, consider a similar example with lists.
3378
data List : Set where
3380
cons : ℕ → List → List
3385
f (cons x nil) = nil
3386
f (cons x (cons y ys)) = aux y ys
3388
aux : ℕ → List → List
3389
aux z zs = f (cons z zs)
3391
Here the termination checker compares cons z zs to z and also to
3392
zs. In both cases, the result will be "unrelated", no matter how
3393
high we set the termination depth. This is because when comparing
3394
cons z zs to zs, for instance, z is unrelated to zs, thus,
3395
cons z zs is also unrelated to zs. We cannot say it is just "one
3396
larger" since z could be a very large term. Note that this points
3397
to a weakness of untyped termination checking.
3399
To regain the benefit of increased termination depth, we need to
3400
index our lists by a linear type such as ℕ or Size. With
3401
termination depth 2, the above example is accepted for vectors
3404
* The codata keyword has been removed. To use coinduction, use the
3405
following new builtins: INFINITY, SHARP and FLAT. Example:
3407
{-# OPTIONS --universe-polymorphism #-}
3409
module Coinduction where
3416
∞ : ∀ {a} (A : Set a) → Set a
3417
♯_ : ∀ {a} {A : Set a} → A → ∞ A
3418
♭ : ∀ {a} {A : Set a} → ∞ A → A
3420
{-# BUILTIN INFINITY ∞ #-}
3421
{-# BUILTIN SHARP ♯_ #-}
3422
{-# BUILTIN FLAT ♭ #-}
3424
Note that (non-dependent) pattern matching on SHARP is no longer
3427
Note also that strange things might happen if you try to combine the
3428
pragmas above with COMPILED_TYPE, COMPILED_DATA or COMPILED pragmas,
3429
or if the pragmas do not occur right after the postulates.
3431
The compiler compiles the INFINITY builtin to nothing (more or
3432
less), so that the use of coinduction does not get in the way of FFI
3435
data Colist (A : Set) : Set where
3437
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
3439
{-# COMPILED_DATA Colist [] [] (:) #-}
3443
If the new flag --guardedness-preserving-type-constructors is used,
3444
then type constructors are treated as inductive constructors when we
3445
check productivity (but only in parameters, and only if they are
3446
used strictly positively or not at all). This makes examples such as
3447
the following possible:
3449
data Rec (A : ∞ Set) : Set where
3452
-- Σ cannot be a record type below.
3454
data Σ (A : Set) (B : A → Set) : Set where
3455
_,_ : (x : A) → B x → Σ A B
3457
syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
3459
-- Corecursive definition of the W-type.
3461
W : (A : Set) → (A → Set) → Set
3462
W A B = Rec (♯ (Σ[ x ∶ A ] (B x → W A B)))
3464
syntax W A (λ x → B) = W[ x ∶ A ] B
3466
sup : {A : Set} {B : A → Set} (x : A) (f : B x → W A B) → W A B
3467
sup x f = fold (x , f)
3469
W-rec : {A : Set} {B : A → Set}
3471
(∀ {x} {f : B x → W A B} → (∀ y → P (f y)) → P (sup x f)) →
3473
W-rec P h (fold (x , f)) = h (λ y → W-rec P h (f y))
3475
-- Induction-recursion encoded as corecursion-recursion.
3477
data Label : Set where
3478
′0 ′1 ′2 ′σ ′π ′w : Label
3489
U′ ′σ = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
3490
U′ ′π = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
3491
U′ ′w = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
3497
El (′σ , fold (a , b)) = Σ[ x ∶ El a ] El (b x)
3498
El (′π , fold (a , b)) = (x : El a) → El (b x)
3499
El (′w , fold (a , b)) = W[ x ∶ El a ] El (b x)
3501
U-rec : (P : ∀ u → El u → Set) →
3506
P a x → P (b x) y → P (′σ , fold (a , b)) (x , y)) →
3508
(∀ x → P (b x) (f x)) → P (′π , fold (a , b)) f) →
3510
(∀ y → P (′w , fold (a , b)) (f y)) →
3511
P (′w , fold (a , b)) (sup x f)) →
3512
∀ u (x : El u) → P u x
3513
U-rec P P1 P2t P2f Pσ Pπ Pw = rec
3515
rec : ∀ u (x : El u) → P u x
3518
rec (′2 , _) true = P2t
3519
rec (′2 , _) false = P2f
3520
rec (′σ , fold (a , b)) (x , y) = Pσ (rec _ x) (rec _ y)
3521
rec (′π , fold (a , b)) f = Pπ (λ x → rec _ (f x))
3522
rec (′w , fold (a , b)) (fold (x , f)) = Pw (λ y → rec _ (f y))
3524
The --guardedness-preserving-type-constructors extension is based on
3525
a rather operational understanding of ∞/♯_; it's not yet clear if
3526
this extension is consistent.
3528
* Qualified constructors.
3530
Constructors can now be referred to qualified by their data type.
3533
data Nat : Set where
3537
data Fin : Nat → Set where
3538
zero : ∀ {n} → Fin (suc n)
3539
suc : ∀ {n} → Fin n → Fin (suc n)
3541
you can refer to the constructors unambiguously as Nat.zero,
3542
Nat.suc, Fin.zero, and Fin.suc (Nat and Fin are modules containing
3543
the respective constructors). Example:
3545
inj : (n m : Nat) → Nat.suc n ≡ suc m → n ≡ m
3546
inj .m m refl = refl
3548
Previously you had to write something like
3550
inj : (n m : Nat) → _≡_ {Nat} (suc n) (suc m) → n ≡ m
3552
to make the type checker able to figure out that you wanted the
3553
natural number suc in this case.
3557
There are two new constructs for reflection:
3561
In e the value of x will be a representation of the goal type
3562
(the type expected of the whole expression) as an element in a
3563
datatype of Agda terms (see below). For instance,
3566
example = quoteGoal x in {! at this point x = def (quote ℕ) [] !}
3570
If x is the name of a definition (function, datatype, record, or
3571
a constructor), quote x gives you the representation of x as a
3572
value in the primitive type Name (see below).
3574
Quoted terms use the following BUILTINs and primitives (available
3575
from the standard library module Reflection):
3577
-- The type of Agda names.
3579
postulate Name : Set
3581
{-# BUILTIN QNAME Name #-}
3583
primitive primQNameEquality : Name → Name → Bool
3589
data Arg A : Set where
3590
arg : Explicit? → A → Arg A
3592
{-# BUILTIN ARG Arg #-}
3593
{-# BUILTIN ARGARG arg #-}
3595
-- The type of Agda terms.
3597
data Term : Set where
3598
var : ℕ → List (Arg Term) → Term
3599
con : Name → List (Arg Term) → Term
3600
def : Name → List (Arg Term) → Term
3601
lam : Explicit? → Term → Term
3602
pi : Arg Term → Term → Term
3606
{-# BUILTIN AGDATERM Term #-}
3607
{-# BUILTIN AGDATERMVAR var #-}
3608
{-# BUILTIN AGDATERMCON con #-}
3609
{-# BUILTIN AGDATERMDEF def #-}
3610
{-# BUILTIN AGDATERMLAM lam #-}
3611
{-# BUILTIN AGDATERMPI pi #-}
3612
{-# BUILTIN AGDATERMSORT sort #-}
3613
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
3615
Reflection may be useful when working with internal decision
3616
procedures, such as the standard library's ring solver.
3618
* Minor record definition improvement.
3620
The definition of a record type is now available when type checking
3621
record module definitions. This means that you can define things
3624
record Cat : Set₁ where
3627
_=>_ : Obj → Obj → Set
3630
-- not possible before:
3632
op = record { Obj = Obj; _=>_ = λ A B → B => A }
3637
* The "Goal type and context" command now shows the goal type before
3638
the context, and the context is shown in reverse order. The "Goal
3639
type, context and inferred type" command has been modified in a
3642
* Show module contents command.
3644
Given a module name M the Emacs mode can now display all the
3645
top-level modules and names inside M, along with types for the
3646
names. The command is activated using C-c C-o or the menus.
3650
A command which searches for type inhabitants has been added. The
3651
command is invoked by pressing C-C C-a (or using the goal menu).
3652
There are several flags and parameters, e.g. '-c' which enables
3653
case-splitting in the search. For further information, see the Agda
3656
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto
3658
* HTML generation is now possible for a module with unsolved
3659
meta-variables, provided that the --allow-unsolved-metas flag is
3662
------------------------------------------------------------------------
3663
-- Release notes for Agda 2 version 2.2.6
3664
------------------------------------------------------------------------
3666
Important changes since 2.2.4:
3671
* Universe polymorphism (experimental extension).
3673
To enable universe polymorphism give the flag
3674
--universe-polymorphism on the command line or (recommended) as an
3677
When universe polymorphism is enabled Set takes an argument which is
3678
the universe level. For instance, the type of universe polymorphic
3681
id : {a : Level} {A : Set a} → A → A.
3683
The type Level is isomorphic to the unary natural numbers and should be
3684
specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:
3686
data Level : Set where
3690
{-# BUILTIN LEVEL Level #-}
3691
{-# BUILTIN LEVELZERO zero #-}
3692
{-# BUILTIN LEVELSUC suc #-}
3694
There is an additional BUILTIN LEVELMAX for taking the maximum of two
3697
max : Level → Level → Level
3699
max (suc n) zero = suc n
3700
max (suc n) (suc m) = suc (max n m)
3702
{-# BUILTIN LEVELMAX max #-}
3704
The non-polymorphic universe levels Set, Set₁ and so on are sugar
3705
for Set zero, Set (suc zero), etc.
3707
At present there is no automatic lifting of types from one level to
3708
another. It can still be done (rather clumsily) by defining types
3709
like the following one:
3711
data Lifted {a} (A : Set a) : Set (suc a) where
3714
However, it is likely that automatic lifting is introduced at some
3715
point in the future.
3717
* Multiple constructors, record fields, postulates or primitives can
3718
be declared using a single type signature:
3720
data Bool : Set where
3726
* Record fields can be implicit:
3728
record R : Set₁ where
3735
By default implicit fields are not printed.
3737
* Record constructors can be defined:
3739
record Σ (A : Set) (B : A → Set) : Set where
3745
In this example _,_ gets the type
3747
(proj₁ : A) → B proj₁ → Σ A B.
3749
For implicit fields the corresponding constructor arguments become
3752
Note that the constructor is defined in the /outer/ scope, so any
3753
fixity declaration has to be given outside the record definition.
3754
The constructor is not in scope inside the record module.
3756
Note also that pattern matching for records has not been implemented
3759
* BUILTIN hooks for equality.
3763
data _≡_ {A : Set} (x : A) : A → Set where
3766
can be specified as the builtin equality type using the following
3769
{-# BUILTIN EQUALITY _≡_ #-}
3770
{-# BUILTIN REFL refl #-}
3772
The builtin equality is used for the new rewrite construct and
3773
the primTrustMe primitive described below.
3775
* New rewrite construct.
3777
If eqn : a ≡ b, where _≡_ is the builtin equality (see above) you
3780
f ps rewrite eqn = rhs
3785
... | ._ | refl = rhs
3787
The rewrite construct has the effect of rewriting the goal and the
3788
context by the given equation (left to right).
3790
You can rewrite using several equations (in sequence) by separating
3791
them with vertical bars (|):
3793
f ps rewrite eqn₁ | eqn₂ | … = rhs
3795
It is also possible to add with clauses after rewriting:
3797
f ps rewrite eqns with e
3800
Note that pattern matching happens before rewriting—if you want to
3801
rewrite and then do pattern matching you can use a with after the
3804
See test/succeed/Rewrite.agda for some examples.
3806
* A new primitive, primTrustMe, has been added:
3808
primTrustMe : {A : Set} {x y : A} → x ≡ y
3810
Here _≡_ is the builtin equality (see BUILTIN hooks for equality,
3813
If x and y are definitionally equal, then
3814
primTrustMe {x = x} {y = y} reduces to refl.
3816
Note that the compiler replaces all uses of primTrustMe with the
3817
REFL builtin, without any check for definitional equality. Incorrect
3818
uses of primTrustMe can potentially lead to segfaults or similar
3821
For an example of the use of primTrustMe, see Data.String in version
3822
0.3 of the standard library, where it is used to implement decidable
3823
equality on strings using the primitive boolean equality.
3825
* Changes to the syntax and semantics of IMPORT pragmas, which are
3826
used by the Haskell FFI. Such pragmas must now have the following
3829
{-# IMPORT <module name> #-}
3831
These pragmas are interpreted as /qualified/ imports, so Haskell
3832
names need to be given qualified (unless they come from the Haskell
3835
* The horizontal tab character (U+0009) is no longer treated as white
3838
* Line pragmas are no longer supported.
3840
* The --include-path flag can no longer be used as a pragma.
3842
* The experimental and incomplete support for proof irrelevance has
3848
* New "intro" command in the Emacs mode. When there is a canonical way
3849
of building something of the goal type (for instance, if the goal
3850
type is a pair), the goal can be refined in this way. The command
3851
works for the following goal types:
3853
- A data type where only one of its constructors can be used to
3854
construct an element of the goal type. (For instance, if the
3855
goal is a non-empty vector, a "cons" will be introduced.)
3857
- A record type. A record value will be introduced. Implicit
3858
fields will not be included unless showing of implicit arguments
3861
- A function type. A lambda binding as many variables as possible
3862
will be introduced. The variable names will be chosen from the
3863
goal type if its normal form is a dependent function type,
3864
otherwise they will be variations on "x". Implicit lambdas will
3865
only be inserted if showing of implicit arguments is switched
3868
This command can be invoked by using the refine command (C-c C-r)
3869
when the goal is empty. (The old behaviour of the refine command in
3870
this situation was to ask for an expression using the minibuffer.)
3872
* The Emacs mode displays "Checked" in the mode line if the current
3873
file type checked successfully without any warnings.
3875
* If a file F is loaded, and this file defines the module M, it is an
3876
error if F is not the file which defines M according to the include
3879
Note that the command-line tool and the Emacs mode define the
3880
meaning of relative include paths differently: the command-line tool
3881
interprets them relative to the current working directory, whereas
3882
the Emacs mode interprets them relative to the root directory of the
3883
current project. (As an example, if the module A.B.C is loaded from
3884
the file <some-path>/A/B/C.agda, then the root directory is
3887
* It is an error if there are several files on the include path which
3888
match a given module name.
3890
* Interface files are relocatable. You can move around source trees as
3891
long as the include path is updated in a corresponding way. Note
3892
that a module M may be re-typechecked if its time stamp is strictly
3893
newer than that of the corresponding interface file (M.agdai).
3895
* Type-checking is no longer done when an up-to-date interface exists.
3896
(Previously the initial module was always type-checked.)
3898
* Syntax highlighting files for Emacs (.agda.el) are no longer used.
3899
The --emacs flag has been removed. (Syntax highlighting information
3900
is cached in the interface files.)
3902
* The Agate and Alonzo compilers have been retired. The options
3903
--agate, --alonzo and --malonzo have been removed.
3905
* The default directory for MAlonzo output is the project's root
3906
directory. The --malonzo-dir flag has been renamed to --compile-dir.
3908
* Emacs mode: C-c C-x C-d no longer resets the type checking state.
3909
C-c C-x C-r can be used for a more complete reset. C-c C-x C-s
3910
(which used to reload the syntax highlighting information) has been
3911
removed. C-c C-l can be used instead.
3913
* The Emacs mode used to define some "abbrevs", unless the user
3914
explicitly turned this feature off. The new default is /not/ to add
3915
any abbrevs. The old default can be obtained by customising
3916
agda2-mode-abbrevs-use-defaults (a customisation buffer can be
3917
obtained by typing M-x customize-group agda2 RET after an Agda file
3920
------------------------------------------------------------------------
3921
-- Release notes for Agda 2 version 2.2.4
3922
------------------------------------------------------------------------
3924
Important changes since 2.2.2:
3926
* Change to the semantics of "open import" and "open module". The
3929
open import M <using/hiding/renaming>
3934
open A <using/hiding/renaming>
3938
import A <using/hiding/renaming>
3941
The same translation is used for "open module M = E …". Declarations
3942
involving the keywords as or public are changed in a corresponding
3943
way ("as" always goes with import, and "public" always with open).
3945
This change means that import directives do not affect the qualified
3946
names when open import/module is used. To get the old behaviour you
3947
can use the expanded version above.
3949
* Names opened publicly in parameterised modules no longer inherit the
3950
module parameters. Example:
3955
module B (Y : Set) where
3958
In Agda 2.2.2 B.X has type (Y : Set) → Set, whereas in Agda 2.2.4
3961
* Previously it was not possible to export a given constructor name
3962
through two different "open public" statements in the same module.
3963
This is now possible.
3965
* Unicode subscript digits are now allowed for the hierarchy of
3966
universes (Set₀, Set₁, …): Set₁ is equivalent to Set1.
3968
------------------------------------------------------------------------
3969
-- Release notes for Agda 2 version 2.2.2
3970
------------------------------------------------------------------------
3972
Important changes since 2.2.0:
3977
* The --malonzodir option has been renamed to --malonzo-dir.
3979
* The output of agda --html is by default placed in a directory called
3985
* The Emacs mode is included in the Agda Cabal package, and installed
3986
by cabal install. The recommended way to enable the Emacs mode is to
3987
include the following code in .emacs:
3989
(load-file (let ((coding-system-for-read 'utf-8))
3990
(shell-command-to-string "agda-mode locate")))
3992
------------------------------------------------------------------------
3993
-- Release notes for Agda 2 version 2.2.0
3994
------------------------------------------------------------------------
3996
Important changes since 2.1.2 (which was released 2007-08-16):
4001
* Exhaustive pattern checking. Agda complains if there are missing
4002
clauses in a function definition.
4004
* Coinductive types are supported. This feature is under
4005
development/evaluation, and may change.
4007
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes
4009
* Another experimental feature: Sized types, which can make it easier
4010
to explain why your code is terminating.
4012
* Improved constraint solving for functions with constructor headed
4015
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments
4017
* A simple, well-typed foreign function interface, which allows use of
4018
Haskell functions in Agda code.
4020
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.FFI
4022
* The tokens forall, -> and \ can be written as ∀, → and λ.
4024
* Absurd lambdas: λ () and λ {}.
4026
http://thread.gmane.org/gmane.comp.lang.agda/440
4028
* Record fields whose values can be inferred can be omitted.
4030
* Agda complains if it spots an unreachable clause, or if a pattern
4031
variable "shadows" a hidden constructor of matching type.
4033
http://thread.gmane.org/gmane.comp.lang.agda/720
4038
* Case-split: The user interface can replace a pattern variable with
4039
the corresponding constructor patterns. You get one new left-hand
4040
side for every possible constructor.
4042
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
4044
* The MAlonzo compiler.
4046
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo
4048
* A new Emacs input method, which contains bindings for many Unicode
4049
symbols, is by default activated in the Emacs mode.
4051
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput
4053
* Highlighted, hyperlinked HTML can be generated from Agda source
4056
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.HowToGenerateWebPagesFromSourceCode
4058
* The command-line interactive mode (agda -I) is no longer supported,
4059
but should still work.
4061
http://thread.gmane.org/gmane.comp.lang.agda/245
4063
* Reload times when working on large projects are now considerably
4066
http://thread.gmane.org/gmane.comp.lang.agda/551
4071
* A standard library is under development.
4073
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
4078
* The Agda wiki is better organised. It should be easier for a
4079
newcomer to find relevant information now.
4081
http://wiki.portal.chalmers.se/agda/
4086
* Easy-to-install packages for Windows and Debian/Ubuntu have been
4089
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download
4091
* Agda 2.2.0 is available from Hackage.
4093
http://hackage.haskell.org/
added
removed
CHANGELOG
