[Agda] A question of terminology

[Dominique Devriese]

Thorsten,

2011/4/29 Thorsten Altenkirch <txa at cs.nott.ac.uk>:
>> * The generated RecordWithImplicits modules have been removed because
>> they caused a significant performance increase of type checking. The
>> problem was that the modules were generated and kept in memory for
>> every record in the standard library, even if they were not needed.
>> As I discussed in my talk in AIM XIII, the modules can be defined
>> relatively easily by the user as follows:
>>
>> module RecordWithImplicits {args : Ts} {{rec : Record Ts}} = Record rec
>
> I thought this was a nice feature, maybe it can be switched on via a pragma?

I also think it's a pity that it was removed (even though the
workaround is not extremely long). I have been working a bit on an
alternative that only generates the RecordWithImplicits module
on-demand. I have an experimental version of Agda which takes the
syntax

   import Record {{...}}

(this is unambiguous because "..." is reserved for with patterns, and
illegal there)
and basically translates it into

   module RecordWithImplicits {args : Ts} {{rec : Record Ts}} = Record rec

You can also write
    open import Record {{...}}
or  import Record {{...}} <import-directive>

This doens't have the performance problem of the previous solution,
and also gets rid of the arbitrary "...WithImplicits" name. However,
I'm not fully happy with this either, because the syntax feels a bit
ad hoc, and the implementation is relatively heavy (new "concrete"
"Nice" and "abstract" syntax, with a lot of extra boilerplate code).
The heaviness basically comes from the fact that I can only figure out
the needed arguments during type-checking. I'm thinking about
simplifying it somewhat, by dropping the 'import' and making the
syntax into a separate case of normal section applications, something
like
  module RecordWithImplicits = Record {{...}}
and
  open Record {{...}}
This could also allow me to simplify the code a bit, by generalising
normal ModuleMacro's.

Comments and suggestions are welcome.

Dominique