The Best Errors for Solving Dependency Versions

Details of versions and version ranges

Quick notes on conventions/terminology before we get too far in:

The actual details of how versions are tagged doesnʼt matter, just that they are totally ordered.Actually we probably donʼt even need a total order, a partial order would work fine for it? For example, it could just be flat integers for all we care. But usually we take them to be lexicographically-ordered lists of integers, like 5.0.3 which is less than 5.1.0.

How we form ranges over versions is pretty important, though, and early on the registry decided to only allow half-open intervals. That is, ranges have the form >=A.B.C <X.Y.Z, which I will use throughout this article. Again, it isnʼt very sensitive to details here (who cares that it is half-open?), but this does seem to be the right level of generality. Supporting more complex queries is asking for trouble.

Finally, from a version-solving point of view, a registry contains information of what versions of packages there are, and for each package version a record of what dependencies it requires and the appropriate version ranges for those packages. That is, it can be represented with the following PureScript datatype:

-- A list of required dependencies
-- with their version ranges
type Manifest = Map PackageName Range

-- A list of all extant package versions
type RegistryIndex =
  Map PackageName
    (Map Version Manifest)

The problem statement

Solving means taking a manifest and finding versions for each package in it, preferring later versionsThis is actually a weird requirement, since there can be incomparable solutions that need to be tie-broken arbitrarily. In practice I do it alphabetically just by dint of how the package versions are tried.:

solve
  :: RegistryIndex
  -> Manifest
  -> Either SolverErrors
      (Map PackageName Version)

Along with some correctness constraints to ensure it is the solution we want.

let r :: RegistryIndex
let m :: Manifest
let otherSol :: Map PackageName Version

-- We need the solution to solve the manifest and dependency's requirements
isASolutionFor r m (fromRight (solve r m)) &&
-- There are no strictly better versions to be found
( isASolutionFor r m otherSol
  `implies` isn'tWorseSolutionThan otherSol (fromRight (solve r m))
)
where
satisfies
  :: Map PackageName Version
  -> Map PackageName Range
  -> Boolean
satisfies sol m =
  allWithIndex
    ( \package range ->
        case Map.lookup package sol of
          Nothing -> false
          Just version -> range `includes` version
    )
    m

isASolutionFor
  :: RegistryIndex
  -> Manifest
  -> Map PackageName Version
  -> Boolean
isASolutionFor r m sol = and
  -- All packages received a version
  [ Map.keys m `isSubsetEqOf` Map.keys sol
  -- All solved versions fit into the range
  -- as required in the manifest
  , sol `satisfies` m
  -- All packages have their dependencies satisfied
  , allWithIndex
      ( \package version ->
          case Map.lookup package r >>= Map.lookup version of
            Nothing -> false
            Just deps ->
              sol `satisfies` deps
    )
    sol
  ]

isn'tWorseSolutionThan :: Map PackageName Version -> Map PackageName Version -> Boolean
isn'tWorseSolutionThan other optimal =
  Maps.keys optimal `isSubsetEqOf` Map.keys other
  && not allWithIndex
    ( \package version ->
        case Map.lookup package other of
          Nothing -> true

    )
    optimal
  -- FIXME

Dependencies are tricky

In particular, note that dependencies are associated with a particular version. A package range doesnʼt need to have well-defined dependencies at all!

This is something that we forget about when using packages in our day-to-day lives, but an algorithm needs to handle all cases we could throw at it.

Algebraic errors

In a solver algorithm, we write programs in terms of some error monad. The backtracking algorithm essentially corresponds to a complicated Boolean expression, a tree of various constraints joined with conjunction and disjunction. Thinking of it as Applicative+Alternative, we see that <*> corresponds to conjunction && and <|> corresponds to disjunction ||.

console >=5.0.0 <6.0.0

(console == 5.0.0 && prelude >=5.0.0 <6.0.0)
|| (console == 5.0.1 && prelude >=5.0.1 <6.0.0)

An error, then, is some kind of proof that the Boolean always evaluates to false. SAT solvers have done a great job of doing this in the general case. And you can think a bit about what this means.

In addition to the literal Boolean clauses, we want the errors to record some additional metadata about where they came from: particular manifests and the current dependency from the manifest we are trying to solve.

Composing relations

This quasi-transitive dependency business looks a bit like a familiar formula: the composition of two relations in logic.

The key part here is that we take our input and our output and we ask: is there something in the middle that serves to connect the input to the output? (Thinking of relations as boxes that connect certain inputs to certain outputs.)

However, we arenʼt dealing with general relations here, weʼre only dealing with half-open intervals. Weʼre asking: for a version range, what range is constructed by taking the ranges of each version in the middle?

To be a bit more direct with this analogy, a relation $R \subseteq X \times Y$ can equivalently be written as $R \in \mathcal{P}(X \times Y)$. ($\mathcal{P}(Z)$ here is the powerset monad $\mathcal{P}(Z) = Z \to \textrm{Prop}$, which consists of all subsets of the given set $Z$.) And by currying, this can be viewed as $R \in X \to \mathcal{P}(Y)$. This construction $X \to M(Y)$ for a monad $M$ is called the Kleisli category. So now the question is: do intervals also form a monad, by taking loose bounds?

The easy answer is that we can certainly think of it as an approximation on top of the underlying set-relation model. That is, we know how to make intervallic dependencies a relation, so we compose them as relations and then take the smallest interval that contains every interval we came across.

Perhaps there is a way to categorify it directly, I donʼt know. We can come up with an identity, but Iʼm not so sure that associativity would hold.

Monoids, monoids everywhere

Again, a topic for another blog post, but I love monoids, especially semilattices, because they capture information gathering in ways that lend themselves to reliable implementation.

In particular, because of their idempotence, semilattices are great because you just need to make sure you cover all cases. Thereʼs no such thing as double-counting in a semilattice computation! When youʼre dealing with a well-behaved logical scenario, if have written your logic correctly (i.e. each derivation is valid) and you cover all the cases (you eventually produce every fact you are allowed to derive), thereʼs no chance that you accidentally make things break. If the logical scenario does not have a finite upper bound of information to derive, this naïve process may not terminate, but in our case it is certainly finite: the registry itself is finite, so any logical derivations from it will eventually be saturated.

We already saw our first semilattice Semigroup (App (Map PackageName) Loose) above. However, I left out the definition of Loose and its Semigroup instance.

The data contained in Loose is just a lower bound and an upper bound, and we want the lower bound to be less than the upper bound for it to be valid. We also pack in metadata that describes where each bound came from, the SolverPosition datatype which we will discuss below in Provenance.

To achieve this, we first define a type that describes a bound with metadata packed in. Then we add to this operations that take the maximum and minimum of the bounds, and aggregate the metadata if they were the same bound. Thatʼs right, the metadata itself forms a semilattice!I cannot emphasize how key this is to a lot of the work of carrying around metadata by bundling it in with data like this.

data Sourced = Sourced Version SolverPosition

newtype MinSourced = MinSourced Sourced

instance Semigroup MinSourced where
  append a@(MinSourced (Sourced av as)) b@(MinSourced (Sourced bv bs)) =
    case compare av bv of
      LT -> a
      GT -> b
      EQ -> MinSourced (Sourced av (as <> bs))

newtype MaxSourced = MaxSourced Sourced

instance Semigroup MaxSourced where
  append a@(MaxSourced (Sourced av as)) b@(MaxSourced (Sourced bv bs)) =
    case compare av bv of
      GT -> a
      LT -> b
      EQ -> MaxSourced (Sourced av (as <> bs))

Now we get both Loose and Intersection for free by the right arrangement of these types. Heck, we even get their coercion for free:

newtype Loose = Loose
  { lower :: MinSourced
  , upper :: MaxSourced
  }
derive newtype instance Semigroup Loose

newtype Intersection = Intersection
  { lower :: MaxSourced
  , upper :: MinSourced
  }

derive newtype instance Semigroup Intersection

-- API for `Intersection`
upperBound :: Intersection -> Version
upperBound (Intersection { upper: MinSourced (Sourced v _) }) = v

lowerBound :: Intersection -> Version
lowerBound (Intersection { lower: MaxSourced (Sourced v _) }) = v

good :: Intersection -> Boolean
good i = lowerBound i < upperBound i

satisfies
  :: Version -> Intersection -> Boolean
satisfies v r = v >= lowerBound r && v < upperBound r

-- `Loose` has to be a valid interval
toLoose :: Intersection -> Maybe Loose
toLoose i | good i = Just (coerce i)
toLoose _ = Nothing

fromLoose :: Loose -> Intersection
fromLoose = coerce

Why donʼt we require Intersection to be a valid interval? As we will talk about in the next section, Intersection is the primary way we keep track of the knowledge we have learned already. Being in the business of aggregating information, we want to know all we can about the situation our solver is confronted with, and we just can accumulate knowledge by throwing it into this semilattice.

We could make taking the intersection of intervals a partially-defined operation (Intersection -> Intersection -> Either Error Intersection), but that means we have to bail out once a single intersection becomes invalid. Instead, we integrate them directly into the semilattice structure by keeping invalid intervals around and turning them into errors later (this is why we give them the metadata about provenance!). This gives us multiple errors emerging from one step for free, it is incredibly convenient.

Knowledge propagation

Figuring out the correct way to propagate known requirements kept me occupied for days. It turns out I had done it wrong the first time, so it is good I thought it over again!

Our goal is to implement solveStep here using commonDependencies (see above) and exploreTransitiveDependencies:

-- Semilattice version of `Registry`
type TransitivizedRegistry =
  SemigroupMap PackageName
    (SemigroupMap Version
      (SemigroupMap PackageName Intersection)
    )

type RRU =
  { registry :: TransitivizedRegistry
  , required :: SemigroupMap PackageName Intersection
  , updated :: TransitivizedRegistry
  }

-- | Discover one step of quasi transitive dependencies, for known requirements
-- | and the rest of the registry too.
solveStep :: RRU -> RRU

-- Key piece:
exploreTransitiveDependencies :: RRU -> RRU

The registry :: TransitivizedRegistry and required :: SemigroupMap PackageName Intersection represent the local dependencies for each package version and the global requirements of the initial manifest given to the solver, respectively. They both are purely accumulative: what goes in comes out with some more information. The additional information will simply be added dependencies and tightened bounds on existing dependencies. Provenance metadata may accumulate too (we donʼt really need to care about that, it is just along for the ride).

The other field, updated :: TransitivizedRegistry, is a bit different: it does not carry over from step to step, it only talks about what changed at the last step. This is because as weʼre keeping registry :: TransitivizedRegistry updated, we want to only calculate updates to the things that might need it.

When we first call solveStep, we treat everything as updated:

solveSeed :: RR () -> RRU
solveSeed { registry, required } = { registry, required, updated: registry }

and the process stabilizes when there are no updates:

-- | Add quasi transitive dependencies until it stabilizes (no more updates).
-- | Needs to know what was updated since it last ran.
solveSteps :: RRU -> RR ()
solveSteps r0 = go r0
  where
  go r@{ registry, required } | noUpdates r = { registry, required }
  go r = go (solveStep r)

Keeping track of what was updated is certainly the trickiest part of the whole algorithm to reason about, but there is this one nugget of insight that coalesced into the knowledge I needed to turn it into an algorithm:

-- | A package may update because its dependencies tightened, but any reverse
-- | dependencies should have already caught that update in this same tick.
-- | So what we look for is either a new transitive dependency picked up (which
-- | the parent will need to incorporate), or newly failing to solve,
-- | both of which may introduce new dependencies for reverse dependencies
-- | through the `commonDependencies` calculation.
majorUpdate :: SemigroupMap PackageName Intersection -> SemigroupMap PackageName Intersection -> SemigroupMap PackageName Intersection -> Boolean
majorUpdate (SemigroupMap required) (SemigroupMap orig) updated =
  let
    minor = { added: false, failedAlready: false, failedNow: false }

    info :: { added :: Boolean, failedNow :: Boolean, failedAlready :: Boolean }
    info = updated # anyWithIndex \package range ->
      case Map.lookup package orig of
        Nothing ->
          -- This bound may have been omitted merely because it was subsumed by
          -- a global requirement (see `addFrom`), so adding it back does not
          -- count as a major update:
          case Map.lookup package required of
            Nothing -> minor { added = true }
            Just range' -> minor { added = lowerBound range > lowerBound range' || upperBound range < upperBound range' }
        Just r -> minor { failedAlready = not good r, failedNow = not good range }
  in
    case info of
      { added: true } -> true
      { failedNow: true, failedAlready: false } -> true
      _ -> false

-- | Update package versions in the registry with their quasi-transitive
-- | dependencies, if their dependencies were updated in the last tick. The set
-- | global requirements is needed here because those are elided from the
-- | dependencies in each package version, so to tell how the local requirements
-- | updated we need need to peek at that (see `majorUpdate`).
exploreTransitiveDependencies :: RRU -> RRU
exploreTransitiveDependencies lastTick = (\t -> { required: lastTick.required, updated: accumulated (fst t), registry: snd t }) $
  lastTick.registry # traverseWithIndex \package -> traverseWithIndex \version deps ->
    let
      updateOne depName depRange = case Map.isEmpty (unwrap (getPackageRange lastTick.updated depName depRange)) of
        true -> mempty
        false -> Tuple (Disj true) (commonDependencies lastTick.registry depName depRange)
      Tuple (Disj peek) newDeps = foldMapWithIndex updateOne deps
      -- keep GC churn down by re-using old deps if nothing changed, maybe?
      dependencies = if peek then deps <> newDeps else deps
      updated = case peek && majorUpdate lastTick.required deps dependencies of
        true -> doubleton package version dependencies
        false -> mempty
    in
      Tuple updated dependencies

-- | Discover one step of quasi transitive dependencies, for known requirements
-- | and the rest of the registry too.
solveStep :: RRU -> RRU
solveStep initial =
  { required: initial.required <> moreRequired
  , registry: moreRegistry
  , updated: updated <> updatedOfReqs
  }
  where
  -- Transitivize direct requirements
  moreRequired = initial.required # foldMapWithIndex (commonDependencies initial.registry)
  -- Record updates to them
  updatedOfReqs = requirementUpdates initial moreRequired
  -- Transitivize the rest of the registry, which should be:
  --   (1) Pruned at the start to only reachable package versions
  --   (2) Only touching packages that were directly updated last round
  { updated, registry: moreRegistry } = exploreTransitiveDependencies (initial { registry = map (addFrom moreRequired) <$> initial.registry })

One simple trick for efficiency

It turns out that the algorithm is naturally efficient, with some help.

The biggest trick is using global constraints to discard redundant local constraints. That is, if the manifest you are solving already constrains prelude >=6.0.0 <7.0.0, then each package that lists that requirement or a looser one can ignore it.

-- | The key to efficiency: take information from the bounds of global
-- | requirements and add it to the local requirements of each package version
-- | in the registry, BUT remove redundant bounds as we do so.
-- |
-- | For example, if we have a global requirement `>=3.1.0 <4.0.0`, then in the
-- | registry we will keep local dependency ranges for the same package that
-- | look like `>=3.2.0 <4.0.0` or `>=3.1.0 <3.9.0` and remove ranges like
-- | `>=3.0.0 <4.0.0` or `>=3.1.0 <4.0.0` itself.
addFrom
  :: SemigroupMap PackageName Intersection
  -> SemigroupMap PackageName Intersection
  -> SemigroupMap PackageName Intersection
addFrom (SemigroupMap required) =
  over SemigroupMap $ Map.mapMaybeWithKey \package ->
    case Map.lookup package required of
      Nothing -> Just
      Just i -> \j ->
        if j `wouldUpdate` i then Just (j <> i)
        else Nothing

-- | Used in `addFrom, `wouldUpdate j i` is an optimized version of
-- | `(i <> j /= i)`.
wouldUpdate :: Intersection -> Intersection -> Boolean
wouldUpdate j i =
  lowerBound j > lowerBound i ||
  upperBound j < upperBound i

Unfortunately I had to add a bit of special casing in the propagation to handle this, in particular when checking for major updates, but the exceptional efficiency is more than worth the slight inelegance.

Provenance

Normally I like to keep full provenance to detail exactly the path a piece of data took to get through the logic. In particular, in dependently-typed languages it is really helpful to be able to trace terms through their evaluation, so that by the time you get to a type error you know exactly why those particular things popped up, not just a rough idea of where in the source they were originally found once upon a time. Especially because once separate terms are unified, you donʼt want to arbitrarily pick a location, you want to know both locations! However, it is really slick in this domain: we only need to keep track of the endpoints, users donʼt exactly care about what came in between (just that it is reasonable to assume, because it is in fact correct).

So in this case I keep track of which particular package version manifest(s) gave us the constraint we are talking about (LocalSolverPosition), and which constraints in the current manifest caused it to be required. Thereʼs some logic to combine these positions which I will not reproduce here.

data LocalSolverPosition
  -- | Dependency asked for in manifest
  = Root
  -- | Committed to a specific version
  | Trial
  -- | Required transitive dependency seen in said packages
  | Solving
      ( NonEmptySet
          { package :: PackageName
          , version :: Version
          }
      )

data SolverPosition = Pos LocalSolverPosition (Set PackageName)

It seems that it weakens the logical connection just a bit, I donʼt know if they can be put into formal properties anymore. (E.g. “Deleting the mentioned constraint from the current manifest affects it in this way.”)

But I believe it is the information that users want to see; it certainly falls into the category of making it actionable so they can fix things and run it again to make progress. In the case that it is a local error, knowing which clauses of the current manifest led to it is crucial in answering the question, “What do I need to change to fix the error”. And sometimes it is a deeper error of outdated dependencies, so you want to know what package is responsible for that incongruous version requirement.