Replacement of 'as' in module statements? [Re: [Agda] Some module statements, for your amusement]

[Andreas Abel]

I have implemented the new syntax

   open import ModulePath arg1 .. argn directives

which is equivalent to

   import ModulePath
   open module ModulePath arg1 .. argn directives

On 17.10.12 9:17 AM, Andreas Abel wrote:
> Valid Agda:
>
>    open import Issue481PonderBase
>    open import Issue481PonderImportMe as as
>
>    module Issue481PonderMaster where
>
>    module M = as as as
>
> Potential future Agda will shorten this to:
>
>    open import Issue481PonderBase
>    open import Issue481PonderImportMe as as as M

This is not supported, 'as' and module arguments cannot be mixed (at 
least I could not get this to work).

Wolfram suggests the syntax

   open import M = ModulePath args

which would avoid the potential of confusing args with an 'as' clause:

   open import M = Issue481PonderImportMe as as

The drawback is that the 'import' is not adjacent to the thing that is 
imported.  That could be remedied by.

   open [module] M = import ModulePath args
   module M = import ModulePath args

The current

   import MP as M
   open import MP as M

could be deprecated in favor of

   module M = import MP
   open M = import MP

'import MP' would then just mean MP with side effect of importing MP 
first.  As standalone

   import MP

is short for

   module MP = import MP

Since we have module definitions in Agda, '=' makes more sense than 
Haskell's 'as'.

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/