On Wed, Aug 5, 2015 at 12:12 PM Alan & Kim Zimmerman <alan.zimm@gmail.com> wrote:
This seems to show the syntax in agda

https://code.google.com/p/agda/issues/detail?id=1077

-- 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


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:

import qualified Relation.Binary as Setoid
...
... where
   f = Setoid.f
  g = Setoid.g
  -- and whatever other names you need from Setoid.

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.

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.