[Agda] A question of terminology

[Andreas Abel]

First of all, thanks to Dominique for adding type-class like features to 
Agda, and to coming to AIM XIII to explain them to us!!

The preliminary name for this feature "non-canonical implicit 
arguments", is a no-go in the context of dependent type theory. 
Canonicity already has its fixed meaning.  The term "implicit arguments" 
has also its ambiguities and should be avoided, speaking of "hidden 
arguments" instead.

So I am proposing

   instance arguments

for the new features.  This is accordance with Haskell class instances 
and with instances in the context of Coq canonical structures. See, 
e.g., beginning of section 2.1 in

   http://software.imdea.org/~aleks/papers/lessadhoc/paper.pdf

If no one shouts, I will adjust the terminology in the Agda release 
notes very soon.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/