Nils Anders Danielsson | 27 Sep 22:37 2010
Picon

ANNOUNCE: Agda 2.2.8

Hi,

Agda 2.2.8 has now been released. Important changes since 2.2.6:

Language
--------

* Record pattern matching.

   It is now possible to pattern match on named record constructors.
   Example:

     record Σ (A : Set) (B : A → Set) : Set where
       constructor _,_
       field
         proj₁ : A
         proj₂ : B proj₁

     map : {A B : Set} {P : A → Set} {Q : B → Set}
           (f : A → B) → (∀ {x} → P x → Q (f x)) →
           Σ A P → Σ B Q
     map f g (x , y) = (f x , g y)

   The clause above is internally translated into the following one:

     map f g p = (f (Σ.proj₁ p) , g (Σ.proj₂ p))

   Record patterns containing data type patterns are not translated.
   Example:

     add : ℕ × ℕ → ℕ
     add (zero  , n) = n
     add (suc m , n) = suc (add (m , n))

   Record patterns which do not contain data type patterns, but which
   do contain dot patterns, are currently rejected. Example:

     Foo : {A : Set} (p₁ p₂ : A × A) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
     Foo (x , y) (.x , y′) refl = Set

* Proof irrelevant function types.

   Agda now supports irrelevant non-dependent function types:

     f : .A → B

   This type implies that f does not depend computationally on its
   argument. One intended use case is data structures with embedded
   proofs, like sorted lists:

     postulate
       _≤_ : ℕ → ℕ → Set
       p₁  : 0 ≤ 1
       p₂  : 0 ≤ 1

     data SList (bound : ℕ) : Set where
       []    : SList bound
       scons : (head : ℕ) →
               .(head ≤ bound) →
               (tail : SList head) →
               SList bound

   The effect of the irrelevant type in the signature of scons is that
   scons's second argument is never inspected after Agda has ensured
   that it has the right type. It is even thrown away, leading to
   smaller term sizes and hopefully some gain in efficiency. The
   type-checker ignores irrelevant arguments when checking equality, so
   two lists can be equal even if they contain different proofs:

     l₁ : SList 1
     l₁ = scons 0 p₁ []

     l₂ : SList 1
     l₂ = scons 0 p₂ []

     l₁≡l₂ : l₁ ≡ l₂
     l₁≡l₂ = refl

   Irrelevant arguments can only be used in irrelevant contexts.
   Consider the following subset type:

     data Subset (A : Set) (P : A → Set) : Set where
       _#_ : (elem : A) → .(P elem) → Subset A P

   The following two uses are fine:

     elimSubset : ∀ {A C : Set} {P} →
                  Subset A P → ((a : A) → .(P a) → C) → C
     elimSubset (a # p) k = k a p

     elem : {A : Set} {P : A → Set} → Subset A P → A
     elem (x # p) = x

   However, if we try to project out the proof component, then Agda
   complains that "variable p is declared irrelevant, so it cannot be
   used here":

     prjProof : ∀ {A P} (x : Subset A P) → P (elem x)
     prjProof (a # p) = p

   Matching against irrelevant arguments is also forbidden, except in
   the case of irrefutable matches (record constructor patterns which
   have been translated away). For instance, the match against the
   pattern (p , q) here is accepted:

     elim₂ : ∀ {A C : Set} {P Q : A → Set} →
             Subset A (λ x → Σ (P x) (λ _ → Q x)) →
             ((a : A) → .(P a) → .(Q a) → C) → C
     elim₂ (a # (p , q)) k = k a p q

   Absurd matches () are also allowed.

   Note that record fields can also be irrelevant. Example:

     record Subset (A : Set) (P : A → Set) : Set where
       constructor _#_
       field
         elem   : A
         .proof : P elem

   Irrelevant fields are never in scope, neither inside nor outside the
   record. This means that no record field can depend on an irrelevant
   field, and furthermore projections are not defined for such fields.
   Irrelevant fields can only be accessed using pattern matching, as in
   elimSubset above.

   Irrelevant function types were added very recently, and have not
   been subjected to much experimentation yet, so do not be surprised
   if something is changed before the next release. For instance,
   dependent irrelevant function spaces (.(x : A) → B) might be added
   in the future.

* Mixfix binders.

   It is now possible to declare user-defined syntax that binds
   identifiers. Example:

     postulate
       State  : Set → Set → Set
       put    : ∀ {S} → S → State S ⊤
       get    : ∀ {S} → State S S
       return : ∀ {A S} → A → State S A
       bind   : ∀ {A B S} → State S B → (B → State S A) → State S A

     syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂

     increment : State ℕ ⊤
     increment = x ← get ,
                 put (1 + x)

   The syntax declaration for bind implies that x is in scope in e₂,
   but not in e₁.

   You can give fixity declarations along with syntax declarations:

     infixr 40 bind
     syntax bind e₁ (λ x → e₂) = x ← e₁ , e₂

   The fixity applies to the syntax, not the name; syntax declarations
   are also restricted to ordinary, non-operator names. The following
   declaration is disallowed:

     syntax _==_ x y = x === y

   Syntax declarations must also be linear; the following declaration
   is disallowed:

     syntax wrong x = x + x

   Syntax declarations were added very recently, and have not been
   subjected to much experimentation yet, so do not be surprised if
   something is changed before the next release.

* Prop has been removed from the language.

   The experimental sort Prop has been disabled. Any program using Prop
   should typecheck if Prop is replaced by Set₀. Note that Prop is still
   a keyword.

* Injective type constructors off by default.

   Automatic injectivity of type constructors has been disabled (by
   default). To enable it, use the flag --injective-type-constructors,
   either on the command line or in an OPTIONS pragma. Note that this
   flag makes Agda anti-classical and possibly inconsistent:

     Agda with excluded middle is inconsistent
     http://thread.gmane.org/gmane.comp.lang.agda/1367

   See test/succeed/InjectiveTypeConstructors.agda for an example.

* Termination checker can count.

   There is a new flag --termination-depth=N accepting values N >= 1
   (with N = 1 being the default) which influences the behavior of the
   termination checker. So far, the termination checker has only
   distinguished three cases when comparing the argument of a recursive
   call with the formal parameter of the callee.

     < : the argument is structurally smaller than the parameter
     = : they are equal
     ? : the argument is bigger or unrelated to the parameter

   This behavior, which is still the default (N = 1), will not
   recognise the following functions as terminating.

     mutual

       f : ℕ → ℕ
       f zero          = zero
       f (suc zero)    = zero
       f (suc (suc n)) = aux n

       aux : ℕ → ℕ
       aux m = f (suc m)

   The call graph

     f --(<)--> aux --(?)--> f

   yields a recursive call from f to f via aux where the relation of
   call argument to callee parameter is computed as "unrelated"
   (composition of < and ?).

   Setting N >= 2 allows a finer analysis: n has two constructors less
   than suc (suc n), and suc m has one more than m, so we get the call
   graph:

     f --(-2)--> aux --(+1)--> f

   The indirect call f --> f is now labeled with (-1), and the
   termination checker can recognise that the call argument is
   decreasing on this path.

   Setting the termination depth to N means that the termination
   checker counts decrease up to N and increase up to N-1. The default,
   N=1, means that no increase is counted, every increase turns to
   "unrelated".

   In practice, examples like the one above sometimes arise when "with"
   is used. As an example, the program

     f : ℕ → ℕ
     f zero          = zero
     f (suc zero)    = zero
     f (suc (suc n)) with zero
     ... | _ = f (suc n)

   is internally represented as

     mutual

       f : ℕ → ℕ
       f zero          = zero
       f (suc zero)    = zero
       f (suc (suc n)) = aux n zero

       aux : ℕ → ℕ → ℕ
       aux m k = f (suc m)

   Thus, by default, the definition of f using "with" is not accepted
   by the termination checker, even though it looks structural (suc n
   is a subterm of suc suc n). Now, the termination checker is
   satisfied if the option "--termination-depth=2" is used.

   Caveats:

   - This is an experimental feature, hopefully being replaced by
     something smarter in the near future.

   - Increasing the termination depth will quickly lead to very long
     termination checking times. So, use with care. Setting termination
     depth to 100 by habit, just to be on the safe side, is not a good
     idea!

   - Increasing termination depth only makes sense for linear data
     types such as ℕ and Size. For other types, increase cannot be
     recognised. For instance, consider a similar example with lists.

       data List : Set where
	nil  : List
	cons : ℕ → List → List

       mutual
	f : List → List
	f nil                  = nil
	f (cons x nil)         = nil
	f (cons x (cons y ys)) = aux y ys

	aux : ℕ → List → List
	aux z zs = f (cons z zs)

     Here the termination checker compares cons z zs to z and also to
     zs. In both cases, the result will be "unrelated", no matter how
     high we set the termination depth. This is because when comparing
     cons z zs to zs, for instance, z is unrelated to zs, thus,
     cons z zs is also unrelated to zs. We cannot say it is just "one
     larger" since z could be a very large term. Note that this points
     to a weakness of untyped termination checking.

     To regain the benefit of increased termination depth, we need to
     index our lists by a linear type such as ℕ or Size. With
     termination depth 2, the above example is accepted for vectors
     instead of lists.

* The codata keyword has been removed. To use coinduction, use the
   following new builtins: INFINITY, SHARP and FLAT. Example:

     {-# OPTIONS --universe-polymorphism #-}

     module Coinduction where

     open import Level

     infix 1000 ♯_

     postulate
       ∞  : ∀ {a} (A : Set a) → Set a
       ♯_ : ∀ {a} {A : Set a} → A → ∞ A
       ♭  : ∀ {a} {A : Set a} → ∞ A → A

     {-# BUILTIN INFINITY ∞  #-}
     {-# BUILTIN SHARP    ♯_ #-}
     {-# BUILTIN FLAT     ♭  #-}

   Note that (non-dependent) pattern matching on SHARP is no longer
   allowed.

   Note also that strange things might happen if you try to combine the
   pragmas above with COMPILED_TYPE, COMPILED_DATA or COMPILED pragmas,
   or if the pragmas do not occur right after the postulates.

   The compiler compiles the INFINITY builtin to nothing (more or
   less), so that the use of coinduction does not get in the way of FFI
   declarations:

     data Colist (A : Set) : Set where
       []  : Colist A
       _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

     {-# COMPILED_DATA Colist [] [] (:) #-}

* Infinite types.

   If the new flag --guardedness-preserving-type-constructors is used,
   then type constructors are treated as inductive constructors when we
   check productivity (but only in parameters, and only if they are
   used strictly positively or not at all). This makes examples such as
   the following possible:

     data Rec (A : ∞ Set) : Set where
       fold : ♭ A → Rec A

     -- Σ cannot be a record type below.

     data Σ (A : Set) (B : A → Set) : Set where
       _,_ : (x : A) → B x → Σ A B

     syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

     -- Corecursive definition of the W-type.

     W : (A : Set) → (A → Set) → Set
     W A B = Rec (♯ (Σ[ x ∶ A ] (B x → W A B)))

     syntax W A (λ x → B) = W[ x ∶ A ] B

     sup : {A : Set} {B : A → Set} (x : A) (f : B x → W A B) → W A B
     sup x f = fold (x , f)

     W-rec : {A : Set} {B : A → Set}
             (P : W A B → Set) →
             (∀ {x} {f : B x → W A B} → (∀ y → P (f y)) → P (sup x f)) →
             ∀ x → P x
     W-rec P h (fold (x , f)) = h (λ y → W-rec P h (f y))

     -- Induction-recursion encoded as corecursion-recursion.

     data Label : Set where
       ′0 ′1 ′2 ′σ ′π ′w : Label

     mutual

       U : Set
       U = Σ Label U′

       U′ : Label → Set
       U′ ′0 = ⊤
       U′ ′1 = ⊤
       U′ ′2 = ⊤
       U′ ′σ = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
       U′ ′π = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
       U′ ′w = Rec (♯ (Σ[ a ∶ U ] (El a → U)))

       El : U → Set
       El (′0 , _)            = ⊥
       El (′1 , _)            = ⊤
       El (′2 , _)            = Bool
       El (′σ , fold (a , b)) = Σ[ x ∶ El a ]  El (b x)
       El (′π , fold (a , b)) =   (x : El a) → El (b x)
       El (′w , fold (a , b)) = W[ x ∶ El a ]  El (b x)

     U-rec : (P : ∀ u → El u → Set) →
             P (′1 , _) tt →
             P (′2 , _) true →
             P (′2 , _) false →
             (∀ {a b x y} →
              P a x → P (b x) y → P (′σ , fold (a , b)) (x , y)) →
             (∀ {a b f} →
              (∀ x → P (b x) (f x)) → P (′π , fold (a , b)) f) →
             (∀ {a b x f} →
              (∀ y → P (′w , fold (a , b)) (f y)) →
              P (′w , fold (a , b)) (sup x f)) →
             ∀ u (x : El u) → P u x
     U-rec P P1 P2t P2f Pσ Pπ Pw = rec
       where
       rec : ∀ u (x : El u) → P u x
       rec (′0 , _)            ()
       rec (′1 , _)            _              = P1
       rec (′2 , _)            true           = P2t
       rec (′2 , _)            false          = P2f
       rec (′σ , fold (a , b)) (x , y)        = Pσ (rec _ x) (rec _ y)
       rec (′π , fold (a , b)) f              = Pπ (λ x → rec _ (f x))
       rec (′w , fold (a , b)) (fold (x , f)) = Pw (λ y → rec _ (f y))

   The --guardedness-preserving-type-constructors extension is based on
   a rather operational understanding of ∞/♯_; it's not yet clear if
   this extension is consistent.

* Qualified constructors.

   Constructors can now be referred to qualified by their data type.
   For instance, given

     data Nat : Set where
       zero : Nat
       suc  : Nat → Nat

     data Fin : Nat → Set where
       zero : ∀ {n} → Fin (suc n)
       suc  : ∀ {n} → Fin n → Fin (suc n)

   you can refer to the constructors unambiguously as Nat.zero,
   Nat.suc, Fin.zero, and Fin.suc (Nat and Fin are modules containing
   the respective constructors). Example:

     inj : (n m : Nat) → Nat.suc n ≡ suc m → n ≡ m
     inj .m m refl = refl

   Previously you had to write something like

     inj : (n m : Nat) → _≡_ {Nat} (suc n) (suc m) → n ≡ m

   to make the type checker able to figure out that you wanted the
   natural number suc in this case.

* Reflection.

   There are two new constructs for reflection:

     - quoteGoal x in e

       In e the value of x will be a representation of the goal type
       (the type expected of the whole expression) as an element in a
       datatype of Agda terms (see below). For instance,

       example : ℕ
       example = quoteGoal x in {! at this point x = def (quote ℕ) [] !}

     - quote x : Name

       If x is the name of a definition (function, datatype, record, or
       a constructor), quote x gives you the representation of x as a
       value in the primitive type Name (see below).

   Quoted terms use the following BUILTINs and primitives (available
   from the standard library module Reflection):

     -- The type of Agda names.

     postulate Name : Set

     {-# BUILTIN QNAME Name #-}

     primitive primQNameEquality : Name → Name → Bool

     -- Arguments.

     Explicit? = Bool

     data Arg A : Set where
       arg : Explicit? → A → Arg A

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

     -- The type of Agda terms.

     data Term : Set where
       var     : ℕ → List (Arg Term) → Term
       con     : Name → List (Arg Term) → Term
       def     : Name → List (Arg Term) → Term
       lam     : Explicit? → Term → Term
       pi      : Arg Term → Term → Term
       sort    : Term
       unknown : Term

     {-# BUILTIN AGDATERM            Term    #-}
     {-# BUILTIN AGDATERMVAR         var     #-}
     {-# BUILTIN AGDATERMCON         con     #-}
     {-# BUILTIN AGDATERMDEF         def     #-}
     {-# BUILTIN AGDATERMLAM         lam     #-}
     {-# BUILTIN AGDATERMPI          pi      #-}
     {-# BUILTIN AGDATERMSORT        sort    #-}
     {-# BUILTIN AGDATERMUNSUPPORTED unknown #-}

   Reflection may be useful when working with internal decision
   procedures, such as the standard library's ring solver.

* Minor record definition improvement.

   The definition of a record type is now available when type checking
   record module definitions. This means that you can define things
   like the following:

     record Cat : Set₁ where
       field
         Obj  : Set
         _=>_ : Obj → Obj → Set
         -- ...

       -- not possible before:
       op : Cat
       op = record { Obj = Obj; _=>_ = λ A B → B => A }

Tools
-----

* The "Goal type and context" command now shows the goal type before
   the context, and the context is shown in reverse order. The "Goal
   type, context and inferred type" command has been modified in a
   similar way.

* Show module contents command.

   Given a module name M the Emacs mode can now display all the
   top-level modules and names inside M, along with types for the
   names. The command is activated using C-c C-o or the menus.

* Auto command.

   A command which searches for type inhabitants has been added. The
   command is invoked by pressing C-C C-a (or using the goal menu).
   There are several flags and parameters, e.g. '-c' which enables
   case-splitting in the search. For further information, see the Agda
   wiki:

     http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto

* HTML generation is now possible for a module with unsolved
   meta-variables, provided that the --allow-unsolved-metas flag is
   used.

--
/NAD

Gmane