<div dir="ltr"><div><div>This seems to show the syntax in agda<br><br><a href="https://code.google.com/p/agda/issues/detail?id=1077">https://code.google.com/p/agda/issues/detail?id=1077</a><br><br><pre>-- M.agda ------------
open import Relation.Binary using (Setoid; module Setoid)
open import Data.Nat        using (ℕ)

h : ℕ
h = 0

module M {α α=} (A : Setoid α α=)
  where
  open Setoid A

  f : Carrier → ℕ
  f _ = 0

  module _ (B : Set)  where
                      g : B → ℕ
                      g _ = 0
</pre>-----------------------------------------<br><br></div>I think the "open Setoid A" is the effect you are looking for<br><br></div>Alan<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Aug 5, 2015 at 7:08 PM, Evan Laforge <span dir="ltr"><<a href="mailto:qdunkan@gmail.com" target="_blank">qdunkan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Wed, Aug 5, 2015 at 9:55 AM, Oliver Charles <<a href="mailto:ollie@ocharles.org.uk">ollie@ocharles.org.uk</a>> wrote:<br>
> It makes me sad if we can't progress the language on the grounds that<br>
> people's attempts at parsing the source code themselves would break. If you<br>
> want to know all the imports, then we should be providing this information<br>
> through tools for people to consume.<br>
<br>
</span>It's not whether or not there's a tool, there already is.  It's that<br>
the tool must be more complicated.  For example, we can get imports<br>
from haskell-src-exts but it has bugs, it can be out of date, and it's<br>
slower.  Or ghc -M... which doesn't have those problems.  So maybe<br>
it's not really a serious objection.<br>
<span class=""><br>
>> On the other hand, lots of languages have a "local open" feature like<br>
>> this.  I think many of them make you first import the module, and then<br>
>> you can "open" it in a local scope.  This would address both my "parse<br>
>> the whole file for imports" objection and the "what about instances",<br>
>> because module importing would be unchanged.<br>
><br>
> Indeed, this could be a path forward. I'm not really familiar with any<br>
> languages that do this, could you link to some examples of how this works in<br>
> other languages?<br>
<br>
</span>I was thinking of agda.. though it's only from memory so I could be<br>
wrong.  Or perhaps it was cayenne... one of those dependently typed<br>
languages models modules as records, and then has syntax to dequalify<br>
record access.  Rust has a full-on nested module system, but I seem to<br>
recall you have to declare a link dependency on an external crate<br>
("import"), and then separately import the symbols from it ("use").<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>