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

Mike Meyer mwm at mired.org
Wed Aug 5 17:31:12 UTC 2015

On Wed, Aug 5, 2015 at 12:12 PM Alan & Kim Zimmerman <alan.zimm at gmail.com>

> 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

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

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>

More information about the Haskell-Cafe mailing list