Idiom for 'import qualified' / 'import ... as'?

[Cliff L. Biffle]

When working with modules with similar shapes but different purposes, I find myself reaching for this Haskell idiom:

import qualified Data.Map as M

Data.Map is a good example: its names deliberately collide with the operations on lists, for familiarity, and are designed to be used qualified.

Similarly, in Agda, I see people doing this:

private module M = The.Real.Module

What's the closest equivalent in Idris?  (I realize that overloading makes this a little less critical in Idris, but I do occasionally need to qualify names.)

Apologies if I missed this in the FAQ.

-Cliff L. Biffle

[David Christiansen]

You can say

import Data.Fin as F

Then F.name will refer to Data.Foo.name instead.

/David

On 14/09/15 16:39, Cliff L. Biffle wrote:
> When working with modules with similar shapes but different purposes, I
> find myself reaching for this Haskell idiom:
>
> import qualified Data.Map as M
>
>
> Data.Map is a good example: its names deliberately collide with the

> operations on lists, for familiarity, and are /designed/ to be used

> qualified.
>
> Similarly, in Agda, I see people doing this:
>
> private module M = The.Real.Module
>
>
> What's the closest equivalent in Idris? (I realize that overloading
> makes this a little less critical in Idris, but I do occasionally need
> to qualify names.)
>
> Apologies if I missed this in the FAQ.
>
> -Cliff L. Biffle
>

> --
> You received this message because you are subscribed to the Google
> Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to idris-lang+...@googlegroups.com
> <mailto:idris-lang+...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.

[Cliff L. Biffle]

On Mon, Sep 14, 2015 at 7:52 AM, David Christiansen <da...@davidchristiansen.dk> wrote:

You can say

import Data.Fin as F

Then F.name will refer to Data.Foo.name instead.

Fabulous, I must have missed this in the docs.  Thanks David!

[Jan de Muijnck-Hughes]

Cliff;

You haven’t missed it in the docs, as I am sure it is an undocumented feature. I was not even aware of it ;-)

Jan

> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Cliff L. Biffle]

On Mon, Sep 14, 2015 at 10:09 AM, Jan de Muijnck-Hughes <j.demuij...@gmail.com> wrote:

Cliff;

You haven’t missed it in the docs, as I am sure it is an undocumented feature. I was not even aware of it ;-)

Thanks, Jan.

I've just taken a crack at adding it to the docs, but the right place isn't obvious to me.  There's:

1. The tutorial, which discusses imports, but also seems like the wrong place for an exhaustive list of features!
2. The "syntax reference", which doesn't mention imports at all.

My inclination is to add it to the syntax reference, but I wonder if it's so bare for a reason -- is the team worried that the syntax is changing too fast to reasonably document, or...?

[David Christiansen]

> My inclination is to add it to the syntax reference, but I wonder if
> it's so bare for a reason -- is the team worried that the syntax is
> changing too fast to reasonably document, or...?

It's not intentionally bare - it's merely bare because we haven't yet
gotten to it. Adding a section on imports and documenting this there
seems like exactly the right place.

Thanks so much!

/David

[Cliff L. Biffle]

On Mon, Sep 14, 2015 at 11:39 PM, David Christiansen <da...@davidchristiansen.dk> wrote:

It's not intentionally bare - it's merely bare because we haven't yet
gotten to it. Adding a section on imports and documenting this there
seems like exactly the right place.

I've taken a crack at it and sent a pull request.  Feedback greatly appreciated.