Clarificaiton on relation between Inigo namespaces and Idris module names

[bbarker]

From the examples, it looks as though the namespaces (e.g. "Base") is part of a module name, but it seems like this might not be ideal, since my understanding is there is a single user to single namespace relation, but multiple users may wish to upload packages to e.g. "Data" or "Control.Monad" for instance. I don't think this is actually the case, but just wanted to check to be sure. So as an example, say you were running inigo init for a package Control.Monad.X - how would you complete the inigo init command?

[bbarker]

Actually, my main point of confusion is how module names work, which may be more of an issue with my understanding of Idris modules, because doing e.g. doesn't work:

[nix-shell:~/workspace/TypeAlignedSeqs]$ inigo init bebarker Data.TASequence
Initializing new inigo application bebarker.Data.TASequence from template base skeleton with tests
Successfully built BaseWithTest

[nix-shell:~/workspace/TypeAlignedSeqs]$ ls
Data.TASequence.idr  Inigo.toml  Test

[nix-shell:~/workspace/TypeAlignedSeqs]$ inigo exec
Uncaught error: Parse error (Parse error: Expected package name (next tokens: [DotSepIdentifier: Data.TASequence, DotSepIdentifier: modules, Equals, DotSepIdentifier: Data.TASequence, DotSepIdentifier: depends, Equals, DotSepIdentifier: contrib, Separator, DotSepIdentifier: idris2, DotSepIdentifier: sourcedir]))
Executing Data.TASequence with args []...
internal/modules/cjs/loader.js:638
    throw err;
    ^

Error: Cannot find module '/home/brandon/workspace/TypeAlignedSeqs/build/exec/Data.TASequence'
    at Function.Module._resolveFilename (internal/modules/cjs/loader.js:636:15)
    at Function.Module._load (internal/modules/cjs/loader.js:562:25)
    at Function.Module.runMain (internal/modules/cjs/loader.js:831:12)
    at startup (internal/bootstrap/node.js:283:19)
    at bootstrapNodeJSCore (internal/bootstrap/node.js:623:3)

However, it seems like "." is supported in module names in the docs: https://idris2.readthedocs.io/en/latest/tutorial/modules.html

I think the issue is that the file Data.TASequence.idr is created instead of Data/TASequence.idr, but in this latter case, we would need e.g. Main.idr to import and run it I suppose.

[hayesgm]

It's a design choice that I'm happy to reconsider. The hope is that you could build a package like JSON and then build files like:

module JSON

public export
parse : String -> Maybe JSONDoc
parse =
  -- ...

as opposed to:

module Hayesgm.JSON

-- ...

which I felt would feel like a strange experience from a user's perspective building packages.

You publish a package to Hayesgm (your namespace) and user's add a dep on Hayesgm.JSON=~1.0.0 and then in their project they just use JSON, which, I agree, might conflict between packages.

It was hard to convince Idris to properly namespace packages automatically, and I had a requirement that I didn't want to require changes to Idris core for this project (at its inception). Happy to rethink this strategy, but the current idea is:

Namespaces = "Single Non-Dotted Word with a Capital Letter" = E.g. "Base" or "Thomas" Packages = Built without consideration of namespaces

Once packages are posted (via Inigo.toml) they are pushed and pulled via namespace, but act independently of that once used in your project.

Again, happy to discuss if this is right.

FWIW, we do a little weirdness where we compile packages separately to enforce isolation (and allow them to live in the Deps directory), which is why you're seeing that error. We could definitely work on allowing dots in namespaces, but I'd rather resolve the overarching issue if you think it seems strange.

[bbarker]

Thanks for the clarification! I don't want to jump the gun, so with this description in mind I'll continue to use it as-is for now, and post back here once I've had a chance to use it more (or you can feel free to close this for now). Your intuition may well be right; I'm just more used to the "."-delimited namespaces, but that doesn't mean it is better.