[Agda] ANNOUNCE: Agda 2.2.0

[Nils Anders Danielsson]

Hi,

Agda 2.2.0 has now been released. Important changes since 2.1.2 (which
was released 2007-08-16):

Language
--------

* Exhaustive pattern checking. Agda complains if there are missing
  clauses in a function definition.

* Coinductive types are supported. This feature is under
  development/evaluation, and may change.

  http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes

* Another experimental feature: Sized types, which can make it easier
  to explain why your code is terminating.

* Improved constraint solving for functions with constructor headed
  right hand sides.

  http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments

* A simple, well-typed foreign function interface, which allows use of
  Haskell functions in Agda code.

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.FFI

* The tokens forall, -> and \ can be written as ∀, → and λ.

* Absurd lambdas: λ () and λ {}.

  http://thread.gmane.org/gmane.comp.lang.agda/440

* Record fields whose values can be inferred can be omitted.

* Agda complains if it spots an unreachable clause, or if a pattern
  variable "shadows" a hidden constructor of matching type.

  http://thread.gmane.org/gmane.comp.lang.agda/720

Tools
-----

* Case-split: The user interface can replace a pattern variable with
  the corresponding constructor patterns. You get one new left-hand
  side for every possible constructor.

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

* The MAlonzo compiler.

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo

* A new Emacs input method, which contains bindings for many Unicode
  symbols, is by default activated in the Emacs mode.

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput

* Highlighted, hyperlinked HTML can be generated from Agda source
  code.

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

* The command-line interactive mode (agda -I) is no longer supported,
  but should still work.

  http://thread.gmane.org/gmane.comp.lang.agda/245

* Reload times when working on large projects are now considerably
  better.

  http://thread.gmane.org/gmane.comp.lang.agda/551

Libraries
---------

* A standard library is under development.

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary

Documentation
-------------

* The Agda wiki is better organised. It should be easier for a
  newcomer to find relevant information now.

  http://wiki.portal.chalmers.se/agda/

Infrastructure
--------------

* Easy-to-install packages for Windows and Debian/Ubuntu have been
  prepared.

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

* Agda 2.2.0 is available from Hackage.

  http://hackage.haskell.org/

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.