<div>I'm happy to announce that Agda version 2.3.0 is now up on Hackage. </div><div>These commands should get you set up with the new version:</div><div><br></div><div>cabal update</div><div>cabal install Agda-executable</div>
<div><br></div><div>It's been a while since the last release so there's a lot of new stuff.</div><div>Check out the release notes below.</div><div><br></div><div>/ Ulf</div><div><br></div><div><div>------------------------------------------------------------------------</div>
<div>-- Release notes for Agda 2 version 2.3.0</div><div>------------------------------------------------------------------------</div><div><br></div><div>Important changes since 2.2.10:</div><div><br></div><div>Language</div>
<div>========</div><div><br></div><div>* New more liberal syntax for mutually recursive definitions.</div><div><br></div><div> It is no longer necessary to use the 'mutual' keyword to define</div><div> mutually recursive functions or datatypes. Instead, it is enough to</div>
<div> declare things before they are used. Instead of</div><div><br></div><div> mutual</div><div> f : A</div><div> f = a[f, g]</div><div><br></div><div> g : B[f]</div><div> g = b[f, g]</div><div><br>
</div><div> you can now write</div><div><br></div><div> f : A</div><div> g : B[f]</div><div> f = a[f, g]</div><div> g = b[f, g].</div><div><br></div><div> With the new style you have more freedom in choosing the order in</div>
<div> which things are type checked (previously type signatures were</div><div> always checked before definitions). Furthermore you can mix</div><div> arbitrary declarations, such as modules and postulates, with</div>
<div>
mutually recursive definitions.</div><div><br></div><div> For data types and records the following new syntax is used to</div><div> separate the declaration from the definition:</div><div><br></div><div> -- Declaration.</div>
<div> data Vec (A : Set) : Nat → Set -- Note the absence of 'where'.</div><div><br></div><div> -- Definition.</div><div> data Vec A where</div><div> [] : Vec A zero</div><div> _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)</div>
<div><br></div><div> -- Declaration.</div><div> record Sigma (A : Set) (B : A → Set) : Set</div><div><br></div><div> -- Definition.</div><div> record Sigma A B where</div><div> constructor _,_</div><div>
field fst : A</div>
<div> snd : B fst</div><div><br></div><div> When making separated declarations/definitions private or abstract</div><div> you should attach the 'private' keyword to the declaration and the</div><div>
'abstract' keyword to the definition. For instance, a private,</div>
<div> abstract function can be defined as</div><div><br></div><div> private</div><div> f : A</div><div> abstract</div><div> f = e</div><div><br></div><div> Finally it may be worth noting that the old style of mutually</div>
<div> recursive definitions is still supported (it basically desugars into</div><div> the new style).</div><div><br></div><div>* Pattern matching lambdas.</div><div><br></div><div> Anonymous pattern matching functions can be defined using the syntax</div>
<div><br></div><div> \ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }</div><div><br></div><div> (where, as usual, \ and -> can be replaced by λ and →). Internally</div><div> this is translated into a function definition of the following form:</div>
<div><br></div><div> .extlam p11 .. p1n = e1</div><div> ...</div><div> .extlam pm1 .. pmn = em</div><div><br></div><div> This means that anonymous pattern matching functions are generative.</div><div> For instance, refl will not be accepted as an inhabitant of the type</div>
<div><br></div><div> (λ { true → true ; false → false }) ≡</div><div> (λ { true → true ; false → false }),</div><div><br></div><div> because this is equivalent to extlam1 ≡ extlam2 for some distinct</div><div> fresh names extlam1 and extlam2.</div>
<div><br></div><div> Currently the 'where' and 'with' constructions are not allowed in</div><div> (the top-level clauses of) anonymous pattern matching functions.</div><div><br></div><div> Examples:</div>
<div><br></div><div> and : Bool → Bool → Bool</div><div> and = λ { true x → x ; false _ → false }</div><div><br></div><div> xor : Bool → Bool → Bool</div><div> xor = λ { true true → false</div><div> ; false false → false</div>
<div> ; _ _ → true</div><div> }</div><div><br></div><div> fst : {A : Set} {B : A → Set} → Σ A B → A</div><div> fst = λ { (a , b) → a }</div><div><br></div><div> snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)</div>
<div> snd = λ { (a , b) → b }</div><div><br></div><div>* Record update syntax.</div><div><br></div><div> Assume that we have a record type and a corresponding value:</div><div><br></div><div> record MyRecord : Set where</div>
<div> field</div><div> a b c : ℕ</div><div><br></div><div> old : MyRecord</div><div> old = record { a = 1; b = 2; c = 3 }</div><div><br></div><div> Then we can update (some of) the record value's fields in the</div>
<div> following way:</div><div><br></div><div> new : MyRecord</div><div> new = record old { a = 0; c = 5 }</div><div><br></div><div> Here new normalises to record { a = 0; b = 2; c = 5 }. Any</div><div> expression yielding a value of type MyRecord can be used instead of</div>
<div> old.</div><div><br></div><div> Record updating is not allowed to change types: the resulting value</div><div> must have the same type as the original one, including the record</div><div> parameters. Thus, the type of a record update can be inferred if the type</div>
<div> of the original record can be inferred.</div><div><br></div><div> The record update syntax is expanded before type checking. When the</div><div> expression</div><div><br></div><div> record old { upd-fields }</div>
<div><br></div><div> is checked against a record type R, it is expanded to</div><div><br></div><div> let r = old in record { new-fields },</div><div><br></div><div> where old is required to have type R and new-fields is defined as</div>
<div> follows: for each field x in R,</div><div><br></div><div> - if x = e is contained in upd-fields then x = e is included in</div><div> new-fields, and otherwise</div><div> - if x is an explicit field then x = R.x r is included in</div>
<div> new-fields, and</div><div> - if x is an implicit or instance field, then it is omitted from</div><div> new-fields.</div><div><br></div><div> (Instance arguments are explained below.) The reason for treating</div>
<div> implicit and instance fields specially is to allow code like the</div><div> following:</div><div><br></div><div> record R : Set where</div><div> field</div><div> {length} : ℕ</div><div> vec : Vec ℕ length</div>
<div> -- More fields…</div><div><br></div><div> xs : R</div><div> xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }</div><div><br></div><div> ys = record xs { vec = 0 ∷ [] }</div><div><br></div><div> Without the special treatment the last expression would need to</div>
<div> include a new binding for length (for instance "length = _").</div><div><br></div><div>* Record patterns which do not contain data type patterns, but which</div><div> do contain dot patterns, are no longer rejected.</div>
<div><br></div><div>* When the --without-K flag is used literals are now treated as</div><div> constructors.</div><div><br></div><div>* Under-applied functions can now reduce.</div><div><br></div><div> Consider the following definition:</div>
<div><br></div><div> id : {A : Set} → A → A</div><div> id x = x</div><div><br></div><div> Previously the expression id would not reduce. This has been changed</div><div> so that it now reduces to λ x → x. Usually this makes little</div>
<div> difference, but it can be important in conjunction with 'with'. See</div><div> issue 365 for an example.</div><div><br></div><div>* Unused AgdaLight legacy syntax (x y : A; z v : B) for telescopes has</div>
<div> been removed.</div><div><br></div><div>Universe polymorphism</div><div>---------------------</div><div><br></div><div>* Universe polymorphism is now enabled by default.</div><div> Use --no-universe-polymorphism to disable it.</div>
<div><br></div><div>* Universe levels are no longer defined as a data type.</div><div><br></div><div> The basic level combinators can be introduced in the following way:</div><div><br></div><div> postulate</div><div> Level : Set</div>
<div> zero : Level</div><div> suc : Level → Level</div><div> max : Level → Level → Level</div><div><br></div><div> {-# BUILTIN LEVEL Level #-}</div><div> {-# BUILTIN LEVELZERO zero #-}</div><div> {-# BUILTIN LEVELSUC suc #-}</div>
<div> {-# BUILTIN LEVELMAX max #-}</div><div><br></div><div>* The BUILTIN equality is now required to be universe-polymorphic.</div><div><br></div><div>* trustMe is now universe-polymorphic.</div><div><br></div><div>
Meta-variables and unification</div>
<div>------------------------------</div><div><br></div><div>* Unsolved meta-variables are now frozen after every mutual block.</div><div> This means that they cannot be instantiated by subsequent code. For</div><div> instance,</div>
<div><br></div><div> one : Nat</div><div> one = _</div><div><br></div><div> bla : one ≡ suc zero</div><div> bla = refl</div><div><br></div><div> leads to an error now, whereas previously it lead to the</div>
<div>
instantiation of _ with "suc zero". If you want to make use of the</div><div> old behaviour, put the two definitions in a mutual block.</div><div><br></div><div> All meta-variables are unfrozen during interactive editing, so that</div>
<div> the user can fill holes interactively. Note that type-checking of</div><div> interactively given terms is not perfect: Agda sometimes refuses to</div><div> load a file, even though no complaints were raised during the</div>
<div> interactive construction of the file. This is because certain checks</div><div> (for instance, positivity) are only invoked when a file is loaded.</div><div><br></div><div>* Record types can now be inferred.</div>
<div><br></div><div> If there is a unique known record type with fields matching the</div><div> fields in a record expression, then the type of the expression will</div><div> be inferred to be the record type applied to unknown parameters.</div>
<div><br></div><div> If there is no known record type with the given fields the type</div><div> checker will give an error instead of producing lots of unsolved</div><div> meta-variables.</div><div><br></div><div> Note that "known record type" refers to any record type in any</div>
<div> imported module, not just types which are in scope.</div><div><br></div><div>* The occurrence checker distinguishes rigid and strongly rigid</div><div> occurrences [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011].</div>
<div><br></div><div> The completeness checker now accepts the following code:</div><div><br></div><div> h : (n : Nat) → n ≡ suc n → Nat</div><div> h n ()</div><div><br></div><div> Internally this generates a constraint _n = suc _n where the</div>
<div> meta-variable _n occurs strongly rigidly, i.e. on a constructor path</div><div> from the root, in its own defining term tree. This is never</div><div> solvable.</div><div><br></div><div> Weakly rigid recursive occurrences may have a solution [Jason Reed's</div>
<div> PhD thesis, page 106]:</div><div><br></div><div> test : (k : Nat) →</div><div> let X : (Nat → Nat) → Nat</div><div> X = _</div><div> in</div><div> (f : Nat → Nat) → X f ≡ suc (f (X (λ x → k)))</div>
<div> test k f = refl</div><div><br></div><div> The constraint _X k f = suc (f (_X k (λ x → k))) has the solution</div><div> _X k f = suc (f (suc k)), despite the recursive occurrence of _X.</div><div> Here _X is not strongly rigid, because it occurs under the bound</div>
<div> variable f. Previously Agda rejected this code; now it instead</div><div> complains about an unsolved meta-variable.</div><div><br></div><div>* Equation constraints involving the same meta-variable in the head</div>
<div> now trigger pruning [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA</div><div> 2011]. Example:</div><div><br></div><div> same : let X : A → A → A → A × A</div><div> X = _</div><div> in {x y z : A} → X x y y ≡ (x , y)</div>
<div> × X x x y ≡ X x y y</div><div> same = refl , refl</div><div><br></div><div> The second equation implies that X cannot depend on its second</div><div> argument. After pruning the first equation is linear and can be</div>
<div> solved.</div><div><br></div><div>* Instance arguments.</div><div><br></div><div> A new type of hidden function arguments has been added: instance</div><div> arguments. This new feature is based on influences from Scala's</div>
<div> implicits and Agda's existing implicit arguments.</div><div><br></div><div> Plain implicit arguments are marked by single braces: {…}. Instance</div><div> arguments are instead marked by double braces: {{…}}. Example:</div>
<div><br></div><div> postulate</div><div> A : Set</div><div> B : A → Set</div><div> a : A</div><div> f : {{a : A}} → B a</div><div><br></div><div> Instead of the double braces you can use the symbols ⦃ and ⦄, but</div>
<div> these symbols must in many cases be surrounded by whitespace. (If</div><div> you are using Emacs and the Agda input method, then you can conjure</div><div> up the symbols by typing "\{{" and "\}}", respectively.)</div>
<div><br></div><div> Instance arguments behave as ordinary implicit arguments, except for</div><div> one important aspect: resolution of arguments which are not provided</div><div> explicitly. For instance, consider the following code:</div>
<div><br></div><div> test = f</div><div><br></div><div> Here Agda will notice that f's instance argument was not provided</div><div> explicitly, and try to infer it. All definitions in scope at f's</div><div>
call site, as well as all variables in the context, are considered.</div><div> If exactly one of these names has the required type (A), then the</div><div> instance argument will be instantiated to this name.</div><div>
<br></div><div> This feature can be used as an alternative to Haskell type classes.</div><div> If we define</div><div><br></div><div> record Eq (A : Set) : Set where</div><div> field equal : A → A → Bool,</div>
<div>
<br></div><div> then we can define the following projection:</div><div><br></div><div> equal : {A : Set} {{eq : Eq A}} → A → A → Bool</div><div> equal {{eq}} = Eq.equal eq</div><div><br></div><div> Now consider the following expression:</div>
<div><br></div><div> equal false false ∨ equal 3 4</div><div><br></div><div> If the following Eq "instances" for Bool and ℕ are in scope, and no</div><div> others, then the expression is accepted:</div><div>
<br></div><div> eq-Bool : Eq Bool</div><div> eq-Bool = record { equal = … }</div><div><br></div><div> eq-ℕ : Eq ℕ</div><div> eq-ℕ = record { equal = … }</div><div><br></div><div> A shorthand notation is provided to avoid the need to define</div>
<div> projection functions manually:</div><div><br></div><div> module Eq-with-implicits = Eq {{...}}</div><div><br></div><div> This notation creates a variant of Eq's record module, where the</div><div> main Eq argument is an instance argument instead of an explicit one.</div>
<div> It is equivalent to the following definition:</div><div><br></div><div> module Eq-with-implicits {A : Set} {{eq : Eq A}} = Eq eq</div><div><br></div><div> Note that the short-hand notation allows you to avoid naming the</div>
<div> "-with-implicits" module:</div><div><br></div><div> open Eq {{...}}</div><div><br></div><div><br></div><div> Instance argument resolution is not recursive. As an example,</div><div> consider the following "parametrised instance":</div>
<div><br></div><div> eq-List : {A : Set} → Eq A → Eq (List A)</div><div> eq-List {A} eq = record { equal = eq-List-A }</div><div> where</div><div> eq-List-A : List A → List A → Bool</div><div> eq-List-A [] [] = true</div>
<div> eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs</div><div> eq-List-A _ _ = false</div><div><br></div><div> Assume that the only Eq instances in scope are eq-List and eq-ℕ.</div><div>
Then the following code does not type-check:</div><div><br></div><div> test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])</div><div><br></div><div> However, we can make the code work by constructing a suitable</div><div> instance manually:</div>
<div><br></div><div> test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])</div><div> where eq-List-ℕ = eq-List eq-ℕ</div><div><br></div><div> By restricting the "instance search" to be non-recursive we avoid</div><div>
introducing a new, compile-time-only evaluation model to Agda.</div><div><br></div><div> For more information about instance arguments, see Devriese &</div><div> Piessens [ICFP 2011]. Some examples are also available in the</div>
<div> examples/instance-arguments subdirectory of the Agda distribution.</div><div><br></div><div>Irrelevance</div><div>-----------</div><div><br></div><div>* Dependent irrelevant function types.</div><div><br></div><div>
Some examples illustrating the syntax of dependent irrelevant</div><div> function types:</div><div><br></div><div> .(x y : A) → B .{x y z : A} → B</div><div> ∀ x .y → B ∀ x .{y} {z} .v → B</div><div><br>
</div><div> The declaration</div><div><br></div><div> f : .(x : A) → B[x]</div><div> f x = t[x]</div><div><br></div><div> requires that x is irrelevant both in t[x] and in B[x]. This is</div><div> possible if, for instance, B[x] = B′ x, with B′ : .A → Set.</div>
<div><br></div><div> Dependent irrelevance allows us to define the eliminator for the</div><div> Squash type:</div><div><br></div><div> record Squash (A : Set) : Set where</div><div> constructor squash</div><div>
field</div><div> .proof : A</div><div><br></div><div> elim-Squash : {A : Set} (P : Squash A → Set)</div><div> (ih : .(a : A) → P (squash a)) →</div><div> (a⁻ : Squash A) → P a⁻</div>
<div> elim-Squash P ih (squash a) = ih a</div><div><br></div><div> Note that this would not type-check with</div><div> (ih : (a : A) -> P (squash a)).</div><div><br></div><div>* Records with only irrelevant fields.</div>
<div><br></div><div> The following now works:</div><div><br></div><div> record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where</div><div> field</div><div> .refl : Reflexive _≈_</div><div> .sym : Symmetric _≈_</div>
<div> .trans : Transitive _≈_</div><div><br></div><div> record Setoid : Set₁ where</div><div> infix 4 _≈_</div><div> field</div><div> Carrier : Set</div><div> _≈_ : Carrier → Carrier → Set</div>
<div> .isEquivalence : IsEquivalence _≈_</div><div><br></div><div> open IsEquivalence isEquivalence public</div><div><br></div><div> Previously Agda complained about the application</div><div> IsEquivalence isEquivalence, because isEquivalence is irrelevant and</div>
<div> the IsEquivalence module expected a relevant argument. Now, when</div><div> record modules are generated for records consisting solely of</div><div> irrelevant arguments, the record parameter is made irrelevant:</div>
<div><br></div><div> module IsEquivalence {A : Set} {_≈_ : A → A → Set}</div><div> .(r : IsEquivalence {A = A} _≈_) where</div><div> …</div><div><br></div><div>* Irrelevant things are no longer erased internally. This means that</div>
<div> they are printed as ordinary terms, not as "_" as before.</div><div><br></div><div>* The new flag --experimental-irrelevance enables irrelevant universe</div><div> levels and matching on irrelevant data when only one constructor is</div>
<div> available. These features are very experimental and likely to change</div><div> or disappear.</div><div><br></div><div>Reflection</div><div>----------</div><div><br></div><div>* The reflection API has been extended to mirror features like</div>
<div> irrelevance, instance arguments and universe polymorphism, and to</div><div> give (limited) access to definitions. For completeness all the</div><div> builtins and primitives are listed below:</div><div><br></div>
<div> -- Names.</div><div><br></div><div> postulate Name : Set</div><div><br></div><div> {-# BUILTIN QNAME Name #-}</div><div><br></div><div> primitive</div><div> -- Equality of names.</div><div> primQNameEquality : Name → Name → Bool</div>
<div><br></div><div> -- Is the argument visible (explicit), hidden (implicit), or an</div><div> -- instance argument?</div><div><br></div><div> data Visibility : Set where</div><div> visible hidden instance : Visibility</div>
<div><br></div><div> {-# BUILTIN HIDING Visibility #-}</div><div> {-# BUILTIN VISIBLE visible #-}</div><div> {-# BUILTIN HIDDEN hidden #-}</div><div> {-# BUILTIN INSTANCE instance #-}</div><div>
<br>
</div><div> -- Arguments can be relevant or irrelevant.</div><div><br></div><div> data Relevance : Set where</div><div> relevant irrelevant : Relevance</div><div><br></div><div> {-# BUILTIN RELEVANCE Relevance #-}</div>
<div> {-# BUILTIN RELEVANT relevant #-}</div><div> {-# BUILTIN IRRELEVANT irrelevant #-}</div><div><br></div><div> -- Arguments.</div><div><br></div><div> data Arg A : Set where</div><div> arg : (v : Visibility) (r : Relevance) (x : A) → Arg A</div>
<div><br></div><div> {-# BUILTIN ARG Arg #-}</div><div> {-# BUILTIN ARGARG arg #-}</div><div><br></div><div> -- Terms.</div><div><br></div><div> mutual</div><div> data Term : Set where</div><div> -- Variable applied to arguments.</div>
<div> var : (x : ℕ) (args : List (Arg Term)) → Term</div><div> -- Constructor applied to arguments.</div><div> con : (c : Name) (args : List (Arg Term)) → Term</div><div> -- Identifier applied to arguments.</div>
<div> def : (f : Name) (args : List (Arg Term)) → Term</div><div> -- Different kinds of λ-abstraction.</div><div> lam : (v : Visibility) (t : Term) → Term</div><div> -- Pi-type.</div><div>
pi : (t₁ : Arg Type) (t₂ : Type) → Term</div><div> -- A sort.</div><div> sort : Sort → Term</div><div> -- Anything else.</div><div> unknown : Term</div><div><br></div><div> data Type : Set where</div>
<div> el : (s : Sort) (t : Term) → Type</div><div><br></div><div> data Sort : Set where</div><div> -- A Set of a given (possibly neutral) level.</div><div> set : (t : Term) → Sort</div><div>
-- A Set of a given concrete level.</div>
<div> lit : (n : ℕ) → Sort</div><div> -- Anything else.</div><div> unknown : Sort</div><div><br></div><div> {-# BUILTIN AGDASORT Sort #-}</div><div> {-# BUILTIN AGDATYPE Type #-}</div>
<div> {-# BUILTIN AGDATERM Term #-}</div><div> {-# BUILTIN AGDATERMVAR var #-}</div><div> {-# BUILTIN AGDATERMCON con #-}</div><div> {-# BUILTIN AGDATERMDEF def #-}</div>
<div> {-# BUILTIN AGDATERMLAM lam #-}</div><div> {-# BUILTIN AGDATERMPI pi #-}</div><div> {-# BUILTIN AGDATERMSORT sort #-}</div><div> {-# BUILTIN AGDATERMUNSUPPORTED unknown #-}</div>
<div> {-# BUILTIN AGDATYPEEL el #-}</div><div> {-# BUILTIN AGDASORTSET set #-}</div><div> {-# BUILTIN AGDASORTLIT lit #-}</div><div> {-# BUILTIN AGDASORTUNSUPPORTED unknown #-}</div>
<div><br></div><div> postulate</div><div> -- Function definition.</div><div> Function : Set</div><div> -- Data type definition.</div><div> Data-type : Set</div><div> -- Record type definition.</div>
<div> Record : Set</div><div><br></div><div> {-# BUILTIN AGDAFUNDEF Function #-}</div><div> {-# BUILTIN AGDADATADEF Data-type #-}</div><div> {-# BUILTIN AGDARECORDDEF Record #-}</div><div><br></div>
<div> -- Definitions.</div><div><br></div><div> data Definition : Set where</div><div> function : Function → Definition</div><div> data-type : Data-type → Definition</div><div> record′ : Record → Definition</div>
<div> constructor′ : Definition</div><div> axiom : Definition</div><div> primitive′ : Definition</div><div><br></div><div> {-# BUILTIN AGDADEFINITION Definition #-}</div><div> {-# BUILTIN AGDADEFINITIONFUNDEF function #-}</div>
<div> {-# BUILTIN AGDADEFINITIONDATADEF data-type #-}</div><div> {-# BUILTIN AGDADEFINITIONRECORDDEF record′ #-}</div><div> {-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-}</div><div>
{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}</div><div> {-# BUILTIN AGDADEFINITIONPRIMITIVE primitive′ #-}</div><div><br></div><div> primitive</div><div> -- The type of the thing with the given name.</div>
<div> primQNameType : Name → Type</div><div> -- The definition of the thing with the given name.</div><div> primQNameDefinition : Name → Definition</div><div> -- The constructors of the given data type.</div>
<div> primDataConstructors : Data-type → List Name</div><div><br></div><div> As an example the expression</div><div><br></div><div> primQNameType (quote zero)</div><div><br></div><div> is definitionally equal to</div>
<div><br></div><div> el (lit 0) (def (quote ℕ) [])</div><div><br></div><div> (if zero is a constructor of the data type ℕ).</div><div><br></div><div>* New keyword: unquote.</div><div><br></div><div> The construction "unquote t" converts a representation of an Agda term</div>
<div> to actual Agda code in the following way:</div><div><br></div><div> 1. The argument t must have type Term (see the reflection API above).</div><div><br></div><div> 2. The argument is normalised.</div><div><br></div>
<div> 3. The entire construction is replaced by the normal form, which is</div><div> treated as syntax written by the user and type-checked in the</div><div> usual way.</div><div><br></div><div> Examples:</div>
<div>
<br></div><div> test : unquote (def (quote ℕ) []) ≡ ℕ</div><div> test = refl</div><div><br></div><div> id : (A : Set) → A → A</div><div> id = unquote (lam visible (lam visible (var 0 [])))</div><div><br></div>
<div> id-ok : id ≡ (λ A (x : A) → x)</div><div> id-ok = refl</div><div><br></div><div>* New keyword: quoteTerm.</div><div><br></div><div> The construction "quoteTerm t" is similar to "quote n", but whereas</div>
<div> quote is restricted to names n, quoteTerm accepts terms t. The</div><div> construction is handled in the following way:</div><div><br></div><div> 1. The type of t is inferred. The term t must be type-correct.</div>
<div><br></div><div> 2. The term t is normalised.</div><div><br></div><div> 3. The construction is replaced by the Term representation (see the</div><div> reflection API above) of the normal form. Any unsolved metavariables</div>
<div> in the term are represented by the "unknown" term constructor.</div><div><br></div><div> Examples:</div><div><br></div><div> test₁ : quoteTerm (λ {A : Set} (x : A) → x) ≡</div><div> lam hidden (lam visible (var 0 []))</div>
<div> test₁ = refl</div><div><br></div><div> -- Local variables are represented as de Bruijn indices.</div><div> test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])</div><div> test₂ = refl</div><div>
<br></div><div> -- Terms are normalised before being quoted.</div><div> test₃ : quoteTerm (0 + 0) ≡ con (quote zero) []</div><div> test₃ = refl</div><div><br></div><div>Compiler backends</div><div>=================</div>
<div><br></div><div>MAlonzo</div><div>-------</div><div><br></div><div>* The MAlonzo backend's FFI now handles universe polymorphism in a</div><div> better way.</div><div><br></div><div> The translation of Agda types and kinds into Haskell now supports</div>
<div> universe-polymorphic postulates. The core changes are that the</div><div> translation of function types has been changed from</div><div><br></div><div> T[[ Pi (x : A) B ]] =</div><div> if A has a Haskell kind then</div>
<div> forall x. () -> T[[ B ]]</div><div> else if x in fv B then</div><div> undef</div><div> else</div><div> T[[ A ]] -> T[[ B ]]</div><div><br></div><div> into</div><div><br></div><div>
T[[ Pi (x : A) B ]] =</div><div> if x in fv B then</div><div> forall x. T[[ A ]] -> T[[ B ]] -- Note: T[[A]] not Unit.</div><div> else</div><div> T[[ A ]] -> T[[ B ]],</div><div><br></div>
<div> and that the translation of constants (postulates, constructors and</div><div> literals) has been changed from</div><div><br></div><div> T[[ k As ]] =</div><div> if COMPILED_TYPE k T then</div><div> T T[[ As ]]</div>
<div> else</div><div> undef</div><div><br></div><div> into</div><div><br></div><div> T[[ k As ]] =</div><div> if COMPILED_TYPE k T then</div><div> T T[[ As ]]</div><div> else if COMPILED k E then</div>
<div> ()</div><div> else</div><div> undef.</div><div><br></div><div> For instance, assuming a Haskell definition</div><div><br></div><div> type AgdaIO a b = IO b,</div><div><br></div><div> we can set up universe-polymorphic IO in the following way:</div>
<div><br></div><div> postulate</div><div> IO : ∀ {ℓ} → Set ℓ → Set ℓ</div><div> return : ∀ {a} {A : Set a} → A → IO A</div><div> _>>=_ : ∀ {a b} {A : Set a} {B : Set b} →</div><div> IO A → (A → IO B) → IO B</div>
<div><br></div><div> {-# COMPILED_TYPE IO AgdaIO #-}</div><div> {-# COMPILED return (\_ _ -> return) #-}</div><div> {-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-}</div><div><br></div>
<div> This is accepted because (assuming that the universe level type is</div><div> translated to the Haskell unit type "()")</div><div><br></div><div> (\_ _ -> return)</div><div> : forall a. () -> forall b. () -> b -> AgdaIO a b</div>
<div> = T [[ ∀ {a} {A : Set a} → A → IO A ]]</div><div><br></div><div> and</div><div><br></div><div> (\_ _ _ _ -> (>>=))</div><div> : forall a. () -> forall b. () -></div><div> forall c. () -> forall d. () -></div>
<div> AgdaIO a c -> (c -> AgdaIO b d) -> AgdaIO b d</div><div> = T [[ ∀ {a b} {A : Set a} {B : Set b} →</div><div> IO A → (A → IO B) → IO B ]].</div><div><br></div><div>Epic</div><div>
----</div><div><br></div><div>* New Epic backend pragma: STATIC.</div><div><br></div><div> In the Epic backend, functions marked with the STATIC pragma will be</div><div> normalised before compilation. Example usage:</div>
<div><br></div><div> {-# STATIC power #-}</div><div><br></div><div> power : ℕ → ℕ → ℕ</div><div> power 0 x = 1</div><div> power 1 x = x</div><div> power (suc n) x = power n x * x</div><div><br>
</div>
<div> Occurrences of "power 4 x" will be replaced by "((x * x) * x) * x".</div><div><br></div><div>* Some new optimisations have been implemented in the Epic backend:</div><div><br></div><div> - Removal of unused arguments.</div>
<div><br></div><div> A worker/wrapper transformation is performed so that unused</div><div> arguments can be removed by Epic's inliner. For instance, the map</div><div> function is transformed in the following way:</div>
<div><br></div><div> map_wrap : (A B : Set) → (A → B) → List A → List B</div><div> map_wrap A B f xs = map_work f xs</div><div><br></div><div> map_work f [] = []</div><div> map_work f (x ∷ xs) = f x ∷ map_work f xs</div>
<div><br></div><div> If map_wrap is inlined (which it will be in any saturated call),</div><div> then A and B disappear in the generated code.</div><div><br></div><div> Unused arguments are found using abstract interpretation. The bodies</div>
<div> of all functions in a module are inspected to decide which variables</div><div> are used. The behaviour of postulates is approximated based on their</div><div> types. Consider return, for instance:</div><div><br>
</div><div> postulate return : {A : Set} → A → IO A</div><div><br></div><div> The first argument of return can be removed, because it is of type</div><div> Set and thus cannot affect the outcome of a program at runtime.</div>
<div><br></div><div> - Injection detection.</div><div><br></div><div> At runtime many functions may turn out to be inefficient variants of</div><div> the identity function. This is especially true after forcing.</div>
<div>
Injection detection replaces some of these functions with more</div><div> efficient versions. Example:</div><div><br></div><div> inject : {n : ℕ} → Fin n → Fin (1 + n)</div><div> inject {suc n} zero = zero</div>
<div> inject {suc n} (suc i) = suc (inject {n} i)</div><div><br></div><div> Forcing removes the Fin constructors' ℕ arguments, so this function</div><div> is an inefficient identity function that can be replaced by the</div>
<div> following one:</div><div><br></div><div> inject {_} x = x</div><div><br></div><div> To actually find this function, we make the induction hypothesis</div><div> that inject is an identity function in its second argument and look</div>
<div> at the branches of the function to decide if this holds.</div><div><br></div><div> Injection detection also works over data type barriers. Example:</div><div><br></div><div> forget : {A : Set} {n : ℕ} → Vec A n → List A</div>
<div> forget [] = []</div><div> forget (x ∷ xs) = x ∷ forget xs</div><div><br></div><div> Given that the constructor tags (in the compiled Epic code) for</div><div> Vec.[] and List.[] are the same, and that the tags for Vec._∷_ and</div>
<div> List._∷_ are also the same, this is also an identity function. We</div><div> can hence replace the definition with the following one:</div><div><br></div><div> forget {_} xs = xs</div><div><br></div><div> To get this to apply as often as possible, constructor tags are</div>
<div> chosen /after/ injection detection has been run, in a way to make as</div><div> many functions as possible injections.</div><div><br></div><div> Constructor tags are chosen once per source file, so it may be</div>
<div> advantageous to define conversion functions like forget in the same</div><div> module as one of the data types. For instance, if Vec.agda imports</div><div> List.agda, then the forget function should be put in Vec.agda to</div>
<div> ensure that vectors and lists get the same tags (unless some other</div><div> injection function, which puts different constraints on the tags, is</div><div> prioritised).</div><div><br></div><div> - Smashing.</div>
<div><br></div><div> This optimisation finds types whose values are inferable at runtime:</div><div><br></div><div> * A data type with only one constructor where all fields are</div><div> inferable is itself inferable.</div>
<div> * Set ℓ is inferable (as it has no runtime representation).</div><div><br></div><div> A function returning an inferable data type can be smashed, which</div><div> means that it is replaced by a function which simply returns the</div>
<div> inferred value.</div><div><br></div><div> An important example of an inferable type is the usual propositional</div><div> equality type (_≡_). Any function returning a propositional equality</div><div> can simply return the reflexivity constructor directly without</div>
<div> computing anything.</div><div><br></div><div> This optimisation makes more arguments unused. It also makes the</div><div> Epic code size smaller, which in turn speeds up compilation.</div><div><br></div><div>JavaScript</div>
<div>----------</div><div><br></div><div>* ECMAScript compiler backend.</div><div><br></div><div> A new compiler backend is being implemented, targetting ECMAScript</div><div> (also known as JavaScript), with the goal of allowing Agda programs</div>
<div> to be run in browsers or other ECMAScript environments.</div><div><br></div><div> The backend is still at an experimental stage: the core language is</div><div> implemented, but many features are still missing.</div>
<div><br></div><div> The ECMAScript compiler can be invoked from the command line using</div><div> the flag --js:</div><div><br></div><div> agda --js --compile-dir=<DIR> <FILE>.agda</div><div><br></div><div>
Each source <FILE>.agda is compiled into an ECMAScript target</div><div> <DIR>/jAgda.<TOP-LEVEL MODULE NAME>.js. The compiler can also be</div><div> invoked using the Emacs mode (the variable agda2-backend controls</div>
<div> which backend is used).</div><div><br></div><div> Note that ECMAScript is a strict rather than lazy language. Since</div><div> Agda programs are total, this should not impact program semantics,</div><div> but it may impact their space or time usage.</div>
<div><br></div><div> ECMAScript does not support algebraic datatypes or pattern-matching.</div><div> These features are translated to a use of the visitor pattern. For</div><div> instance, the standard library's List data type and null function</div>
<div> are translated into the following code:</div><div><br></div><div> exports["List"] = {};</div><div> exports["List"]["[]"] = function (x0) {</div><div> return x0["[]"]();</div>
<div> };</div><div> exports["List"]["_∷_"] = function (x0) {</div><div> return function (x1) {</div><div> return function (x2) {</div><div> return x2["_∷_"](x0, x1);</div>
<div> };</div><div> };</div><div> };</div><div><br></div><div> exports["null"] = function (x0) {</div><div> return function (x1) {</div><div> return function (x2) {</div>
<div>
return x2({</div><div> "[]": function () {</div><div> return jAgda_Data_Bool["Bool"]["true"];</div><div> },</div><div> "_∷_": function (x3, x4) {</div>
<div> return jAgda_Data_Bool["Bool"]["false"];</div><div> }</div><div> });</div><div> };</div><div> };</div><div> };</div><div><br></div><div>
Agda records are translated to ECMAScript objects, preserving field</div><div> names.</div><div><br></div><div> Top-level Agda modules are translated to ECMAScript modules,</div><div> following the common.js module specification. A top-level Agda</div>
<div> module "Foo.Bar" is translated to an ECMAScript module</div><div> "jAgda.Foo.Bar".</div><div><br></div><div> The ECMAScript compiler does not compile to Haskell, so the pragmas</div><div> related to the Haskell FFI (IMPORT, COMPILED_DATA and COMPILED) are</div>
<div> not used by the ECMAScript backend. Instead, there is a COMPILED_JS</div><div> pragma which may be applied to any declaration. For postulates,</div><div> primitives, functions and values, it gives the ECMAScript code to be</div>
<div> emitted by the compiler. For data types, it gives a function which</div><div> is applied to a value of that type, and a visitor object. For</div><div> instance, a binding of natural numbers to ECMAScript integers</div>
<div> (ignoring overflow errors) is:</div><div><br></div><div> data ℕ : Set where</div><div> zero : ℕ</div><div> suc : ℕ → ℕ</div><div><br></div><div> {-# COMPILED_JS ℕ function (x,v) {</div><div> if (x < 1) { return v.zero(); } else { return v.suc(x-1); }</div>
<div> } #-}</div><div> {-# COMPILED_JS zero 0 #-}</div><div> {-# COMPILED_JS suc function (x) { return x+1; } #-}</div><div><br></div><div> _+_ : ℕ → ℕ → ℕ</div><div> zero + n = n</div><div> suc m + n = suc (m + n)</div>
<div><br></div><div> {-# COMPILED_JS _+_ function (x) { return function (y) {</div><div> return x+y; };</div><div> } #-}</div><div><br></div><div> To allow FFI code to be optimised, the ECMAScript in a COMPILED_JS</div>
<div> declaration is parsed, using a simple parser that recognises a pure</div><div> functional subset of ECMAScript, consisting of functions, function</div><div> applications, return, if-statements, if-expressions,</div>
<div> side-effect-free binary operators (no precedence, left associative),</div><div> side-effect-free prefix operators, objects (where all member names</div><div> are quoted), field accesses, and string and integer literals.</div>
<div> Modules may be imported using the require("<module-id>") syntax: any</div><div> impure code, or code outside the supported fragment, can be placed</div><div> in a module and imported.</div><div><br>
</div><div>Tools</div><div>=====</div><div><br></div><div>* New flag --safe, which can be used to type-check untrusted code.</div><div><br></div><div> This flag disables postulates, primTrustMe, and "unsafe" OPTION</div>
<div> pragmas, some of which are known to make Agda inconsistent.</div><div><br></div><div> Rejected pragmas:</div><div><br></div><div> --allow-unsolved-metas</div><div> --experimental-irrelevance</div><div> --guardedness-preserving-type-construtors</div>
<div> --injective-type-constructors</div><div> --no-coverage-check</div><div> --no-positivity-check</div><div> --no-termination-check</div><div> --sized-types</div><div> --type-in-type</div><div><br></div>
<div> Note that, at the moment, it is not possible to define the universe</div><div> level or coinduction primitives when --safe is used (because they</div><div> must be introduced as postulates). This can be worked around by</div>
<div> type-checking trusted files in a first pass, without using --safe,</div><div> and then using --safe in a second pass. Modules which have already</div><div> been type-checked are not re-type-checked just because --safe is</div>
<div> used.</div><div><br></div><div>* Dependency graphs.</div><div><br></div><div> The new flag --dependency-graph=FILE can be used to generate a DOT</div><div> file containing a module dependency graph. The generated file (FILE)</div>
<div> can be rendered using a tool like dot.</div><div><br></div><div>* The --no-unreachable-check flag has been removed.</div><div><br></div><div>* Projection functions are highlighted as functions instead of as</div><div>
fields. Field names (in record definitions and record values) are</div><div> still highlighted as fields.</div><div><br></div><div>* Support for jumping to positions mentioned in the information</div><div> buffer has been added.</div>
<div><br></div><div>* The "make install" command no longer installs Agda globally (by</div><div> default).</div></div><div><br></div>