Idris export rules inflate namespaces, Haskell rules do no. Why ? about idris-dev HOT 5 CLOSED

Hmm, I haven't really thought so much about import/export rules. It is to do with the way import works, which I know to be broken in some (easily fixable) ways.

I'll have a think about how to do it properly, though I probably can't do it very quickly. The behaviour you're seeing is definitely wrong.

from idris-dev.

Maybe it is not a problem if names which are defined in modules which
are imported by imported modules are resolved and can be addressed
without full qualification.

But I think in this case the programmer needs some form of control.
Maybe a "-noautoexport" or a user settable "nameresolutiondepth" ?

Edwin Brady [email protected] wrote:

Hmm, I haven't really thought so much about import/export rules. It is
to do with the way import works, which I know to be broken in some
(easily fixable) ways.

I'll have a think about how to do it properly, though I probably can't
do it very quickly. The behaviour you're seeing is definitely wrong.

—
Reply to this email directly or view it on GitHub.
[Xa8jSg8hAG_XCIX7_YoUpRXz5UHBHTwiX9khz7iuyV7CyTEXymXfI42r0PdrtUxJ.gif]

from idris-dev.

The default is now that imported modules are not automatically reexported, and you need to say "import public A" if that's the behaviour you want (which is exactly the old behaviour). This might break a few things, but I think the new way is better, and what you were looking for.

Sorry to take 2 years over this. At least it's evidence I get back to things eventually :).

from idris-dev.

This is wonderful!

from idris-dev.

Edwin Brady [email protected] wrote:
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Sun, 14 Dec 2014 16:03:59 +0100
Message-ID: [email protected]

The default is now that imported modules are not automatically
reexported, and you need to say "import public A" if that's the
behaviour you want (which is exactly the old behaviour). This might
break a few things, but I think the new way is better, and what you
were looking for.

Thanks a lot Edwin, this is great news ! Best, Nicola

Sorry to take 2 years over this. At least it's evidence I get back to
things eventually :).

—
Reply to this email directly or view it on GitHub.*

Fcc: +outbox
Subject: Re: [Idris-dev] Idris export rules inflate namespaces, Haskell rules do no. Why ? (#111)
In-reply-to: idris-lang/Idris-dev/issues/111/[email protected]
References: idris-lang/Idris-dev/issues/[email protected] idris-lang/Idris-dev/issues/111/[email protected]
Comments: In-reply-to Edwin Brady [email protected]
message dated "Sat, 13 Dec 2014 09:47:35 -0800."

X-Mailer: MH-E 8.3; nmh 1.5; GNU Emacs 23.4.1

from idris-dev.