Should Idris support versioning of packages?

[jfdm]

We may want to consider supporting the versioning of packages. This will be useful when constructing an Idris package manager and help towards resolving dependancy issues.

Some, issues to consider:

1. How different versions should be indicated:
   • Explicit version numbers?
   • Commit hashes if building from a DCVS?
2. How package versions should be specified at the command line and in iPKG files.
3. How to specify ranges and min versions?
4. Selection of dependancies to satisfy build constraints.
5. Should there be a register of active packages?
6. What other issues are there?

Note parts of this issue may be 'resolved' in the future depending on how modules are implemented.

[LeifW]

Thanks for writing this up!
My idea for a minimalist start for a package manager would be to extend the ipkg install command to allow referencing a git url besides just a local foo.ipkg file; and allow that to additionally specify branch / tag / hash. After that, add something to the .ipkg format allowing libs to specificy such urls as deps (perhaps converting to YAML in the process).

As far as version numbers / ranges: I'm a bit unhappy with how this works out currently on hackage, that is, requiring package authors to guess at some dep ranges in their package description, and hope they guessed right and that upstream packagers adhere to a convention of not breaking the parts of the API they use in minor version bumps.
My suggestions would be to just allow "latest" or pin to say a specific hash in the meantime (before allowing some kind of auto-choosing amongst ranges and throwing a SAT solver at it), until some more thought has been put into the above issue. Perhaps use a checksum of the type sigs exposed in the public API? A range populated by whitelisted versions built + tested on a CI server?

[worldsayshi]

Here's a crazy idea: Move the dependency graph out of the packages. As I see it, the stackage approach is halfway there. This could open up for true dependency injection.

The packages themselves are only allowed to hint at what packages they need - they should describe what requirements they put on such dependencies but does not point out particular dependencies/versions. It should be possible to generate this requirements description mostly automatically by looking at what the current package declares as imports.

A separate entity - a dependency configuration - declares how dependencies are pieced together concretely. A dependency declaration can be handled completely independently from the packages themselves and can be version controlled. Here we can compare the stackage approach. Stackage maintains a list of dependencies that have been proven to build together.

Finally - you can release a default dependency configuration with your package. But it becomes optional. One possible way of building your package.

[be5invis]

In node.js we simply write conditions in package.json and, if there is any conflict, two version of packages will be installed side-by-side, and downstreams simply require the different thing. This is a good solution for a language without namespaces.
However Idris have a global namespace tree...

[mitchmindtree]

Rust's package manager cargo is one of the nicest I've used for a programming language. While it supports git and path dependencies, it primarily revolves around a central package repository called crates.io which requires that all packages use semantic versioning, e.g. MAJOR.MINOR.PATCH where

• MAJOR is incremented when you make incompatible API changes,
• MINOR is incremented when you add functionality in a backwards-compatible manner, and
• PATCH is incremented when you make backwards-compatible bug fixes.

You can find more details on semantic versioning here.

This allows cargo to provide a cargo update command which automatically updates all dependencies to the latest, non-breaking changes for each package in the user's dependency list.

Enforced Semver?

One common issue with cargo however is that these semantic versioning rules are not enforced, so occasionally a breaking change might slip through into a MINOR or PATCH release, breaking downstream crates.

I'd love to see an Idris package manager that attempts to solve this by enforcing the versioning rules. Specifically, if any part of the public API of an Idris package is changed in a way that might break downstream usage, the package manager disallows publishing the package until a newer version is specified, perhaps with a message along the lines of:

You are attempting to publish a MINOR version update (`3.11.0` -> `3.12.0`), however Idris
has discovered the following backwards-incompatible changes:

------------------------------------------------------------
Main.Idr - L250:

    The signature of the public function:

        Bar : Int -> String

    was changed to:

        Bar : Double -> String
------------------------------------------------------------

Would you like to change the version to `4.0.0` and continue publishing (Y/n)?

Or something similar.

This would probably have to be limited to some best-effort, limited scope of API changes like "public data and function signature changes only". I imagine this might work better in Idris than other languages though due to its rich type system!

Immutability

Another benefit of cargo and its central package repository is providing package immutability. Packages published to crates.io cannot be removed, greatly reducing the chance of downstream packages mysteriously breaking for reasons like this. That said, I'm not sure what happens if legal action is taken (e.g. a package violates some copyright or something).

[ahmadsalim]

@mitchmindtree If you are thinking of contributing updates to the package manager you are welcome to. I think the features you are suggesting sound exciting, and of course you are welcome to add the changes incrementally.

I do not like the idea that packages can not be removed, since I can think of plenty of legitimate reasons to keep the feature.

[ahmadsalim]

@mitchmindtree As w.r.t to backwards compatability and enforced semver, this might not be trivial to detect. You are welcome to propose an algorithm of course, but you could e.g. change Bar : Int -> String to Bar : Num a => a -> String which is perfectly backwards compatible.

Perhaps, it can be strongly suggested changes, but not necessarily enforced (i.e., the tool can list possibly breaking changes).

[mitchmindtree]

I do not like the idea that packages can not be removed, since I can think of plenty of legitimate reasons to keep the feature.

@ahmadsalim Ah true, I should have elaborated on this: although you can't completely remove packages, cargo allows you to "yank" packages. Here's the description:

Occasions may arise where you publish a version of a crate that actually ends up being broken for one reason or another (syntax error, forgot to include a file, etc.). For situations such as this, Cargo supports a “yank” of a version of a crate.

$ cargo yank --vers 1.0.1
$ cargo yank --vers 1.0.1 --undo

A yank does not delete any code. This feature is not intended for deleting accidentally uploaded secrets, for example. If that happens, you must reset those secrets immediately.

The semantics of a yanked version are that no new dependencies can be created against that version, but all existing dependencies continue to work. One of the major goals of crates.io is to act as a permanent archive of crates that does not change over time, and allowing deletion of a version would go against this goal. Essentially a yank means that all projects with a Cargo.lock will not break, while any future Cargo.lock files generated will not list the yanked version.

[peacememories]

Is there any progress on package management in Idris? I'm very interested in the language and its features, but I'm wary of lacking tooling/ecosystem.

[jdevuyst]

Idris has several features that can cause imports to break very easily.

Use of unqualified names is one issue. You could have a file file.idr that imports packages A and B and makes use of a function foo, which the compiler resolves for you as A.foo. Suppose that you then upgrade your packages and find that B also added a function foo with the same signature as A.foo. file.idr will now fail to compile.

The above problem can be solved by disallowing unqualified names. However, a similar problem exists when it comes to finding interface implementations.

Auto implicits and elaborator reflection may rely on the environment in even more subtle ways.

What I conclude from this is that semantic versioning cannot guarantee that imports won't break. This makes it enticing to depend on a specific version of a package.

---

If packages depend on specific versions of their dependencies, then what do we do when two packages a and b rely on different versions of a package c?

In NPM fashion we could import two versions of c. Idris doesn't support this out of the box, but it seems like it should be possible to get this behavior by making a physical copy of c—call it c2—and then renaming all namespaces in c2 as well as all mentions of these namespaces in b.

So if we have this:

-- Suppose packages a, b, c provide namespaces A, B, C with the following content
A.T : Type
B.f : A.T
C.g : A.T -> Nat

Then this would be rewritten as:

b_A.T : Type
c_A.T : Type
B.f : b_A.T
C.g : c_A.T -> Nat

However, functions like h will fail to compile:

h : Nat
h = g . f

In the case where T has access public export the compilation problem can be solved by adding implicit functions that convert between b_A.T and c_A.T. I’m not sure if there’s any way to solve this for the general case though.

---

TL;DR. It strikes me that managing dependencies in languages like Idris will be particularly challenging.

Warning: Sci Fi musings ahead

Having looked at some of the problems that some of Idris’s features pose, let’s look at some of Idris’s strengths:

1. We have a neat IDE protocol that allows us to gather useful information about our code.
2. We have strong types that can make us feel comfortable about refactoring code without breaking things.

This makes me think that we could add scripts to our IDE for handling potential conflicts between packages:

• There could be an ‘upgrade package’ action that would first record the fully qualified names of all identifiers. It would then upgrade the selected package. Afterwards it resolves ambiguities by inserting fully qualified names and implicit parameters where required.
• When h first fails to compile, the IDE could propose to add some implicit conversions. If access does not permit such a solution, it explain the issue to the user or it could recommend other options.

Roughly, I’m proposing this:

• Exact versions of dependencies
• Patching of dependencies to resolve package incompatibilities
• (IDE) scripts to help user install and upgrade dependencies