[Haskell-cafe] Syntax extension - adding import support to let/where bindings

[Mike Meyer]

On Wed, Aug 5, 2015 at 12:12 PM Alan & Kim Zimmerman <alan.zimm at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150805/3c294e81/attachment.html>