Agda v2.6.2 Release Notes

  • Installation and infrastructure

    • βž• Added support for GHC 8.10.4 and 9.0.1.

    • 0️⃣ Some expensive optimisations are now off by default (see #4521).

    These optimisations can in some cases make Agda substantially faster, but they can also make the compilation of the Agda program take more time and space.

    The optimisations can be turned on manually (Cabal: -foptimise-heavily, Stack: --flag Agda:optimise-heavily). They are turned on (by default) when Agda is installed using make install.

    If the optimisations are turned on it might make sense to limit GHC's memory usage (using something like --ghc-options="+RTS -M6G -RTS").

    Pragmas and options

    • πŸ†• New option --auto-inline turns on automatic compile-time inlining of simple functions. This was previously enabled by default.

    Note that the absence of automatic inlining can make typechecking substantially slower.

    The new default has repercussions on termination checking, for instance (see #4702). The following formulation of plus termination checks with --auto-inline but not without:

      open import Agda.Builtin.Nat
      case_of_ : {A B : Set} β†’ A β†’ (A β†’ B) β†’ B
      case x of f = f x
      plus : Nat β†’ Nat β†’ Nat
      plus m n = case m of Ξ»
         { zero    β†’ n
         ; (suc m) β†’ suc (plus m n)

    In this particular case, we can work around the limitation of the termination checker with pragma {-# INLINE case_of_ #-}.

    • πŸ†• New options --qualified-instances (default) and --no-qualified-instances. When --no-qualified-instances is enabled, Agda will only consider candidates for instance search that are in scope under an unqualified name (see #4522).

    • πŸ†• New option --call-by-name turns off call-by-need evaluation at type checking time.

    • πŸ†• New option --highlight-occurrences (off by default) enables the HTML backend to include a JavaScript file that highlights all occurrences of the mouse-hovered symbol (see #4535).

    • πŸ†• New option --no-import-sorts disables the implicit open import Agda.Primitive using (Set; Prop) at the top of each file (see below).

    • πŸ†• New option --local-confluence-check to restore the old behaviour of the --confluence-check flag (see below for the new behaviour).

    • πŸ†• New primitive primStringFromListInjective internalising the fact that primStringFromList is an injective function. It is bound in Agda.Builtin.String.Properties.

    • πŸ†• New option --allow-exec enables the use of system calls during type checking using the AGDATCMEXECTC builtin.

    • πŸ†• New option --show-identity-substitutions shows all arguments of metavariables when pretty-printing a term, even if they amount to just applying all the variables in the context.

    • The option --rewriting is now considered infective: if a module has --rewriting enabled, then all modules importing it must also have --rewriting enabled.

    Command-line interaction

    • πŸš€ In the previous release, Agda exited with either status 0 when the program type checks successfully, or status 1 when encountering any kind of error. Now Agda exits with status 42 for type errors, 71 for errors in the commandline arguments, and 154 for impossible errors. Exit status 1 may be returned under other circumstances; for instance, an incomplete pattern matching, or an error generated by the Haskell runtime. See PR #4540.


    • πŸ‘ Inductive records without Ξ·-equality no longer support both matching on the record constructor and construction of record elements by copattern matching. It has been discovered that the combination of both leads to loss of subject reduction, i.e., reduction does not preserve typing. See issue #4560.

    Ξ·-equality for a record can be turned off manually with directive no-eta-equality or command-line option --no-eta-equality, but it is also automatically turned off for some recursive records. For records without Ξ·, matching on the record constructor is now off by default and construction by copattern matching is on. If you want the converse, you can add the new record directive pattern.

    Example with record pattern:

      record N : Set where
        field out : Maybe N
      pred : N β†’ Maybe N
      pred record{ out = m } = m

    Example with record constructor and use of ; instead of newline:

      record N : Set where
        inductive; no-eta-equality
        pattern; constructor inn
        field out : Maybe N
      pred : N β†’ Maybe N
      pred (inn m) = m
    • Set and Prop are no longer keywords but are now primitives defined in the module Agda.Primitive. They can be renamed when importing this module, for example:
      open import Agda.Primitive renaming (Set to Type)
      test : Type₁
      test = Type

    To preserve backwards compatibility, each top-level Agda module now starts with an implicit statement:

      open import Agda.Primitive using (Set; Prop)

    This implicit import can be disabled with the --no-import-sorts flag.

    • πŸ‘ Agda now has support for sorts SetΟ‰α΅’ (alternative syntax: SetΟ‰i) for natural numbers i, where SetΟ‰β‚€ = SetΟ‰. These sorts form a second hierarchy SetΟ‰α΅’ : SetΟ‰α΅’β‚Šβ‚ similar to the standard hierarchy of Setα΅’, but do not support universe polymorphism. It should not be necessary to refer to these sorts during normal usage of Agda, but they might be useful for defining reflection-based macros (see #2119 and #4585).

    • πŸ”„ Changed the internal representation of literal strings: instead of using a linked list of characters (String), we are now using Data.Text. This should be a transparent change from the user's point of view: the backend was already packing these strings as text.

    Used this opportunity to introduce a primStringUncons primitive in Agda.Builtin.String (and to correspondingly add the Agda.Builtin.Maybe it needs).

    • The option --confluence-check for rewrite rules has been given a new implementation that checks global confluence instead of local confluence. Concretely, it does so by enforcing two properties:
    1. For any two left-hand sides of the rewrite rules that overlap (either at the root position or at a subterm), the most general unifier of the two left-hand sides is again a left-hand side of a rewrite rule. For example, if there are two rules @suc m + n = suc (m + n)@ and @m + suc n = suc (m + n)@, then there should also be a rule @suc m + suc n = suc (suc (m + n))@.

    2. Each rewrite rule should satisfy the triangle property: For any rewrite rule @u = [email protected] and any single-step parallel unfolding @u => [email protected], we should have another single-step parallel unfolding @v => [email protected]

    The previous behaviour of the confluence checker that only ensures local confluence can be restored by using the --local-confluence-check flag.

    • Binary integer literals with prefix 0b (for instance, 0b11001001) are now supported.

    • Overloaded literals now require the conversion function (fromNat, fromNeg, or fromString) to be in scope unqualified to take effect.

    Previously, it was enough for the function to be in scope at all, which meant you couldn't import the corresponding builtin module without having overloaded literals turned on.

    • βž• Added interleaved mutual blocks where users can forward-declare function, record, and data types and interleave their definitions. These blocks are elaborated to more traditional mutual blocks by:

      • leaving the signatures where they are
      • grouping the clauses for a function together with the first of them
      • grouping the constructors for a datatype together with the first of them

    Example: two interleaved function definitions

      interleaved mutual
        -- Declarations:
        even : Nat β†’ Bool
        odd  : Nat β†’ Bool
        -- zero is even, not odd
        even zero = true
        odd  zero = false
        -- suc case: switch evenness on the predecessor
        even (suc n) = odd n
        odd  (suc n) = even n

    Other example: the definition of universe of types closed under the natural numbers and pairing:

      interleaved mutual
        -- Declaration of a product record, a universe of codes, and a decoding function
        record _Γ—_ (A B : Set) : Set
        data U : Set
        El : U β†’ Set
        -- We have a code for the type of natural numbers in our universe
        constructor `Nat : U
        El `Nat = Nat
        -- Btw we know how to pair values in a record
        record _Γ—_ A B where
          constructor _,_
          field fst : A; snd : B
        -- And we have a code for pairs in our universe
        constructor _`Γ—_ : (A B : U) β†’ U
        El (A `Γ— B) = El A Γ— El B
    • πŸ‘€ Erased constructors (see #4638).

    Constructors can be marked as erased. Example:

        {-# OPTIONS --cubical --safe #-}
        open import Agda.Builtin.Cubical.Path
        open import Agda.Primitive
            a   : Level
            A B : Set a
        Is-proposition : Set a β†’ Set a
        Is-proposition A = (x y : A) β†’ x ≑ y
        data βˆ₯_βˆ₯ (A : Set a) : Set a where
          ∣_∣        : A β†’ βˆ₯ A βˆ₯
          @0 trivial : Is-proposition βˆ₯ A βˆ₯
        rec : @0 Is-proposition B β†’ (A β†’ B) β†’ βˆ₯ A βˆ₯ β†’ B
        rec p f ∣ x ∣           = f x
        rec p f (trivial x y i) = p (rec p f x) (rec p f y) i

    In the code above the constructor trivial is only available at compile-time, whereas ∣_∣ is also available at run-time. Erased names can be used in bodies of clauses that match on trivial, like the final clause of rec. (Note that Cubical Agda programs still cannot be compiled.)

    The following code is also accepted:

      {-# OPTIONS --without-K --safe #-}
      open import Agda.Builtin.Bool
      data D : Set where
        run-time        : Bool β†’ D
        @0 compile-time : Bool β†’ D
      f : @0 D β†’ D
      f (compile-time x) = compile-time x
      f (run-time _)     = run-time true

    Agda allows matching on an erased argument if there is only one valid run-time case. (If the K rule is turned off, then the data type must also be non-indexed.) When f is compiled the clause that matches on compile-time is omitted.

    • πŸ†• New (?) rule for modalities of generalised variables (see #5058).

    The new rule is that generalisable variables get the modality that they are declared with, whereas other variables always get the default modality. (It is unclear what the old rule was, perhaps nothing was changed.)

    • πŸ‘€ Private abstract type signatures can no longer see through abstract (see #418).

    This means that abstract definitions no longer evaluate in any type signatures in the same module. Previously they evaluated in type signatures of definitions that were both private and abstract.

    It also means that metavariables in type signatures have to be solved locally, and cannot make use of information in the definition body, and that constructors of abstract datatypes are not in scope in type signatures.

    • πŸ‘€ Type inference is disabled for abstract definitions (see #418).

    This means that abstract definitions (inluding functions defined in where blocks of abstract definitions) need complete type signatures.

    • One can now declare syntax with two name parts without any hole in between, and syntax without any holes.


      syntax Ξ£ A (Ξ» x β†’ B) = [ x ∢ A ] Γ— B
      syntax []            = [ ]
    • Internalised the inspect idiom that allows users to abstract over an expression in a with clause while, at the same time, remembering the origin of the abstracted pattern via an equation.

    In the following example, abstracting over and then matching on the result of p x allows the first call to filter p (x ∷ xs) to reduce.

    In case the element x is kept, the second call to filter on the LHS then performs the same p x test. Because we have retained the proof that p x ≑ true in eq, we are able to rewrite by this equality and get it to reduce too.

    This leads to just enough computation that we can finish the proof with an appeal to congruence and the induction hypothesis.

      filter-filter : βˆ€ p xs β†’ filter p (filter p xs) ≑ filter p xs
      filter-filter p []       = refl
      filter-filter p (x ∷ xs) with p x in eq
      ... | false = filter-filter p xs -- easy
      ... | true -- second filter stuck on `p x`: rewrite by `eq`!
        rewrite eq = cong (x ∷_) (filter-filter p xs)


    • Primitive operations for floating-point numbers changed. The equalities now follow IEEE 754 equality, after unifying all NaNs. Primitive inequality was added: agda primFloatEquality : Float -> Float -> Bool -- from primFloatNumericEquality primFloatLess : Float -> Float -> Bool -- from primFloatNumericLess primFloatInequality : Float -> Float -> Bool -- new The β€œnumeric” relations are now deprecated.

    There are several new predicates on floating-point numbers:

      primFloatIsInfinite     : Float -> Bool -- new
      primFloatIsNaN          : Float -> Bool -- new
      primFloatIsSafeInteger  : Float -> Bool -- new

    The primFloatIsSafeInteger function determines whether the value is a number that is a safe integer, i.e., is within the range where the arithmetic operations do not lose precision.

    The operations for conversion to integers (primRound, primFloor, and primCeiling) were renamed for consistency, and return a value of type Maybe Int, returning nothing for NaN and the infinities:

      primFloatRound   : Float β†’ Maybe Int -- from primRound
      primFloatFloor   : Float β†’ Maybe Int -- from primFloor
      primFloatCeiling : Float β†’ Maybe Int -- from primCeiling

    There are several new conversions:

      primIntToFloat    : Int -> Float               -- new
      primFloatToRatio  : Float -> (Int Γ— Nat)       -- new
      primRatioToFloat  : Int -> Nat -> Float        -- new
      primFloatDecode   : Float -> Maybe (Int Γ— Int) -- new
      primFloatEncode   : Int -> Int -> Maybe Float  -- new

    The primFloatDecode function decodes a floating-point number f to a mantissa and exponent, such that f = mantissa * 2 ^ exponent, normalised such that the mantissa is the smallest possible number. The primFloatEncode function encodes a pair of a mantissa and exponent to a floating-point number.

    There are several new operations:

      primFloatPow        : Float -> Float -> Float -- new
      primFloatATan2      : Float -> Float -> Float -- from primATan2
      primFloatSinh       : Float -> Float          -- new
      primFloatCosh       : Float -> Float          -- new
      primFloatTanh       : Float -> Float          -- new
      primFloatASinh      : Float -> Float          -- new
      primFloatACosh      : Float -> Float          -- new
      primFloatATanh      : Float -> Float          -- new

    Furthermore, the following operations were renamed for consistency:

      primFloatExp        : Float -> Float          -- from primExp
      primFloatSin        : Float -> Float          -- from primSin
      primFloatLog        : Float -> Float          -- from primLog
      primFloatCos        : Float -> Float          -- from primCos
      primFloatTan        : Float -> Float          -- from primTan
      primFloatASin       : Float -> Float          -- from primASin
      primFloatACos       : Float -> Float          -- from primACos
      primFloatATan       : Float -> Float          -- from primATan

    All of these operations are implemented on the JavaScript backend.

    • primNatToChar maps surrogate code points to the replacement character 'U+FFFD and surrogate code points are disallowed in character literals

    Surrogate code points are characters in the range U+D800 to U+DFFF and are reserved for use by UTF-16.

    The reason for this change is that strings are represented (at type-checking time and in the GHC backend) by Data.Text byte strings, which cannot represent surrogate code points and replaces them by U+FFFD. By doing the same for characters we can have primStringFromList be injective (witnessed by Agda.Builtin.String.Properties.primStringFromListInjective).


    • πŸ†• New operation in TC monad, similar to quoteTC but operating on types in SetΟ‰ agda quoteΟ‰TC : βˆ€ {A : SetΟ‰} β†’ A β†’ TC Term
    • πŸ–¨ typeError and debugPrint no longer inserts spaces around termErr and nameErr parts. They also do a better job of respecting line breaks in strErr parts.

    • The representation of reflected patterns and clauses has changed. Each clause now includes a telescope with the names and types of the pattern variables.

      data Clause where
        clause        : (tel : List (Ξ£ String Ξ» _ β†’ Arg Type)) (ps : List (Arg Pattern)) (t : Term) β†’ Clause
        absurd-clause : (tel : List (Ξ£ String Ξ» _ β†’ Arg Type)) (ps : List (Arg Pattern)) β†’ Clause

    These telescopes provide additional information on the types of pattern variables that was previously hard to reconstruct (see #2151). When unquoting a clause, the types in the clause telescope are currently ignored (but this is subject to change in the future).

    Three constructors of the Pattern datatype were also changed:

    • pattern variables now refer to a de Bruijn index (relative to the clause telescope) rather than a string,
    • absurd patterns take a de Bruijn index and are expected to be bound by the clause telescope,
    • dot patterns now include the actual dotted term.
      data Pattern where
        con    : (c : Name) (ps : List (Arg Pattern)) β†’ Pattern
        dot    : (t : Term)    β†’ Pattern   -- previously:   dot : Pattern
        var    : (x : Nat)     β†’ Pattern   -- previously:   var : (x : String) β†’ Pattern
        lit    : (l : Literal) β†’ Pattern
        proj   : (f : Name)    β†’ Pattern
        absurd : (x : Nat)     β†’ Pattern

    It is likely that this change to the reflected syntax requires you to update reflection code written for previous versions of Agda. Here are some tips for updating your code:

    • When quoting a clause, you can recover the name of a pattern variable by looking up the given index in the clause telescope. The contents of dot patterns can safely be ignored (unless you have a use for them).

    • When creating a new clause for unquoting, you need to create a telescope for the types of the pattern variables. To get back the old behaviour of Agda, it is sufficient to set all the types of the pattern variables to unknown. So you can construct the telescope by listing the names of all pattern variables and absurd patterns together with their ArgInfo. Meanwhile, the pattern variables should be numbered in order to update them to the new representation. As for the telescope types, the contents of a dot pattern can safely be set to unknown.

      • πŸ†• New operation in TC monad, execTC, which calls an external executable agda execTC : (exe : String) (args : List String) (stdIn : String) β†’ TC (Ξ£ Nat (Ξ» _ β†’ Ξ£ String (Ξ» _ β†’ String))) The execTC builtin takes three arguments: the basename of the executable (e.g., "echo"), aΒ list of arguments, and the contents of the standard input. It returns a triple, consisting of the exit code (as a natural number), the contents of the standard output, and the contents of the standard error.

    The builtin is only available when --allow-exec is passed. (Note that --allow-exec is incompatible with --safe.) To make an executable available to Agda, add the absolute path on a new line in ~/.agda/executables.

    • Two new operations in the TC monad, onlyReduceDefs and dontReduceDefs: agda onlyReduceDefs : βˆ€ {a} {A : Set a} β†’ List Name β†’ TC A β†’ TC A dontReduceDefs : βˆ€ {a} {A : Set a} β†’ List Name β†’ TC A β†’ TC A These functions allow picking a specific set of functions that should (resp. should not) be reduced while executing the given TC computation.

    For example, the following macro unifies the current hole with the term 3 - 3:

      macro₁ : Term -> TC ⊀
      macro₁ goal = do
        u   ← quoteTC ((1 + 2) - 3)
        u'  ← onlyReduceDefs (quote _+_ ∷ []) (normalise u)
        unify u' goal
    • πŸ†• New operation in the TC monad, withReconstructed: agda withReconstructed : βˆ€ {a} {A : Set a} β†’ TC A β†’ TC A

    This function ensures reconstruction of hidden parameters after performing the TC computation. For example, consider the following type and function:

      record RVec {a} (X : Set a) (n : Nat) : Set a where
        constructor vec
        field sel : Fin n β†’ X
      test-rvec : Nat β†’ RVec Nat 5
      test-rvec x = vec Ξ» _ β†’ x

    In the reflected syntax the body of the test-rvec would be represented as con vec (unknown ∷ unknown ∷ unknown ∷ (lam _ x). The use of withReconstructed replaces unknowns with the actual values:

      macroβ‚‚ : Name β†’ Term β†’ TC ⊀
      macroβ‚‚ n hole = do
        (function (clause tel ps t ∷ [])) ←
          withReconstructed (getDefinition n)
          where _ β†’ quoteTC "ERROR" >>= unify hole
        quoteTC t >>= unify hole
    • Three new constructors in the Sort datatype, prop : Level β†’ Sort, propLit : Nat β†’ Sort, and inf : Nat β†’ Sort, representing the sorts Prop β„“, Propα΅’, and SetΟ‰α΅’.

    • Terms that belong to a type in Prop are no longer unquoted to unknown but to a proper Term. (See #3553.)

    Library management

    • .agda-lib files can now contain an extra field flags: with default flags for the library. Flags can be any flags that are accepted as part of an {-# OPTIONS ... #-} pragma. For example, file my-library.agda-lib with
      flags: --without-K

    will apply the --without-K flag to all Agda files in the current directory and (recursive) subdirectories that do not themselves contain an .agda-lib file.

    Emacs mode

    • πŸ†• New command prefix C-u C-u C-u for weak-head normalization. For instance, given
      downFrom : Nat β†’ List Nat
      downFrom 0 = []
      downFrom (suc n) = n ∷ downFrom n

    C-u C-u C-u C-c C-n downFrom 5 returns 4 ∷ downFrom 4.

    • πŸ†• New keyboard shortcut C-c C-x C-i for toggling display of irrelevant arguments.

    • One can no longer use commands like M-; (comment-dwim) to uncomment block comments. In return one can use M-; to comment out pragmas. (See #3329.)

    JSON Interaction mode

    πŸ”„ Changes have been made to the structure of error and warning messages. The πŸ”„ changes are summarized below. See #5052 for additional details.

    • ⚠ The format of an error or warning was previously a bare string. Now, errors and warnings are represented by an object with a "message" key.

    This means that responses previously structured like:

      {"…": "…", "error": "Foo bar baz"}

    will now be structured:

      {"…": "…", "error": {"message": "Foo bar baz"}}

    This applies directly to the PostPonedCheckFunDef response kind and Error info kind of the DisplayInfo response kind.

    • ⚠ The format of collections of errors or warnings, which previously were each represented by a single newline-joined string, has been updated to represent each warning or error individually in a list.

    That means that responses previously structured like:

      { "…": "…"
      , "errors": "Postulates overcooked\nAxioms too wiggly"
      , "warnings": "Something wrong\nSomething else\nwrong"

    will now be structured:

      { "…": "…"
      , "errors":
        [ { "message": "Postulates overcooked" }
        , { "message": "Axioms too wiggly" }
      , "warnings":
        [ { "message": "Something wrong" }
        , { "message": "Something else\nwrong" }

    This applies to CompilationOk, AllGoalsWarning, and Error info kinds of the DisplayInfo response kind.

    • The Error info kind of the DisplayInfo response kind has additionally been updated to distinguish warnings and errors.

    An example of the previous format of a DispayInfo response with an Error info kind was:

        "kind": "DisplayInfo",
        "info": {
          "kind": "Error",
          "message": "β€”β€”β€”β€” Error β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”\n/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M\n\nβ€”β€”β€”β€” Warning(s) β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”\n/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."

    The updated format is:

        "kind": "DisplayInfo",
        "info": {
          "kind": "Error",
          "error": {
            "message": "/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M"
          "warnings": [
              "message": "/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."

    Compiler backends

    • With option --allow-unsolved-metas, code with holes can be compiled. If a hole is reached at runtime, the compiled program crashes. See issue #5103

    • Previously the GHC backend compiled at least one instance of Hinze's memoisation technique from "Memo functions, polytypically!" to reasonably efficient code. That is no longer the case (at least for that particular instance, see #5153).

    JS backend

    • Smaller local variable names in the generated JS code.

    Previously: x0, x1, x2, ...

    Now: a, b, c, ..., z, a0, b0, ..., z0, a1, b1, ...

    • πŸ‘Œ Improved indentation of generated JS code.

    • More compact rendering of generated JS functions.


      exports["N"]["suc"] = function (x0) {
          return function (x1) {
            return x1["suc"](x0);


      exports["N"]["suc"] = a => b => b["suc"](a);
    • Irrelevant arguments are now erased in the generated JS code.

    Example Agda code:

      flip : {A B C : Set} -> (B -> A -> C) -> A -> B -> C
      flip f a b = f b a

    Previously generated JS code:

      exports["flip"] = function (x0) {
          return function (x1) {
            return function (x2) {
              return function (x3) {
                return function (x4) {
                  return function (x5) {
                    return x3(x5)(x4);

    JS code generated now:

      exports["flip"] = a => b => c => a(c)(b);
    • Record fields are not stored separately (the fields are stored only in the constructor) in the generated JS code.

    Example Agda code:

      record Sigma (A : Set) (B : A -> Set) : Set where
          fst : A
          snd : B fst

    Previously generated JS code (look at the "fst" and "snd" fields in the return value of exports["Sigma"]["record"]:

      exports["Sigma"] = {};
      exports["Sigma"]["fst"] = function (x0) {
          return x0["record"]({
            "record": function (x1, x2) {
              return x1;
      exports["Sigma"]["snd"] = function (x0) {
          return x0["record"]({
            "record": function (x1, x2) {
              return x2;
      exports["Sigma"]["record"] = function (x0) {
          return function (x1) {
            return {
              "fst": x0,
              "record": function (x2) {
                return x2["record"](x0, x1);
              "snd": x1

    JS code generated now:

      exports["Sigma"] = {};
      exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});
      exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});
      exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});
    • ⚑️ --js-optimize flag has been added to the agda compiler.

    With --js-optimize, agda does not wrap records in JS objects.

    Example Agda code:

      record Sigma (A : Set) (B : A -> Set) : Set where
          fst : A
          snd : B fst

    JS code generated without the --js-optimize flag:

      exports["Sigma"] = {};
      exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});
      exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});
      exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});

    JS code generated with the --js-optimize flag:

      exports["Sigma"] = {};
      exports["Sigma"]["fst"] = a => a((b,c) => b);
      exports["Sigma"]["snd"] = a => a((b,c) => c);
      exports["Sigma"]["record"] = a => b => c => c(a,b);

    With --js-optimize, agda uses JS arrays instead of JS objects. This is possible because constructor names are not relevant during the evaluation.

    Example Agda code:

      data Bool : Set where
        false : Bool
        true  : Bool
      not : Bool -> Bool
      not false = true
      not true  = false

    JS code generated without the --js-optimize flag:

      exports["Bool"] = {};
      exports["Bool"]["false"] = a => a["false"]();
      exports["Bool"]["true"] = a => a["true"]();
      exports["not"] = a => a({
          "false": () => exports["Bool"]["true"],
          "true": () => exports["Bool"]["false"]

    JS code generated with the --js-optimize flag:

      exports["Bool"] = {};
      exports["Bool"]["false"] = a => a[0/* false */]();
      exports["Bool"]["true"] = a => a[1/* true */]();
      exports["not"] = a => a([
          /* false */() => exports["Bool"]["true"],
          /* true */() => exports["Bool"]["false"]

    Note that comments are added to generated JS code to help human readers.

    Erased branches are replaced by null in the generated array. If more than the half of branches are erased, the array is compressed to be a object like {3: ..., 13: ...}.

    • --js-minify flag has been added to the agda compiler.

    With --js-minify, agda discards comments and whitespace in the generated JS code.

    Agda as a library (API)

    • πŸ“œ The SourceInfo record has been renamed to Source, and the sourceInfo function to parseSource.