On Wed, Aug 5, 2015 at 12:12 PM Alan & Kim Zimmerman
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.