AgdaLanguageReview

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).