Module names should be required to match filenames.

[cbiffle]

Currently, imports work in terms of file paths, but qualified references work in terms of module names. The two have no relation.

As an example, consider these two files:

Foo.idr

module Bar

value : Nat
value = 3

Bar.idr

module Foo

value : Nat
value = 4

Now consider the use of these modules:

import Foo  -- imports module "Bar"
import Bar  -- imports module "Foo"

newValue : Nat
newValue = Foo.value

What is the value of Foo.value? It is 4.

While this may seem somewhat contrived, I've run into this when rearranging a codebase. It's easy to git mv some files (possibly even permuting their names) and forget to update the module declarations.

Clearly, import must follow the filesystem; to do otherwise would require e.g. maintaining a database of which modules live where.

I suggest that the behavior of import be preserved, but the compiler reject with an error any file that

1. Contains a module declaration, and
2. Resides at a path, from the root used by import, that doesn't match its module name, per the usual dot-for-separator substitution.

Precedent in existing languages (Java, Rust, Haskell) suggests that such a requirement is unlikely to be onerous.

[enolan]

Don't you mean it's 4? Foo.value should be the value defined in the module Foo in the file Bar.idr, right? That's the whole point.

[cbiffle]

See? I even confused myself. :-)

[nicolabotta]

If one accepts the idea that file names should match module names (which I do), why do we need the module keyword at all? The argument of the import command could just be a file name. No need for "modules", no confusion because of examples like the one above.

[cbiffle]

I suppose the exception would be source files that don't declare an explicit module (which seem to automatically get named Main in the current implementation). Currently, one can name these files using characters that are illegal in Idris module names.

I think your point is interesting nonetheless.

[melted]

Clearly, import must follow the filesystem; to do otherwise would require e.g. maintaining a database of which modules live where.

Like Haskell and Rust we have package files that could serve to tell where modules are.

Precedent in existing languages (Java, Rust, Haskell) suggests that such a requirement is unlikely to be onerous.

Rust allows multiple nested modules per file, which would be impossible with this restriction. In Haskell it's also just a convention. I don't see why we couldn't handle this by convention.

I don't like locking into a module == File identity. I'd like more flexible and parameterizable modules.

Also, the title is misleading, "Module names should be required to match filenames." would require all main programs to be named Main.idr. I hope nobody is advocating that.

[nicolabotta]

I don't like locking into a module == File identity. I'd like more flexible and
parameterizable modules.

I also would like flexible and parametrizable modules. But at the moment we have:

• Import rules based on file names and name resolution rules based on module names.
• No support for multiple modules in the same file.
• No support for nested modules.
• No support for parameterized modules, flexible renaming rules, etc.
• Support for multiple namespaces in the same file.
• Support for nested namespaces.
• No support for parameterized namespaces, flexible renaming rules, etc.

On the top of this we have export modifiers, hiding directives which take specific arguments but modify the export status of whole module names, upper case and lower case conventions for implicit parameters name resolution rules ... I admit I do not fully understand the problems these constructs are designed to address but I have the impression that having module and namespacein their current form it is a bit too much. I do not really care whether the keyword is called module or namespace (although I would prefer module) but it seems to me that:

• We need only one construct, possibly parameterizable and nestable.
• The argument of an import command should be a file name.

I would not mind if name resolution conventions would require a name guga defined in a namespace Lula in a $WHATEVER_IDRIS_SEARCH_PATH/the_return_of_ZUZU/chapter1/section2/lala.idr file to have to be fully qualified (for resolving a name clash, for instance) as The_return_of_ZUZU.Chapter1.Section2.Lala.Lula.guga.

Also, the title is misleading, "Module names should be required to match filenames."
would require all main programs to be named Main.idr. I hope nobody is advocating that.

I do not advocate that but I would not have anything against that either. What is wrong with files containing main programs to be called Main.idr?

[ghost]

When I met Haskell I was annoyed by the redundancy of file and module names. To move or rename a source folder [or module name], one needs to update all the module headers in all the files in that folder recursively. It is an unnecessary inconvenience.
When I met Idris I was disappointed seeing it kept this bad habit of Haskell.
Why not just mimic Rust's solution?

[cbiffle]

@almale's comment suggests a compromise solution.

What if...

• The name of a module was, by default, taken from its filename -- like Rust.
• The module declaration was available for overriding this, for people who really really want their modules to be confusing.

Personally, I'd rather not allow for the latter (convention over configuration) and eventually unify modules and namespaces. But I thought I'd suggest it.

[nicolabotta]

Cliff L. Biffle [email protected] wrote:

@almale's comment suggests a compromise solution.

What if...

• The name of a module was, by default, taken from its filename -- like Rust.
• The module declaration was available for overriding this, for people who really really want their modules to be confusing.

Personally, I'd rather not allow for the latter (convention over configuration) and eventually unify modules and namespaces. But I
thought I'd suggest it.

What would be the benefits of overriding file names?

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

[cbiffle]

shrug Attempting to short-circuit objections like @melted's.

Though I actually think he's arguing with a strawman; I'll respond directly.

[cbiffle]

Like Haskell and Rust we have package files that could serve to tell where modules are.

True, and this could perhaps provide a back-door for people who insist on having filenames that don't match their module names. That being said, I'm not convinced that a detailed package file should be a prerequisite to a project (that is, there ought to be a default mapping from imported name to filesystem location).

Rust allows multiple nested modules per file, which would be impossible with this restriction.

I think you misunderstand what I was proposing. Banning this was certainly not my intent, and I would love to (1) allow nested modules and (2) eliminate namespaces. I didn't go into detail on the behavior of nested modules since they don't currently exist in Idris.

In the presence of nested modules, I'd rephrase my suggestion as: the top level module in a file ought to match its filename / path relative to a source root.

I don't like locking into a module == File identity. I'd like more flexible and parameterizable modules.

Me too.

Also, the title is misleading, "Module names should be required to match filenames." would require all main programs to be named Main.idr. I hope nobody is advocating that.

I'm open to suggestions for better titles, it seems much of my post misled you.

I consider Idris's assumption that the main function lives in a module called Main to be a misfeature, for the record.

[nicolabotta]

I have added three files to https://github.com/nicolabotta/SeqDecProbs/tree/master/frameworks/14-: FractionSpecification.lidr, FractionImplementationIndependentProperties.lidr and FractionNatPairImplementation.lidr.

The files are meant to provide a small but realistic example to help the current discussion on module and file names being more concrete. At the same time, I wanted to contribute to the (I believe, closely related) problem of "Where to put proofs of e.g. base?" originally initiated by Cliff on idris-lang.

The idea behind the example is that a library developer wants to implement a data type representing fractions equipped with standard operations: addition, multiplications, etc.
Instead of nosediving into an implementation, she tries first to express what she actually wants to do. She puts forwards a specification for fractions in FractionSpecification.lidr. On one hand, the specification should allow her to easily derive further properties of fractions, independently of their concrete implementation. On the other hand, she would like to take advantage of willing contributors to actually do the dirty work and implement her specification.

I have put my (dirty) contribution in FractionNatPairImplementation.lidr and a trivial example of implementation independent properties in FractionImplementationIndependentProperties.lidr. The latter does not actually type check and is meant to exemplify the need for something like "conditional" instance declarations. I think that the example is suitable to discuss a number of questions:

First, there is a problem of splitting and namegiving. Is it appropriate to split specification and implementation into different files, modules, namespaces? Considering that a given specification can, in general, be fulfilled by different implementations, splitting the two would seem quite natural. But which Idris constructs should we use to express such distinction? Modules, namespaces, type classes? Or should we rather rely on files and directory names?

Second, there is a problem of hiding directives and name resolution rules: I have initially tried to put the content of the three files in a single module and under three different namespaces and I failed. I have tried, in FractionSpecification.lidr, to replace plus and mult by (+) and (*) and I failed: I have most likely misunderstood how import and hiding directives and namespaces are meant to be used, but I seem not to be able to apply these Idris constructs in a profitable manner. For instance, I was expecting something like

> module Fraction

> %default total

> namespace Specification

>   Fraction : Type

>   ||| The numerator of a fraction
>   num : Fraction -> Nat

>   ||| The denominator of a fraction
>   den : Fraction -> Nat  

>   ||| Fraction addition
>   (+) : Fraction -> Fraction -> Fraction

>   ||| Addition preserves positivity of denominators
>   plusPreservesPositivity : (x : Fraction) -> (y : Fraction) -> 
>                             Z `LT` den x -> Z `LT` den y -> 
>                             Z `LT` den (x + y)

to allow me to specify infix addition and multiplication operators for fractions. Alas, this does not type check because (+) cannot be disambiguated. Am I missing something obvious? x and y are clearly fractions here and there is only one (+) operator in the local namespace that applies to fractions. What is ambiguous here?

Third, there is a problem of maintainability. If we split specification, implementation independent properties, implementation(s), implementation(s) dependent properties in different files or modules, we might easily end up with circular imports. On the other hand, the consequences of not making such distinction explicitely are even worse, I believe.

[ahmadsalim]

I think that import Foo should import the module named Foo.
Perhaps it would not be bad to enforce a top-level module/file name.
I will change this from Feature Request to Minor issue, since this should really be more intuitively connected, and not just some addition.