[Agda] modules named `_`

[Andreas Abel]

I think _-modules make sense the way they are now.  One could think of 
adding a syntax like

   open module M tel [public] where

but it adds little.  Basically, is saves you from writing the module 
name twice, as in

   module M tel where

   open M public

It might still be a sensible small addition to the language.

Cheers,
Andreas

On 25.09.2015 20:36, David Darais wrote:
> Hello list,
>
> I have a proposal concerning modules named `_`.
>
> What do you think this module does?
>
>      module OuterModule where
>        module _ (A : Set) where
>          foo : A → A
>          foo x = x
>        module _ (A : Set) where
>          foo : A → A
>          foo x = x
>
> Agda doesn't accept this, saying `foo` is already defined.
>
> It looks like:
>
>      module _ (A : Set) where
>        foo : A → A
>        foo x = x
>
> is being desugared to something like:
>
>      module unique$123 (A : Set) where
>        foo : A → A
>        foo x = x
>      open unique$123 public
>
> I consider this slightly strange behavior for someone who doesn't know this
> magical desugaring, particularly for sibling modules named `_`.
>
> What are your thoughts on requiring/allowing `open public` at the end of a
> parameter list, or somewhere else, to indicate that the contents of a module
> should be immediately opened after its definition? Something like:
>
>      module _ (A : Set) open public where
>        foo : A → A
>        foo x = x
>
> This would also allow for the "open after definition" functionality for named
> modules, or the ability to open an unnamed module without the public modifier.
> Also it would remove the confusion about what a module with name `_` means.
> `module _` would then just introduce a unique name, which is a little less
> surprising, and the flavor of automatic opening would be make explicit.
>
> Cheers,
> David
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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