Agda Language Review

We will have an Agda language review at Chalmers on Wed Sep 26, 2007.

The review focuses on

  • the language, not libraries/applications.
  • existing features, not open-ended feature requests.
  • the language specification, not implementation details (bugs).
  • concrete issues based on experience with the Agda implementation.

Issues which may be discussed (please add more suggestions here, and make existing points more concrete):

Implicit syntax
Visibility and evaluation
(abstract keyword, etc.)
Module system
(allowing "ambiguous" names that have the same definitions, etc.)
Inductive Families
Uniqueness of identity proofs (inductive families).