Version-2-3-0

  ------------------------------------------------------------------------
  -- Release notes for Agda 2 version 2.3.0
  ------------------------------------------------------------------------

  Important changes since 2.2.10:

  Language
  ========

  * New more liberal syntax for mutually recursive definitions.

    It is no longer necessary to use the 'mutual' keyword to define
    mutually recursive functions or datatypes. Instead, it is enough to
    declare things before they are used. Instead of

      mutual
        f : A
        f = a[f, g]

        g : B[f]
        g = b[f, g]

    you can now write

      f : A
      g : B[f]
      f = a[f, g]
      g = b[f, g].

    With the new style you have more freedom in choosing the order in
    which things are type checked (previously type signatures were
    always checked before definitions). Furthermore you can mix
    arbitrary declarations, such as modules and postulates, with
    mutually recursive definitions.

    For data types and records the following new syntax is used to
    separate the declaration from the definition:

      -- Declaration.
      data Vec (A : Set) : Nat → Set  -- Note the absence of 'where'.

      -- Definition.
      data Vec A where
        []   : Vec A zero
        _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

      -- Declaration.
      record Sigma (A : Set) (B : A → Set) : Set

      -- Definition.
      record Sigma A B where
        constructor _,_
        field fst : A
              snd : B fst

    When making separated declarations/definitions private or abstract
    you should attach the 'private' keyword to the declaration and the
    'abstract' keyword to the definition. For instance, a private,
    abstract function can be defined as

      private
        f : A
      abstract
        f = e

    Finally it may be worth noting that the old style of mutually
    recursive definitions is still supported (it basically desugars into
    the new style).

  * Pattern matching lambdas.

    Anonymous pattern matching functions can be defined using the syntax

      \ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }

    (where, as usual, \ and -> can be replaced by λ and →). Internally
    this is translated into a function definition of the following form:

      .extlam p11 .. p1n = e1
      ...
      .extlam pm1 .. pmn = em

    This means that anonymous pattern matching functions are generative.
    For instance, refl will not be accepted as an inhabitant of the type

      (λ { true → true ; false → false }) ≡
      (λ { true → true ; false → false }),

    because this is equivalent to extlam1 ≡ extlam2 for some distinct
    fresh names extlam1 and extlam2.

    Currently the 'where' and 'with' constructions are not allowed in
    (the top-level clauses of) anonymous pattern matching functions.

    Examples:

      and : Bool → Bool → Bool
      and = λ { true x → x ; false _ → false }

      xor : Bool → Bool → Bool
      xor = λ { true  true  → false
              ; false false → false
              ; _     _     → true
              }

      fst : {A : Set} {B : A → Set} → Σ A B → A
      fst = λ { (a , b) → a }

      snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
      snd = λ { (a , b) → b }

  * Record update syntax.

    Assume that we have a record type and a corresponding value:

      record MyRecord : Set where
        field
          a b c : ℕ

      old : MyRecord
      old = record { a = 1; b = 2; c = 3 }

    Then we can update (some of) the record value's fields in the
    following way:

      new : MyRecord
      new = record old { a = 0; c = 5 }

    Here new normalises to record { a = 0; b = 2; c = 5 }. Any
    expression yielding a value of type MyRecord can be used instead of
    old.

    Record updating is not allowed to change types: the resulting value
    must have the same type as the original one, including the record
    parameters. Thus, the type of a record update can be inferred if the type
    of the original record can be inferred.

    The record update syntax is expanded before type checking. When the
    expression

      record old { upd-fields }

    is checked against a record type R, it is expanded to

      let r = old in record { new-fields },

    where old is required to have type R and new-fields is defined as
    follows: for each field x in R,

      - if x = e is contained in upd-fields then x = e is included in
        new-fields, and otherwise
      - if x is an explicit field then x = R.x r is included in
        new-fields, and
      - if x is an implicit or instance field, then it is omitted from
        new-fields.

    (Instance arguments are explained below.) The reason for treating
    implicit and instance fields specially is to allow code like the
    following:

      record R : Set where
        field
          {length} : ℕ
          vec      : Vec ℕ length
          -- More fields…

      xs : R
      xs = record { vec = 0 ∷ 1 ∷ 2 ∷ [] }

      ys = record xs { vec = 0 ∷ [] }

    Without the special treatment the last expression would need to
    include a new binding for length (for instance "length = _").

  * Record patterns which do not contain data type patterns, but which
    do contain dot patterns, are no longer rejected.

  * When the --without-K flag is used literals are now treated as
    constructors.

  * Under-applied functions can now reduce.

    Consider the following definition:

      id : {A : Set} → A → A
      id x = x

    Previously the expression id would not reduce. This has been changed
    so that it now reduces to λ x → x. Usually this makes little
    difference, but it can be important in conjunction with 'with'. See
    issue 365 for an example.

  * Unused AgdaLight legacy syntax (x y : A; z v : B) for telescopes has
    been removed.

  Universe polymorphism
  ---------------------

  * Universe polymorphism is now enabled by default.
    Use --no-universe-polymorphism to disable it.

  * Universe levels are no longer defined as a data type.

    The basic level combinators can be introduced in the following way:

    postulate
      Level : Set
      zero  : Level
      suc   : Level → Level
      max   : Level → Level → Level

    {-# BUILTIN LEVEL     Level #-}
    {-# BUILTIN LEVELZERO zero  #-}
    {-# BUILTIN LEVELSUC  suc   #-}
    {-# BUILTIN LEVELMAX  max   #-}

  * The BUILTIN equality is now required to be universe-polymorphic.

  * trustMe is now universe-polymorphic.

  Meta-variables and unification
  ------------------------------

  * Unsolved meta-variables are now frozen after every mutual block.
    This means that they cannot be instantiated by subsequent code. For
    instance,

      one : Nat
      one = _

      bla : one ≡ suc zero
      bla = refl

    leads to an error now, whereas previously it lead to the
    instantiation of _ with "suc zero". If you want to make use of the
    old behaviour, put the two definitions in a mutual block.

    All meta-variables are unfrozen during interactive editing, so that
    the user can fill holes interactively. Note that type-checking of
    interactively given terms is not perfect: Agda sometimes refuses to
    load a file, even though no complaints were raised during the
    interactive construction of the file. This is because certain checks
    (for instance, positivity) are only invoked when a file is loaded.

  * Record types can now be inferred.

    If there is a unique known record type with fields matching the
    fields in a record expression, then the type of the expression will
    be inferred to be the record type applied to unknown parameters.

    If there is no known record type with the given fields the type
    checker will give an error instead of producing lots of unsolved
    meta-variables.

    Note that "known record type" refers to any record type in any
    imported module, not just types which are in scope.

  * The occurrence checker distinguishes rigid and strongly rigid
    occurrences [Reed, LFMTP 2009; Abel & Pientka, TLCA 2011].

    The completeness checker now accepts the following code:

      h : (n : Nat) → n ≡ suc n → Nat
      h n ()

    Internally this generates a constraint _n = suc _n where the
    meta-variable _n occurs strongly rigidly, i.e. on a constructor path
    from the root, in its own defining term tree. This is never
    solvable.

    Weakly rigid recursive occurrences may have a solution [Jason Reed's
    PhD thesis, page 106]:

      test : (k : Nat) →
             let X : (Nat → Nat) → Nat
                 X = _
             in
             (f : Nat → Nat) → X f ≡ suc (f (X (λ x → k)))
      test k f = refl

    The constraint _X k f = suc (f (_X k (λ x → k))) has the solution
    _X k f = suc (f (suc k)), despite the recursive occurrence of _X.
    Here _X is not strongly rigid, because it occurs under the bound
    variable f. Previously Agda rejected this code; now it instead
    complains about an unsolved meta-variable.

  * Equation constraints involving the same meta-variable in the head
    now trigger pruning [Pientka, PhD, Sec. 3.1.2; Abel & Pientka, TLCA
    2011]. Example:

      same : let X : A → A → A → A × A
                 X = _
             in {x y z : A} → X x y y ≡ (x , y)
                            × X x x y ≡ X x y y
      same = refl , refl

    The second equation implies that X cannot depend on its second
    argument. After pruning the first equation is linear and can be
    solved.

  * Instance arguments.

    A new type of hidden function arguments has been added: instance
    arguments. This new feature is based on influences from Scala's
    implicits and Agda's existing implicit arguments.

    Plain implicit arguments are marked by single braces: {…}. Instance
    arguments are instead marked by double braces: {{…}}. Example:

      postulate
        A : Set
        B : A → Set
        a : A
        f : {{a : A}} → B a

    Instead of the double braces you can use the symbols ⦃ and ⦄, but
    these symbols must in many cases be surrounded by whitespace. (If
    you are using Emacs and the Agda input method, then you can conjure
    up the symbols by typing "\{{" and "\}}", respectively.)

    Instance arguments behave as ordinary implicit arguments, except for
    one important aspect: resolution of arguments which are not provided
    explicitly. For instance, consider the following code:

      test = f

    Here Agda will notice that f's instance argument was not provided
    explicitly, and try to infer it. All definitions in scope at f's
    call site, as well as all variables in the context, are considered.
    If exactly one of these names has the required type (A), then the
    instance argument will be instantiated to this name.

    This feature can be used as an alternative to Haskell type classes.
    If we define

      record Eq (A : Set) : Set where
        field equal : A → A → Bool,

    then we can define the following projection:

      equal : {A : Set} {{eq : Eq A}} → A → A → Bool
      equal {{eq}} = Eq.equal eq

    Now consider the following expression:

      equal false false ∨ equal 3 4

    If the following Eq "instances" for Bool and ℕ are in scope, and no
    others, then the expression is accepted:

      eq-Bool : Eq Bool
      eq-Bool = record { equal = … }

      eq-ℕ : Eq ℕ
      eq-ℕ = record { equal = … }

    A shorthand notation is provided to avoid the need to define
    projection functions manually:

      module Eq-with-implicits = Eq {{...}}

    This notation creates a variant of Eq's record module, where the
    main Eq argument is an instance argument instead of an explicit one.
    It is equivalent to the following definition:

      module Eq-with-implicits {A : Set} {{eq : Eq A}} = Eq eq

    Note that the short-hand notation allows you to avoid naming the
    "-with-implicits" module:

      open Eq {{...}}


    Instance argument resolution is not recursive. As an example,
    consider the following "parametrised instance":

      eq-List : {A : Set} → Eq A → Eq (List A)
      eq-List {A} eq = record { equal = eq-List-A }
        where
        eq-List-A : List A → List A → Bool
        eq-List-A []       []       = true
        eq-List-A (a ∷ as) (b ∷ bs) = equal a b ∧ eq-List-A as bs
        eq-List-A _        _        = false

    Assume that the only Eq instances in scope are eq-List and eq-ℕ.
    Then the following code does not type-check:

      test = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])

    However, we can make the code work by constructing a suitable
    instance manually:

      test′ = equal (1 ∷ 2 ∷ []) (3 ∷ 4 ∷ [])
        where eq-List-ℕ = eq-List eq-ℕ

    By restricting the "instance search" to be non-recursive we avoid
    introducing a new, compile-time-only evaluation model to Agda.

    For more information about instance arguments, see Devriese &
    Piessens [ICFP 2011]. Some examples are also available in the
    examples/instance-arguments subdirectory of the Agda distribution.

  Irrelevance
  -----------

  * Dependent irrelevant function types.

    Some examples illustrating the syntax of dependent irrelevant
    function types:

      .(x y : A) → B    .{x y z : A} → B
      ∀ x .y → B        ∀ x .{y} {z} .v → B

    The declaration

      f : .(x : A) → B[x]
      f x = t[x]

    requires that x is irrelevant both in t[x] and in B[x]. This is
    possible if, for instance, B[x] = B′ x, with B′ : .A → Set.

    Dependent irrelevance allows us to define the eliminator for the
    Squash type:

      record Squash (A : Set) : Set where
        constructor squash
        field
          .proof : A

      elim-Squash : {A : Set} (P : Squash A → Set)
                    (ih : .(a : A) → P (squash a)) →
                    (a⁻ : Squash A) → P a⁻
      elim-Squash P ih (squash a) = ih a

    Note that this would not type-check with
    (ih : (a : A) -> P (squash a)).

  * Records with only irrelevant fields.

    The following now works:

      record IsEquivalence {A : Set} (_≈_ : A → A → Set) : Set where
        field
          .refl  : Reflexive _≈_
          .sym   : Symmetric _≈_
          .trans : Transitive _≈_

      record Setoid : Set₁ where
        infix 4 _≈_
        field
          Carrier        : Set
          _≈_            : Carrier → Carrier → Set
          .isEquivalence : IsEquivalence _≈_

        open IsEquivalence isEquivalence public

    Previously Agda complained about the application
    IsEquivalence isEquivalence, because isEquivalence is irrelevant and
    the IsEquivalence module expected a relevant argument. Now, when
    record modules are generated for records consisting solely of
    irrelevant arguments, the record parameter is made irrelevant:

      module IsEquivalence {A : Set} {_≈_ : A → A → Set}
                           .(r : IsEquivalence {A = A} _≈_) where
        …

  * Irrelevant things are no longer erased internally. This means that
    they are printed as ordinary terms, not as "_" as before.

  * The new flag --experimental-irrelevance enables irrelevant universe
    levels and matching on irrelevant data when only one constructor is
    available. These features are very experimental and likely to change
    or disappear.

  Reflection
  ----------

  * The reflection API has been extended to mirror features like
    irrelevance, instance arguments and universe polymorphism, and to
    give (limited) access to definitions. For completeness all the
    builtins and primitives are listed below:

      -- Names.

      postulate Name : Set

      {-# BUILTIN QNAME Name #-}

      primitive
        -- Equality of names.
        primQNameEquality : Name → Name → Bool

      -- Is the argument visible (explicit), hidden (implicit), or an
      -- instance argument?

      data Visibility : Set where
        visible hidden instance : Visibility

      {-# BUILTIN HIDING   Visibility #-}
      {-# BUILTIN VISIBLE  visible    #-}
      {-# BUILTIN HIDDEN   hidden     #-}
      {-# BUILTIN INSTANCE instance   #-}

      -- Arguments can be relevant or irrelevant.

      data Relevance : Set where
        relevant irrelevant : Relevance

      {-# BUILTIN RELEVANCE  Relevance  #-}
      {-# BUILTIN RELEVANT   relevant   #-}
      {-# BUILTIN IRRELEVANT irrelevant #-}

      -- Arguments.

      data Arg A : Set where
        arg : (v : Visibility) (r : Relevance) (x : A) → Arg A

      {-# BUILTIN ARG    Arg #-}
      {-# BUILTIN ARGARG arg #-}

      -- Terms.

      mutual
        data Term : Set where
          -- Variable applied to arguments.
          var     : (x : ℕ) (args : List (Arg Term)) → Term
          -- Constructor applied to arguments.
          con     : (c : Name) (args : List (Arg Term)) → Term
          -- Identifier applied to arguments.
          def     : (f : Name) (args : List (Arg Term)) → Term
          -- Different kinds of λ-abstraction.
          lam     : (v : Visibility) (t : Term) → Term
          -- Pi-type.
          pi      : (t₁ : Arg Type) (t₂ : Type) → Term
          -- A sort.
          sort    : Sort → Term
          -- Anything else.
          unknown : Term

        data Type : Set where
          el : (s : Sort) (t : Term) → Type

        data Sort : Set where
          -- A Set of a given (possibly neutral) level.
          set     : (t : Term) → Sort
          -- A Set of a given concrete level.
          lit     : (n : ℕ) → Sort
          -- Anything else.
          unknown : Sort

      {-# BUILTIN AGDASORT            Sort    #-}
      {-# BUILTIN AGDATYPE            Type    #-}
      {-# BUILTIN AGDATERM            Term    #-}
      {-# BUILTIN AGDATERMVAR         var     #-}
      {-# BUILTIN AGDATERMCON         con     #-}
      {-# BUILTIN AGDATERMDEF         def     #-}
      {-# BUILTIN AGDATERMLAM         lam     #-}
      {-# BUILTIN AGDATERMPI          pi      #-}
      {-# BUILTIN AGDATERMSORT        sort    #-}
      {-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
      {-# BUILTIN AGDATYPEEL          el      #-}
      {-# BUILTIN AGDASORTSET         set     #-}
      {-# BUILTIN AGDASORTLIT         lit     #-}
      {-# BUILTIN AGDASORTUNSUPPORTED unknown #-}

      postulate
        -- Function definition.
        Function  : Set
        -- Data type definition.
        Data-type : Set
        -- Record type definition.
        Record    : Set

      {-# BUILTIN AGDAFUNDEF    Function  #-}
      {-# BUILTIN AGDADATADEF   Data-type #-}
      {-# BUILTIN AGDARECORDDEF Record    #-}

      -- Definitions.

      data Definition : Set where
        function     : Function  → Definition
        data-type    : Data-type → Definition
        record′      : Record    → Definition
        constructor′ : Definition
        axiom        : Definition
        primitive′   : Definition

      {-# BUILTIN AGDADEFINITION                Definition   #-}
      {-# BUILTIN AGDADEFINITIONFUNDEF          function     #-}
      {-# BUILTIN AGDADEFINITIONDATADEF         data-type    #-}
      {-# BUILTIN AGDADEFINITIONRECORDDEF       record′      #-}
      {-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-}
      {-# BUILTIN AGDADEFINITIONPOSTULATE       axiom        #-}
      {-# BUILTIN AGDADEFINITIONPRIMITIVE       primitive′   #-}

      primitive
        -- The type of the thing with the given name.
        primQNameType        : Name → Type
        -- The definition of the thing with the given name.
        primQNameDefinition  : Name → Definition
        -- The constructors of the given data type.
        primDataConstructors : Data-type → List Name

    As an example the expression

      primQNameType (quote zero)

    is definitionally equal to

      el (lit 0) (def (quote ℕ) [])

    (if zero is a constructor of the data type ℕ).

  * New keyword: unquote.

    The construction "unquote t" converts a representation of an Agda term
    to actual Agda code in the following way:

    1. The argument t must have type Term (see the reflection API above).

    2. The argument is normalised.

    3. The entire construction is replaced by the normal form, which is
       treated as syntax written by the user and type-checked in the
       usual way.

    Examples:

      test : unquote (def (quote ℕ) []) ≡ ℕ
      test = refl

      id : (A : Set) → A → A
      id = unquote (lam visible (lam visible (var 0 [])))

      id-ok : id ≡ (λ A (x : A) → x)
      id-ok = refl

  * New keyword: quoteTerm.

    The construction "quoteTerm t" is similar to "quote n", but whereas
    quote is restricted to names n, quoteTerm accepts terms t. The
    construction is handled in the following way:

    1. The type of t is inferred. The term t must be type-correct.

    2. The term t is normalised.

    3. The construction is replaced by the Term representation (see the
       reflection API above) of the normal form. Any unsolved metavariables
       in the term are represented by the "unknown" term constructor.

    Examples:

      test₁ : quoteTerm (λ {A : Set} (x : A) → x) ≡
              lam hidden (lam visible (var 0 []))
      test₁ = refl

      -- Local variables are represented as de Bruijn indices.
      test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])
      test₂ = refl

      -- Terms are normalised before being quoted.
      test₃ : quoteTerm (0 + 0) ≡ con (quote zero) []
      test₃ = refl

  Compiler backends
  =================

  MAlonzo
  -------

  * The MAlonzo backend's FFI now handles universe polymorphism in a
    better way.

    The translation of Agda types and kinds into Haskell now supports
    universe-polymorphic postulates. The core changes are that the
    translation of function types has been changed from

      T[[ Pi (x : A) B ]] =
        if A has a Haskell kind then
          forall x. () -> T[[ B ]]
        else if x in fv B then
          undef
        else
          T[[ A ]] -> T[[ B ]]

    into

      T[[ Pi (x : A) B ]] =
        if x in fv B then
          forall x. T[[ A ]] -> T[[ B ]]  -- Note: T[[A]] not Unit.
        else
          T[[ A ]] -> T[[ B ]],

    and that the translation of constants (postulates, constructors and
    literals) has been changed from

      T[[ k As ]] =
        if COMPILED_TYPE k T then
          T T[[ As ]]
        else
          undef

    into

      T[[ k As ]] =
        if COMPILED_TYPE k T then
          T T[[ As ]]
        else if COMPILED k E then
          ()
        else
          undef.

    For instance, assuming a Haskell definition

      type AgdaIO a b = IO b,

    we can set up universe-polymorphic IO in the following way:

      postulate
        IO     : ∀ {ℓ} → Set ℓ → Set ℓ
        return : ∀ {a} {A : Set a} → A → IO A
        _>>=_  : ∀ {a b} {A : Set a} {B : Set b} →
                 IO A → (A → IO B) → IO B

      {-# COMPILED_TYPE IO AgdaIO              #-}
      {-# COMPILED return  (\_ _ -> return)    #-}
      {-# COMPILED _>>=_   (\_ _ _ _ -> (>>=)) #-}

    This is accepted because (assuming that the universe level type is
    translated to the Haskell unit type "()")

      (\_ _ -> return)
        : forall a. () -> forall b. () -> b -> AgdaIO a b
        = T [[ ∀ {a} {A : Set a} → A → IO A ]]

    and

      (\_ _ _ _ -> (>>=))
        : forall a. () -> forall b. () ->
            forall c. () -> forall d. () ->
              AgdaIO a c -> (c -> AgdaIO b d) -> AgdaIO b d
        = T [[ ∀ {a b} {A : Set a} {B : Set b} →
                 IO A → (A → IO B) → IO B ]].

  Epic
  ----

  * New Epic backend pragma: STATIC.

    In the Epic backend, functions marked with the STATIC pragma will be
    normalised before compilation. Example usage:

      {-# STATIC power #-}

      power : ℕ → ℕ → ℕ
      power 0       x = 1
      power 1       x = x
      power (suc n) x = power n x * x

    Occurrences of "power 4 x" will be replaced by "((x * x) * x) * x".

  * Some new optimisations have been implemented in the Epic backend:

    - Removal of unused arguments.

    A worker/wrapper transformation is performed so that unused
    arguments can be removed by Epic's inliner. For instance, the map
    function is transformed in the following way:

      map_wrap : (A B : Set) → (A → B) → List A → List B
      map_wrap A B f xs = map_work f xs

      map_work f []       = []
      map_work f (x ∷ xs) = f x ∷ map_work f xs

    If map_wrap is inlined (which it will be in any saturated call),
    then A and B disappear in the generated code.

    Unused arguments are found using abstract interpretation. The bodies
    of all functions in a module are inspected to decide which variables
    are used. The behaviour of postulates is approximated based on their
    types. Consider return, for instance:

      postulate return : {A : Set} → A → IO A

    The first argument of return can be removed, because it is of type
    Set and thus cannot affect the outcome of a program at runtime.

    - Injection detection.

    At runtime many functions may turn out to be inefficient variants of
    the identity function. This is especially true after forcing.
    Injection detection replaces some of these functions with more
    efficient versions. Example:

      inject : {n : ℕ} → Fin n → Fin (1 + n)
      inject {suc n} zero    = zero
      inject {suc n} (suc i) = suc (inject {n} i)

    Forcing removes the Fin constructors' ℕ arguments, so this function
    is an inefficient identity function that can be replaced by the
    following one:

      inject {_} x = x

    To actually find this function, we make the induction hypothesis
    that inject is an identity function in its second argument and look
    at the branches of the function to decide if this holds.

    Injection detection also works over data type barriers. Example:

      forget : {A : Set} {n : ℕ} → Vec A n → List A
      forget []       = []
      forget (x ∷ xs) = x ∷ forget xs

    Given that the constructor tags (in the compiled Epic code) for
    Vec.[] and List.[] are the same, and that the tags for Vec._∷_ and
    List._∷_ are also the same, this is also an identity function. We
    can hence replace the definition with the following one:

      forget {_} xs = xs

    To get this to apply as often as possible, constructor tags are
    chosen /after/ injection detection has been run, in a way to make as
    many functions as possible injections.

    Constructor tags are chosen once per source file, so it may be
    advantageous to define conversion functions like forget in the same
    module as one of the data types. For instance, if Vec.agda imports
    List.agda, then the forget function should be put in Vec.agda to
    ensure that vectors and lists get the same tags (unless some other
    injection function, which puts different constraints on the tags, is
    prioritised).

    - Smashing.

    This optimisation finds types whose values are inferable at runtime:

      * A data type with only one constructor where all fields are
        inferable is itself inferable.
      * Set ℓ is inferable (as it has no runtime representation).

    A function returning an inferable data type can be smashed, which
    means that it is replaced by a function which simply returns the
    inferred value.

    An important example of an inferable type is the usual propositional
    equality type (_≡_). Any function returning a propositional equality
    can simply return the reflexivity constructor directly without
    computing anything.

    This optimisation makes more arguments unused. It also makes the
    Epic code size smaller, which in turn speeds up compilation.

  JavaScript
  ----------

  * ECMAScript compiler backend.

    A new compiler backend is being implemented, targetting ECMAScript
    (also known as JavaScript), with the goal of allowing Agda programs
    to be run in browsers or other ECMAScript environments.

    The backend is still at an experimental stage: the core language is
    implemented, but many features are still missing.

    The ECMAScript compiler can be invoked from the command line using
    the flag --js:

      agda --js --compile-dir=<DIR> <FILE>.agda

    Each source <FILE>.agda is compiled into an ECMAScript target
    <DIR>/jAgda.<TOP-LEVEL MODULE NAME>.js. The compiler can also be
    invoked using the Emacs mode (the variable agda2-backend controls
    which backend is used).

    Note that ECMAScript is a strict rather than lazy language. Since
    Agda programs are total, this should not impact program semantics,
    but it may impact their space or time usage.

    ECMAScript does not support algebraic datatypes or pattern-matching.
    These features are translated to a use of the visitor pattern. For
    instance, the standard library's List data type and null function
    are translated into the following code:

      exports["List"] = {};
      exports["List"]["[]"] = function (x0) {
          return x0["[]"]();
        };
      exports["List"]["_∷_"] = function (x0) {
          return function (x1) {
            return function (x2) {
              return x2["_∷_"](x0, x1);
            };
          };
        };

      exports["null"] = function (x0) {
          return function (x1) {
            return function (x2) {
              return x2({
                "[]": function () {
                  return jAgda_Data_Bool["Bool"]["true"];
                },
                "_∷_": function (x3, x4) {
                  return jAgda_Data_Bool["Bool"]["false"];
                }
              });
            };
          };
        };

    Agda records are translated to ECMAScript objects, preserving field
    names.

    Top-level Agda modules are translated to ECMAScript modules,
    following the common.js module specification. A top-level Agda
    module "Foo.Bar" is translated to an ECMAScript module
    "jAgda.Foo.Bar".

    The ECMAScript compiler does not compile to Haskell, so the pragmas
    related to the Haskell FFI (IMPORT, COMPILED_DATA and COMPILED) are
    not used by the ECMAScript backend. Instead, there is a COMPILED_JS
    pragma which may be applied to any declaration. For postulates,
    primitives, functions and values, it gives the ECMAScript code to be
    emitted by the compiler. For data types, it gives a function which
    is applied to a value of that type, and a visitor object. For
    instance, a binding of natural numbers to ECMAScript integers
    (ignoring overflow errors) is:

      data ℕ : Set where
        zero : ℕ
        suc  : ℕ → ℕ

      {-# COMPILED_JS ℕ function (x,v) {
          if (x < 1) { return v.zero(); } else { return v.suc(x-1); }
        } #-}
      {-# COMPILED_JS zero 0 #-}
      {-# COMPILED_JS suc function (x) { return x+1; } #-}

      _+_ : ℕ → ℕ → ℕ
      zero  + n = n
      suc m + n = suc (m + n)

      {-# COMPILED_JS _+_ function (x) { return function (y) {
                            return x+y; };
        } #-}

    To allow FFI code to be optimised, the ECMAScript in a COMPILED_JS
    declaration is parsed, using a simple parser that recognises a pure
    functional subset of ECMAScript, consisting of functions, function
    applications, return, if-statements, if-expressions,
    side-effect-free binary operators (no precedence, left associative),
    side-effect-free prefix operators, objects (where all member names
    are quoted), field accesses, and string and integer literals.
    Modules may be imported using the require("<module-id>") syntax: any
    impure code, or code outside the supported fragment, can be placed
    in a module and imported.

  Tools
  =====

  * New flag --safe, which can be used to type-check untrusted code.

    This flag disables postulates, primTrustMe, and "unsafe" OPTION
    pragmas, some of which are known to make Agda inconsistent.

    Rejected pragmas:

      --allow-unsolved-metas
      --experimental-irrelevance
      --guardedness-preserving-type-construtors
      --injective-type-constructors
      --no-coverage-check
      --no-positivity-check
      --no-termination-check
      --sized-types
      --type-in-type

    Note that, at the moment, it is not possible to define the universe
    level or coinduction primitives when --safe is used (because they
    must be introduced as postulates). This can be worked around by
    type-checking trusted files in a first pass, without using --safe,
    and then using --safe in a second pass. Modules which have already
    been type-checked are not re-type-checked just because --safe is
    used.

  * Dependency graphs.

    The new flag --dependency-graph=FILE can be used to generate a DOT
    file containing a module dependency graph. The generated file (FILE)
    can be rendered using a tool like dot.

  * The --no-unreachable-check flag has been removed.

  * Projection functions are highlighted as functions instead of as
    fields. Field names (in record definitions and record values) are
    still highlighted as fields.

  * Support for jumping to positions mentioned in the information
    buffer has been added.

  * The "make install" command no longer installs Agda globally (by
    default).
Page last modified on November 23, 2011, at 09:21 am
Powered by PmWiki