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

[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

-----------------------------------------

I think the "open Setoid A" is the effect you are looking for

Alan

On Wed, Aug 5, 2015 at 7:08 PM, Evan Laforge <qdunkan at gmail.com> wrote:

> On Wed, Aug 5, 2015 at 9:55 AM, Oliver Charles <ollie at ocharles.org.uk>
> wrote:
> > It makes me sad if we can't progress the language on the grounds that
> > people's attempts at parsing the source code themselves would break. If
> you
> > want to know all the imports, then we should be providing this
> information
> > through tools for people to consume.
>
> It's not whether or not there's a tool, there already is.  It's that
> the tool must be more complicated.  For example, we can get imports
> from haskell-src-exts but it has bugs, it can be out of date, and it's
> slower.  Or ghc -M... which doesn't have those problems.  So maybe
> it's not really a serious objection.
>
> >> On the other hand, lots of languages have a "local open" feature like
> >> this.  I think many of them make you first import the module, and then
> >> you can "open" it in a local scope.  This would address both my "parse
> >> the whole file for imports" objection and the "what about instances",
> >> because module importing would be unchanged.
> >
> > Indeed, this could be a path forward. I'm not really familiar with any
> > languages that do this, could you link to some examples of how this
> works in
> > other languages?
>
> I was thinking of agda.. though it's only from memory so I could be
> wrong.  Or perhaps it was cayenne... one of those dependently typed
> languages models modules as records, and then has syntax to dequalify
> record access.  Rust has a full-on nested module system, but I seem to
> recall you have to declare a link dependency on an external crate
> ("import"), and then separately import the symbols from it ("use").
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150805/581e69fd/attachment.html>