Skip to content
{yen}

uKanren: synthesis with constraints

Some values are not written but found: a port no other app uses, memory that fits a host, a database host in the right environment. µKanren with constraints finds such values. It has logic variables, unification over attrsets, lists and scalars, and goals that run in both directions. The fleet has one host lb with three apps:

modules/fleet.nix
{ yen, ... }:
{
  yen.kinds.fleet = {
    spawns.host = _: yen.host;
    sinks.out.reduce = yen.lib.reduce.merge;
  };
  yen.kinds.host.fields.apps = yen.lib.listOf (yen.lib.is builtins.isString);


  yen.fleet.main = { };
  yen.host.lb.apps = [
    "grafana"
    "loki"
    "prometheus"
  ];
  yen.flake = { out, ... }: out;
}

Ports for the apps

Section titled “Ports for the apps”

The goal gives each app a port in 8080..8083. All ports differ, and prometheus is before grafana. The marked lines are explained below. The goals come from yen.lib.uKanren, and the table at the end of the page lists them.

modules/ports.nix
# µKanren with finite domains: give each app a port in 8080..8083, all different, prometheus before grafana.
{ yen, lib, ... }:
let
  inherit (yen.lib.uKanren) # (1)
    run
    runAll
    freshNamed
    infd
    distinctfd
    ltfd
    eq
    label
    runFuel
    ;
  ports =
    apps: q:
    freshNamed apps (vs: [
      # (2)
      (infd (lib.attrValues vs) 8080 8083) # (3)
      (distinctfd (lib.attrValues vs)) # (4)
      (ltfd vs.prometheus vs.grafana) # (5)
      (eq q vs) # (6)
      (label (lib.attrValues vs)) # (7)
    ]);
  lb.scopesOf = yen.host.lb; # a tree request: lb, with its data
  appsOf = tree: (lib.head (tree.select lb)).apps;
in
{
  yen.aspects.ports = {
    at = yen.kinds.fleet;
    cycle =
      { tree, ... }:
      {
        tree = [ lb ];
        out = [
          {
            ports = {
              first = run 1 (ports (appsOf tree)); # (8) one answer
              count = lib.length (runAll (ports (appsOf tree))); # every answer
              # (9) the same relation, run backward: which app can take 8080?
              on8080 = lib.unique (
                lib.concatMap (a: lib.attrNames (lib.filterAttrs (_: p: p == 8080) a)) (
                  runAll (ports (appsOf tree))
                )
              );
              # (10) a bounded search: `complete = false` means "stopped", never "no answer"
              bounded = removeAttrs (runFuel 1 5 (ports (appsOf tree))) [ "answers" ];
            };
          }
        ];
        errors = [ (lib.optional (run 1 (ports (appsOf tree)) == [ ]) "ports: no assignment for lb") ];
      };
  };
}

(1) takes the goals from the library. (2) makes one logic variable for each app. (3) gives every variable a finite domain of ports. (4) makes all ports differ, and (5) makes the prometheus port lower than the grafana port. (6) unifies the answer q with the variables, and (7) enumerates what is left. (8) takes one answer, and (9) reads the same relation backward. (10) is a search with fuel. The aspect is a cycle that asks the tree for lb. These are the answers:

result
{
  bounded = {
    complete = false;
  };
  count = 12;
  first = [
    {
      grafana = 8081;
      loki = 8082;
      prometheus = 8080;
    }
  ];
  on8080 = [
    "prometheus"
    "loki"
  ];
}

grafana can never take 8080: prometheus must be lower. The same relation, read backward, says so.

Goal Meaning
eq u v, fresh, freshNamed, disj, conde, project µKanren: unify, new variables, any of, clauses, read a value
neq u v u and v never unify
dom x [ … ], infd xs lo hi finite domains
lefd, ltfd, plusfd x y z, neqfd, distinctfd xs propagation over domains
label xs enumerate what is left, smallest domain first
cons, appendo, membero, fromList, toList relational lists
facto rows pattern a table of facts
run n, runAll, runC n answers for q: goal, or { x; y; } for { x, y, ... }: goal; runC adds the constraints left on fresh variables
runFuel n fuel, runAllFuel fuel, maximize fuel measure bounded search: { answers; complete; }
ContributeCommunitySponsor