hello nixperts 
,
i tried to naively translate microkanren
to solve the zebra puzzle in nix.
very important for packaging (/s).
flake.nix
{
description = "solve zebra puzzle with microkanren in nix";
inputs = {
nixpkgs.url =
"github:NixOS/nixpkgs/10069ef4cf863633f57238f179a0297de84bd8d3";
};
outputs = { self, nixpkgs, ... }: {
microkanren = with nixpkgs.lib;
# http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
let
# logic variables
mkVar = int: { __Var = int; };
isVar = term: term ? __Var;
eqVar = a: b: a == b;
# arrays (instead of pairs)
isArray = term: (isList term) && (term != [ ]);
# substitutions
occurs-check = var: val: sub:
let v = walk val sub;
in if isVar v then
eqVar v var
else if isArray v then
occurs-check var (head v) sub || occurs-check var (tail v) sub
else
false;
extendSub = var: val: sub:
if occurs-check var val sub then
false
else
sub // { ${toString var.__Var} = val; };
emptySub = { };
# unification
walk = term: sub:
let
lookup = var: sub: sub ? "${toString var.__Var}";
binding = if isVar term then lookup term sub else false;
in if binding then walk (sub."${toString term.__Var}") sub else term;
unify = A: B: sub:
let
a = walk A sub;
b = walk B sub;
in if (isVar a) && (isVar b) && (eqVar a b) then
sub
else if (isVar a) then
extendSub a b sub
else if (isVar b) then
extendSub b a sub
else if (isArray a) && (isArray b) then
let
headSub = unify (head a) (head b) sub;
tailSub = unify (tail a) (tail b) headSub;
in (if headSub != false then tailSub else false)
else if (a == b) then
sub
else
false;
# logic stream
emptyState = {
sub = emptySub;
counter = 0;
};
isEmptyStream = x: x == { };
isImmatureStream = x: x ? force;
delay = x: { force = x; };
mzero = { };
unit = state: {
head = state;
tail = mzero;
};
mplus = s1: s2:
if (isEmptyStream s1) then
s2
else if (isImmatureStream s1) then
delay (mplus s2 s1.force)
else {
inherit (s1) head;
tail = mplus s1.tail s2;
};
bind = stream: goal:
if (isEmptyStream stream) then
mzero
else if (isImmatureStream stream) then
delay (bind stream.force goal)
else
mplus (goal stream.head) (bind stream.tail goal);
# single constraint
eqq = a: b: state:
let sub = unify a b state.sub;
in if sub != false then
unit {
inherit sub;
inherit (state) counter;
}
else
mzero;
# core goals
disj-i = g1: g2: state: mplus (g1 state) (g2 state);
conj-i = g1: g2: state: bind (g1 state) g2;
conj = goals:
if (length goals) == 1 then
head goals
else
conj-i (head goals) (conj (tail goals));
disj = goals:
if (length goals) == 1 then
head goals
else
disj-i (head goals) (disj (tail goals));
conde = clauses: disj (map (clause: conj clause) clauses);
fresh = f: state:
let
vars = foldlAttrs (acc: n: v: {
counter = acc.counter + 1;
vars = acc.vars // { ${n} = mkVar acc.counter; };
}) {
counter = state.counter;
vars = { };
} (functionArgs f);
in (conj (f vars.vars)) {
inherit (state) sub;
inherit (vars) counter;
};
# stream helpers
pull = stream:
if isImmatureStream stream then pull stream.force else stream;
take-all = Stream:
let stream = pull Stream;
in if stream == { } then
[ ]
else
[ stream.head ] ++ (take-all stream.tail);
take = num: Stream:
if num == 0 then
[ ]
else
let stream = pull Stream;
in if isEmptyStream stream then
[ ]
else
[ stream.head ] ++ (take (num - 1) stream.tail);
# reify
mkReify = vars: states: map (reify-state-vars vars) states;
reify-state-vars = vars: state:
let mkVal = n: walk-h (mkVar n) state.sub;
in (foldlAttrs (acc: n: v:
let val = mkVal acc.counter;
in {
counter = acc.counter + 1;
vars = acc.vars // {
${n} = walk-h val (reify-sub val emptySub);
};
}) {
counter = 0;
vars = { };
} vars).vars;
reify-sub = v: sub:
let
val = walk v sub;
name = reify-name (length (attrNames sub));
in if isVar val then
extendSub val name sub
else if isArray val then
reify-sub (tail val) (reify-sub (head val) sub)
else
sub;
reify-name = n: "__${toString n}";
walk-h = v: sub:
let val = walk v sub;
in if isVar val then
val
else if isArray val then
[ (walk-h (head val) sub) ] ++ (walk-h (tail val) sub)
else
val;
# run
solve = all-or-num: goals:
let stream = (fresh goals) emptyState;
in mkReify (functionArgs goals) (if all-or-num == "all" then
take-all stream
else
take all-or-num stream);
# helper goals
facto = vals: X: disj (map (x: eqq x X) vals);
conso = H: T: P: (eqq ([ H ] ++ [ T ]) P);
fail = state: mzero;
succeed = unit;
in {
# goals
inherit fresh conde conj disj eqq facto conso fail succeed;
# interface
inherit solve;
};
zebra = with self.microkanren;
# https://en.wikipedia.org/wiki/Zebra_Puzzle
let
color = [ "red" "blue" "green" "ivory" "yellow" ];
nationality = [ "englishman" "spaniard" "ukrainian" "norweigian" "japanese" ];
drink = [ "coffee" "tea" "milk" "orange juice" "water" ];
smoke = [ "old gold" "kools" "chesterfields" "lucky strike" "parliaments" ];
pet = [ "dog" "snails" "fox" "horse" "zebra" ];
next = A: B:
conde [
[ (eqq A 1) (eqq B 2) ]
[ (eqq A 2) ((facto [ 1 3 ]) B) ]
[ (eqq A 3) ((facto [ 2 4 ]) B) ]
[ (eqq A 4) ((facto [ 3 5 ]) B) ]
[ (eqq A 5) (eqq B 4) ]
];
right = A: B:
conde [
[ (eqq A 1) ((facto [ 2 3 4 5 ]) B) ]
[ (eqq A 2) ((facto [ 3 4 5 ]) B) ]
[ (eqq A 3) ((facto [ 4 5 ]) B) ]
[ (eqq A 4) (eqq B 5) ]
[ (eqq A 5) fail ]
];
houseNumber = O: H:
fresh ({ C, N, D, S, P }: [
(eqq H [ O C N D S P ])
]);
houseColor = C: H:
fresh ({ O, N, D, S, P }: [
(eqq H [ O C N D S P ])
]);
houseNat = N: H:
fresh ({ O, C, D, S, P }: [
(eqq H [ O C N D S P ])
]);
houseSmoke = S: H:
fresh ({ O, C, N, D, P }: [
(eqq H [ O C N D S P ])
]);
housePet = P: H:
fresh ({ O, C, N, D, S }: [
(eqq H [ O C N D S P ])
]);
houseDrink = D: H:
fresh ({ O, C, N, S, P }: [
(eqq H [ O C N D S P ])
]);
membero = r: X: Tuple:
fresh ({ A1, A2, A3, A4, A5, H1, H2, H3, H4, H5 }: [
(eqq Tuple [ H1 H2 H3 H4 H5 ])
(r A1 H1)
(r A2 H2)
(r A3 H3)
(r A4 H4)
(r A5 H5)
(disj [ (eqq A1 X) (eqq A2 X) (eqq A3 X) (eqq A4 X) (eqq A5 X) ])
]);
unique = set: r: array: conj (map (x: membero r x array) set);
block = B:
fresh ({ H1, H2, H3, H4, H5 }: [
(eqq B [ H1 H2 H3 H4 H5 ])
(houseNumber 1 H1)
(houseNumber 2 H2)
(houseNumber 3 H3)
(houseNumber 4 H4)
(houseNumber 5 H5)
]);
require = Block: H:
fresh ({ H1, H2, H3, H4, H5 }: [
(eqq Block [ H1 H2 H3 H4 H5 ])
(disj [ (eqq H H1) (eqq H H2) (eqq H H3) (eqq H H4) (eqq H H5) ])
]);
puzzle = B:
conj [
(block B)
# The Englishman lives in the red house.
(fresh ({ O, D, S, P }: [
(require B [ O "red" "englishman" D S P ])
]))
# The Spaniard owns the dog.
(fresh ({ O, C, D, S }: [
(require B [ O C "spaniard" D S "dog" ])
]))
# Coffee is drunk in the green house.
(fresh ({ O, N, S, P }: [
(require B [ O "green" N "coffee" S P ])
]))
# The Ukrainian drinks tea.
(fresh ({ O, C, N, S, P }: [
(require B [ O C "ukrainian" "tea" S P ])
]))
# The green house is immediately to the right of the ivory house.
(fresh ({ O1, O2, N1, N2, D1, D2, S1, S2, P1, P2 }: [
(require B [ O1 "ivory" N2 D2 S2 P2 ])
(require B [ O2 "green" N1 D1 S1 P1 ])
(next O1 O2)
(right O1 O2)
]))
# The Old Gold smoker owns snails.
(fresh ({ O, C, N, D, S, P }: [
(require B [ O C N D "old gold" "snails" ])
]))
# Kools are smoked in the yellow house.
(fresh ({ O, C, N, D, S, P }: [
(require B [ O "yellow" N D "kools" P ])
]))
# Milk is drunk in the middle house.
(fresh ({ O, C, N, D, S, P }: [
(require B [ 3 C N "milk" S P ])
]))
# The Norwegian lives in the first house.
(fresh ({ O, C, N, D, S, P }: [
(require B [ 1 C "norweigian" D S P ])
]))
# The man who smokes Chesterfields lives in the house next to the man with the fox.
(fresh ({ O1, O2, C1, C2, N1, N2, D1, D2, S1, S2, P1, P2 }: [
(require B [ O1 C1 N1 D1 "chesterfields" P1 ])
(require B [ O2 C2 N2 D2 S1 "fox" ])
(next O1 O2)
]))
# Kools are smoked in the house next to the house where the horse is kept.
(fresh ({ O1, O2, C1, C2, N1, N2, D1, D2, S1, S2, P1, P2 }: [
(require B [ O1 C1 N1 D1 "kools" P1 ])
(require B [ O2 C2 N2 D2 S1 "horse" ])
(next O1 O2)
]))
# The Lucky Strike smoker drinks orange juice.
(fresh ({ O, C, N, D, S, P }: [
(require B [ O C N "orange juice" "lucky strike" P ])
]))
# The Japanese smokes Parliaments.
(fresh ({ O, C, N, D, S, P }: [
(require B [ O C "japanese" D "parliaments" P ])
]))
# The Norwegian lives next to the blue house.
(fresh ({ O1, O2, C1, C2, N1, N2, D1, D2, S1, S2, P1, P2 }: [
(require B [ O1 C1 "norweigian" D1 S1 P1 ])
(require B [ O2 "blue" N2 D2 S2 P2 ])
(next O1 O2)
]))
(unique color houseColor B)
(unique nationality houseNat B)
(unique drink houseDrink B)
(unique smoke houseSmoke B)
(unique pet housePet B)
];
in { solution = solve "all" ({ X }: [ (puzzle X) ]); };
};
}
nix eval .#zebra.solution --json | jq
thought it was fun so sharing.
happy hacking.