[Agda] Re: Replacement of 'as' in module statements?

[Nils Anders Danielsson]

On 2012-10-18 10:17, Andreas Abel wrote:
> I have implemented the new syntax
>
>    open import ModulePath arg1 .. argn directives
>
> which is equivalent to
>
>    import ModulePath
>    open module ModulePath arg1 .. argn directives

(You can't write the latter if ModulePath is qualified, right?)

I just mentioned on the bug tracker that the semantics

   import ModulePath as <Fresh>
   private
     open module ModulePath = <Fresh> arg1 ... argn directives

might be nicer. Reason: This would mean that I could replace horrible
hacks like

   private
     module M where
       import M; open M x public
   open M using (f)

   ... M.g ...

(which I use fairly often) with readable code:

   open import M x using (f)

   ... M.g ...

Perhaps this semantics is a bit too complicated, though.

> The drawback is that the 'import' is not adjacent to the thing that is
> imported.

Yes, IMO that's not so nice.

> 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

These don't mean the same thing: "import MP as M" doesn't create any new
modules, whereas "module M = import MP" introduces a new, exported
module M. One could use

   private
     module M = import MP,

but that's rather bulky.

-- 
/NAD