Release notes for Agda 2 version 2.2.0

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/