wrote new unify-function that always returns minimal set of reductions

This commit is contained in:
Joeri Exelmans 2025-05-23 14:04:39 +02:00
parent 47786ae792
commit 6fd4a4c0e1
3 changed files with 278 additions and 2 deletions

View file

@ -1,5 +1,5 @@
import assert from "node:assert";
import { assignFn, makeGeneric, unify, UnifyError } from "../lib/generics/generics.js";
import { assignFn, unify, UnifyError } from "../lib/generics/generics.js";
import { getDefaultTypeParser } from "../lib/parser/type_parser.js";
import { prettyT } from "../lib/util/pretty.js";
@ -12,7 +12,7 @@ assert.equal(
prettyT(
unify(
mkType("(a -> Int)"),
makeGeneric(() => mkType("[Bool] -> Int")),
mkType("[Bool] -> Int"),
)
),
// expected

108
tests/unify.js Normal file
View file

@ -0,0 +1,108 @@
import assert from "node:assert";
import { getDefaultTypeParser } from "../lib/parser/type_parser.js";
import { IncompabibleTypesError, subsitutionsEqual, unify } from "../lib/generics/unify.js";
const assertSubsitutionsEqual = (m1,m2) => {
if (!subsitutionsEqual(m1,m2)) {
throw new Error(`substitutions differ:\n m1 = ${prettySS(m1)}\n m2 = ${prettySS(m2)}`);
}
};
const mkType = getDefaultTypeParser();
assertSubsitutionsEqual(
unify(
mkType("Int"),
mkType("Int"),
),
new Map(),
);
assert.throws(
() => {
unify(
mkType("Int"),
mkType("Bool")
);
},
IncompabibleTypesError,
);
assertSubsitutionsEqual(
unify(
mkType("a -> Int"),
mkType("b -> b"),
),
new Map([
[mkType("a").symbol, mkType("Int")],
[mkType("b").symbol, mkType("Int")],
]),
);
assertSubsitutionsEqual(
unify(
mkType("(a -> Int)"),
mkType("[Bool] -> Int"),
),
new Map([
[mkType("a").symbol, mkType("[Bool]")],
]),
);
assertSubsitutionsEqual(
unify(
mkType("(a -> a) -> b"),
mkType("(Bool -> Bool) -> c"),
),
new Map([
[mkType("a").symbol, mkType("Bool")],
[mkType("c").symbol, mkType("b")],
]),
);
assert.throws(
() => {
unify(
mkType("a -> (a -> Ordering)"),
mkType("[b] -> b"),
);
},
IncompabibleTypesError,
);
assertSubsitutionsEqual(
unify(
mkType("[a] -> (Int -> a)"),
mkType("b -> c"),
),
new Map([
[mkType("b").symbol, mkType("[a]")],
[mkType("c").symbol, mkType("Int -> a")],
]),
);
assert.throws(
() => {
unify(
mkType("[a] -> (Int -> a)"),
mkType("b -> (c -> b)"),
);
},
IncompabibleTypesError,
// String,
);
assertSubsitutionsEqual(
unify(
mkType("a -> b -> a -> b"),
mkType("c -> c -> d -> e"),
),
new Map([
[mkType("b").symbol, mkType("a")],
[mkType("c").symbol, mkType("a")],
[mkType("d").symbol, mkType("a")],
[mkType("e").symbol, mkType("a")],
]),
);