[Agda] modules named `_`

[Ulf Norell]

I would argue against that being a sensible addition for a few reasons:

- It's not a common use case. The only time I've seen open public for a
module that's just been defined is for record modules. For that you'd need
to be allowed to say
    open record R Tel : Set public where
- It saves you basically nothing (just a repeated name, and a newline I
suppose)
- It adds two new syntactic constructions that we didn't have before:
   - open before local module
   - public modifier (also using/hiding/renaming?) between telescope and
where

Compare this to 'module _'s as implemented today:
- Very common use case. I use it all the time to share argument telescopes
between multiple definitions, or simply to make left-hand sides shorter.
- Saves you coming up with a throw-away module name, and the keywords
private, open and public.
- No new syntactic constructions, just a regular module definition with
name '_'.

/ Ulf

On Sat, Sep 26, 2015 at 11:34 AM, Andreas Abel <andreas.abel at ifi.lmu.de>
wrote:

> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150926/a973eb09/attachment.html