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

Nils Anders Danielsson nad at chalmers.se
Thu Oct 18 14:55:09 CEST 2012

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>
     open module ModulePath = <Fresh> arg1 ... argn directives

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

     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

     module M = import MP,

but that's rather bulky.


More information about the Agda mailing list