Idris export rules inflate namespaces, Haskell rules do no. Why ?

[nicolabotta]

The Haskell program

> module MA where
> type A = Bool

> module MB where
> import MA
> type B = A

> module TestExport where
> import MB
> i :: A -> B
> i = not

does not type check because, in |TestExport|, |A| is not visible. If one wants to use |MA.A| in |TestExport|, one has to import |MA|. This is good: if the names imported by a module were automatically injected in the namespaces of its clients, name clashes would hardly be avoidable. Maintaining and refactoring programs would be a nightmare: in order to find out the modules a program might depend upon, one would have to backwards reconstruct the whole import tree. In contrast, the Idris program

> module MA
> A : Set
> A = Bool

> module MB
> import MA
> B : Set
> B = A

> module TestExport
> import MB
> i : A -> B
> i = not

type checks. This suggests that the export rules of Idris might be fundamentally different from those of Haskell. Is this the case ? Why ?

[edwinb]

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.

[nicolabotta]

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 notifications@github.com 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]

[edwinb]

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 :).

[david-christiansen]

This is wonderful!

[nicolabotta]

Edwin Brady notifications@github.com wrote:
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Sun, 14 Dec 2014 16:03:59 +0100
Message-ID: 20943.1418569439@cirrus.gutzkowa.net

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/66884545@github.com
References: idris-lang/Idris-dev/issues/111@github.com idris-lang/Idris-dev/issues/111/66884545@github.com
Comments: In-reply-to Edwin Brady notifications@github.com
message dated "Sat, 13 Dec 2014 09:47:35 -0800."

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