turn one example into a test + fix bug in type variable substition function

This commit is contained in:
Joeri Exelmans 2025-05-08 17:30:42 +02:00
parent a664ddac8a
commit 35d682429b
4 changed files with 148 additions and 102 deletions

View file

View file

@ -1,97 +0,0 @@
import { compareTypes } from "../lib/compare/type.js";
import { makeGeneric, substitute, unify } from "../lib/generics/generics.js";
import { Double, Int, Unit } from "../lib/primitives/primitive_types.js";
import { TYPE_VARS } from "../lib/primitives/typevars.js";
import { fnType, lsType, prodType, sumType, setType } from "../lib/structures/type_constructors.js";
import { prettyT } from "../lib/util/pretty.js";
Error.stackTraceLimit = Infinity;
// some recursive types:
const listOfSetOfSelf = lsType(self => setType(_ => self));
const makeLinkedList = elementType => sumType
(self => prodType
(_ => elementType)
(_ => self))
(_ => Unit);
const linkedListOfInt = makeLinkedList(Int);
const linkedListOfDouble = makeLinkedList(Double);
// some generic types
const genericFunction = makeGeneric((a,b) => fnType(_ => a)(_ => b));
const genericLinkedList = makeGeneric(a => makeLinkedList(a));
// pretty-printing of recursive types:
console.log(prettyT(listOfSetOfSelf)); // #0[{#0}]
console.log(prettyT(linkedListOfInt)); // #0((Int #0) + Unit)
console.log(prettyT(genericFunction)); // (a -> b)
console.log(prettyT(genericLinkedList)); // #0((a #0) + Unit)
// comparison
console.log(compareTypes(listOfSetOfSelf)(listOfSetOfSelf)) // 0
console.log(compareTypes(linkedListOfInt)(linkedListOfInt)) // 0
console.log(compareTypes(linkedListOfInt)(linkedListOfDouble)) // 1
console.log(compareTypes(linkedListOfDouble)(linkedListOfInt)) // -1
console.log(compareTypes(linkedListOfDouble)(linkedListOfDouble)) // 0
console.log(compareTypes(linkedListOfDouble)(listOfSetOfSelf)) // 1
console.log(compareTypes(listOfSetOfSelf)(linkedListOfDouble)) // -1
const genericList = makeGeneric(a => lsType(_ => a));
const intList = lsType(_ => Int);
console.log(prettyT(genericList)); // [a]
// substitution of type parameters
const substituted = substitute(
genericList,
new Map([
[TYPE_VARS[0], Int],
])
);
console.log(prettyT(substituted)); // [Int]
// substitution (recursive this time)
console.log("recursive substitution")
console.log(prettyT(substitute(
genericLinkedList,
new Map([
[TYPE_VARS[0], Int],
])
))); // #0((Int #0) + Unit)
// unification (simple case)
const type = unify(
genericList,
makeGeneric(() => intList));
console.log(prettyT(type)); // [Int]
// unification (recursive case)
console.log("complex case...")
const unified = unify(
genericLinkedList,
makeGeneric(() => linkedListOfInt));
console.log(prettyT(unified)); // #0((Int #0) + Unit)
// unification (strange case)
const unified2 = unify(
makeGeneric(() => listOfSetOfSelf),
genericList,
);
console.log(prettyT(unified2)); // #0[{#0}]

View file

@ -163,17 +163,24 @@ export const unify = (fType, aType) => {
export const substitute = (type, substitutions, stack=[]) => {
// console.log('substitute...', {type, substitutions, stack});
return substitutions.get(getSymbol(type))
|| {
const found = substitutions.get(getSymbol(type));
if (found) {
return found;
}
return {
symbol: getSymbol(type),
params: type.params.map(getParam => parent => {
const param = getParam(stack.length);
return stack[param]
|| substitute(param, substitutions, [...stack, parent]);
const param = getParam(parent);
if (stack.includes(param)) {
// param points back up - that's ok - means we don't have to recurse
return param;
}
return substitute(param, substitutions, [...stack, parent]);
}),
};
};
export const assignFn = (funType, paramType) => {
[funType, paramType] = recomputeTypeVars([funType, paramType]);
// console.log(prettyT(funType), prettyT(paramType));

136
tests/recursive_types.js Normal file
View file

@ -0,0 +1,136 @@
import assert from "node:assert";
import { compareTypes } from "../lib/compare/type.js";
import { makeGeneric, substitute, unify } from "../lib/generics/generics.js";
import { Double, Int, Unit } from "../lib/primitives/primitive_types.js";
import { UNBOUND_SYMBOLS } from "../lib/primitives/typevars.js";
import { fnType, lsType, prodType, sumType, setType } from "../lib/structures/type_constructors.js";
import { prettyT } from "../lib/util/pretty.js";
// some recursive types:
const listOfSetOfSelf = lsType(self => setType(_ => self));
const makeLinkedList = elementType =>
sumType
(self => prodType
(_ => elementType)
(_ => self))
(_ => Unit);
const linkedListOfInt = makeLinkedList(Int);
const linkedListOfDouble = makeLinkedList(Double);
// some generic types
const genericFunction = makeGeneric((a,b) => fnType(_ => a)(_ => b));
const genericLinkedList = makeGeneric(a => makeLinkedList(a));
// pretty-printing of recursive types:
assert.equal(
prettyT(listOfSetOfSelf),
"#0[{#0}]",
);
assert.equal(
prettyT(linkedListOfInt),
"#0((Int #0) + Unit)",
);
assert.equal(
prettyT(genericFunction),
"(a -> b)",
);
assert.equal(
prettyT(genericLinkedList),
"#0((a #0) + Unit)",
);
// comparison
assert.equal(
compareTypes(listOfSetOfSelf)(listOfSetOfSelf),
0,
"types should be equal",
);
assert.equal(
compareTypes(linkedListOfInt)(linkedListOfInt),
0,
"types should be equal",
);
assert.notEqual(
compareTypes(linkedListOfInt)(linkedListOfDouble),
0,
"types should not be equal",
);
assert.equal(
compareTypes(linkedListOfDouble)(linkedListOfInt)
+ compareTypes(linkedListOfInt)(linkedListOfDouble),
0,
"comparison invariant",
);
assert.equal(
compareTypes(linkedListOfDouble)(linkedListOfDouble),
0,
"types should be equal",
)
assert.notEqual(
compareTypes(linkedListOfDouble)(listOfSetOfSelf),
0,
"types should not be equal",
);
assert.equal(
compareTypes(linkedListOfDouble)(listOfSetOfSelf)
+ compareTypes(listOfSetOfSelf)(linkedListOfDouble),
0,
"comparison invariant",
);
const genericList = makeGeneric(a => lsType(_ => a));
// substitution of type parameters
assert.equal(
// actual
prettyT(substitute(
genericLinkedList,
new Map([
[UNBOUND_SYMBOLS[0], Int],
])
)),
// expected
"#0((Int #0) + Unit)",
);
// unification (recursive)
assert.equal(
// actual
prettyT(unify(
genericLinkedList,
makeGeneric(() => linkedListOfInt)
)),
// expected
"#0((Int #0) + Unit)",
)
assert.equal(
// actual
prettyT(unify(
makeGeneric(() => listOfSetOfSelf),
genericList,
)),
// expected
"#0[{#0}]",
)