<div dir="ltr">I would argue against that being a sensible addition for a few reasons:<div><br></div><div>- 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</div><div> open record R Tel : Set public where</div><div>- It saves you basically nothing (just a repeated name, and a newline I suppose)</div><div>- It adds two new syntactic constructions that we didn't have before:</div><div> - open before local module</div><div> - public modifier (also using/hiding/renaming?) between telescope and where</div><div><br></div><div>Compare this to 'module _'s as implemented today:</div><div>- 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.</div><div>- Saves you coming up with a throw-away module name, and the keywords private, open and public.</div><div>- No new syntactic constructions, just a regular module definition with name '_'.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Sep 26, 2015 at 11:34 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think _-modules make sense the way they are now. One could think of adding a syntax like<br>
<br>
open module M tel [public] where<br>
<br>
but it adds little. Basically, is saves you from writing the module name twice, as in<br>
<br>
module M tel where<br>
<br>
open M public<br>
<br>
It might still be a sensible small addition to the language.<br>
<br>
Cheers,<br>
Andreas<div class="HOEnZb"><div class="h5"><br>
<br>
On <a href="tel:25.09.2015%2020" value="+12509201520" target="_blank">25.09.2015 20</a>:36, David Darais wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello list,<br>
<br>
I have a proposal concerning modules named `_`.<br>
<br>
What do you think this module does?<br>
<br>
module OuterModule where<br>
module _ (A : Set) where<br>
foo : A → A<br>
foo x = x<br>
module _ (A : Set) where<br>
foo : A → A<br>
foo x = x<br>
<br>
Agda doesn't accept this, saying `foo` is already defined.<br>
<br>
It looks like:<br>
<br>
module _ (A : Set) where<br>
foo : A → A<br>
foo x = x<br>
<br>
is being desugared to something like:<br>
<br>
module unique$123 (A : Set) where<br>
foo : A → A<br>
foo x = x<br>
open unique$123 public<br>
<br>
I consider this slightly strange behavior for someone who doesn't know this<br>
magical desugaring, particularly for sibling modules named `_`.<br>
<br>
What are your thoughts on requiring/allowing `open public` at the end of a<br>
parameter list, or somewhere else, to indicate that the contents of a module<br>
should be immediately opened after its definition? Something like:<br>
<br>
module _ (A : Set) open public where<br>
foo : A → A<br>
foo x = x<br>
<br>
This would also allow for the "open after definition" functionality for named<br>
modules, or the ability to open an unnamed module without the public modifier.<br>
Also it would remove the confusion about what a module with name `_` means.<br>
`module _` would then just introduce a unique name, which is a little less<br>
surprising, and the flavor of automatic opening would be make explicit.<br>
<br>
Cheers,<br>
David<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a></font></span><div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>