<div dir="ltr"><div class="gmail_quote"><div dir="ltr">On Wed, Aug 5, 2015 at 12:12 PM Alan & Kim Zimmerman <<a href="mailto:alan.zimm@gmail.com">alan.zimm@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">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></div></div></div></blockquote><div><br></div><div><br></div><div>If this is going to go into a local block of some kind, how many names are you going to use from A? How much extra work does this save over something like:</div><div><br></div><div>import qualified Relation.Binary as Setoid</div><div>...</div><div>... where</div><div>   f = Setoid.f</div><div>  g = Setoid.g</div><div>  -- and whatever other names you need from Setoid.</div><div><br></div><div>Personally, I'm not a big fan of unqualified imports - I've spent to much time trying to figure out where some variable came from in a module that just imported everything unqualified.   So I'm willing to trade a little extra work now to make sure every name not from the Prelude shows up in the imports lis in order to save time every time I have to figure it out again later.</div><div><br>I think the idea of having local imports is a win, as it means finding names is faster, as they'll be right there, instead of having to go to the imports list at the top of the page. But if I have to import the module qualified, and then pull the names I want out locally (which I will do), it's not clear that this provides a significant advantage over what we already have.</div></div></div>