simplify: no distinction between generic types and 'normal' types.
This commit is contained in:
parent
b4826605af
commit
a664ddac8a
27 changed files with 535 additions and 360 deletions
|
|
@ -1,64 +1,57 @@
|
|||
import { eqType } from "../primitives/type.js";
|
||||
import { eqType, getSymbol } from "../primitives/type.js";
|
||||
import { zip } from "../util/util.js";
|
||||
import { pretty, prettyT } from '../util/pretty.js';
|
||||
import { isTypeVar, TYPE_VARS } from "../primitives/typevars.js";
|
||||
|
||||
// constructor for generic types
|
||||
// helper for creating generic types
|
||||
// for instance, the type:
|
||||
// ∀a: a -> a -> Bool
|
||||
// is created by
|
||||
// makeGeneric(a => fnType(() => a)(() => fnType(() => a)(() => Bool)))
|
||||
export const makeGeneric = callback => {
|
||||
// type variables to make available:
|
||||
const typeVars = ['a', 'b', 'c', 'd', 'e'].map(Symbol);
|
||||
const type = callback(...typeVars);
|
||||
return onlyOccurring(type, new Set(typeVars));
|
||||
const type = callback(...TYPE_VARS);
|
||||
return type;
|
||||
};
|
||||
|
||||
export const onlyOccurring = (type, typeVars) => ({
|
||||
typeVars: occurring(type, typeVars),
|
||||
type,
|
||||
});
|
||||
|
||||
const __occurring = state => typeVars => type => {
|
||||
if (typeVars.has(type)) {
|
||||
return new Set([type]);
|
||||
const _occurring = stack => type => {
|
||||
if (isTypeVar(type)) {
|
||||
return new Set([getSymbol(type)]);
|
||||
}
|
||||
const tag = state.nextTag++;
|
||||
state.seen.add(tag);
|
||||
const tag = stack.length;
|
||||
const newStack = [...stack, tag];
|
||||
return new Set(type.params.flatMap(p => {
|
||||
const innerType = p(tag);
|
||||
if (state.seen.has(innerType)) {
|
||||
if (newStack.includes(innerType)) {
|
||||
return []; // no endless recursion!
|
||||
}
|
||||
return [...__occurring(state)(typeVars)(innerType)];
|
||||
return [..._occurring(newStack)(innerType)];
|
||||
}));
|
||||
};
|
||||
|
||||
// From the given set of type variables, return only those that occur in the given type.
|
||||
export const occurring = (type, typeVars) => {
|
||||
return __occurring({nextTag:0, seen: new Set()})(typeVars)(type);
|
||||
};
|
||||
// Get set of type variables in type.
|
||||
export const occurring = _occurring([]);
|
||||
|
||||
// Merge 2 substitution-mappings, uni-directional.
|
||||
const mergeOneWay = (m1, m2) => {
|
||||
const m1copy = new Map(m1);
|
||||
const m2copy = new Map(m2);
|
||||
for (const [var1, typ1] of m1copy.entries()) {
|
||||
if (m2copy.has(typ1)) {
|
||||
for (const [symbol1, typ1] of m1copy) {
|
||||
if (m2copy.has(getSymbol(typ1))) {
|
||||
// typ1 is a typeVar for which we also have a substitution
|
||||
// -> fold substitutions
|
||||
m1copy.set(var1, m2.get(typ1));
|
||||
m2copy.delete(typ1);
|
||||
return [false, m1copy, m2copy, new Set([typ1])];
|
||||
m1copy.set(symbol1, m2.get(getSymbol(typ1)));
|
||||
m2copy.delete(getSymbol(typ1));
|
||||
return [false, m1copy, m2copy];
|
||||
}
|
||||
}
|
||||
return [true, m1copy, m2copy, new Set()]; // stable
|
||||
return [true, m1copy, m2copy]; // stable
|
||||
};
|
||||
|
||||
const checkConflict = (m1, m2) => {
|
||||
for (const [var1, typ1] of m1) {
|
||||
if (m2.has(var1)) {
|
||||
const other = m2.get(var1);
|
||||
for (const [symbol1, typ1] of m1) {
|
||||
if (m2.has(symbol1)) {
|
||||
const other = m2.get(symbol1);
|
||||
if (!eqType(typ1, other)) {
|
||||
throw new Error(`conflicting substitution: ${pretty(typ1)}vs. ${pretty(other)}`);
|
||||
}
|
||||
|
|
@ -73,21 +66,17 @@ export const mergeTwoWay = (m1, m2) => {
|
|||
// checkConflict(m2, m1); // <- don't think this is necessary...
|
||||
// actually merge
|
||||
let stable = false;
|
||||
let deletions = new Set();
|
||||
while (!stable) {
|
||||
let d;
|
||||
// notice we swap m2 and m1, so the rewriting can happen both ways:
|
||||
[stable, m2, m1, d] = mergeOneWay(m1, m2);
|
||||
deletions = deletions.union(d);
|
||||
[stable, m2, m1] = mergeOneWay(m1, m2);
|
||||
}
|
||||
const result = {
|
||||
substitutions: new Map([...m1, ...m2]),
|
||||
deletions, // deleted type variables
|
||||
};
|
||||
const result = new Map([...m1, ...m2]);
|
||||
// console.log("mergeTwoWay result =", result);
|
||||
return result;
|
||||
};
|
||||
|
||||
export class UnifyError extends Error {}
|
||||
|
||||
// Thanks to Hans for pointing out that this algorithm exactly like "Unification" in Prolog (hence the function name):
|
||||
// https://www.dai.ed.ac.uk/groups/ssp/bookpages/quickprolog/node12.html
|
||||
//
|
||||
|
|
@ -95,35 +84,29 @@ export const mergeTwoWay = (m1, m2) => {
|
|||
// typeVars: all the type variables in both fType and aType
|
||||
// fType, aType: generic types to unify
|
||||
// fStack, aStack: internal use.
|
||||
const __unify = (typeVars, fType, aType, fStack=[], aStack=[]) => {
|
||||
const __unify = (fType, aType, fStack=[], aStack=[]) => {
|
||||
// console.log("__unify", {typeVars, fType: prettyT(fType), aType: prettyT(aType), fStack, aStack});
|
||||
if (typeVars.has(fType)) {
|
||||
if (isTypeVar(fType)) {
|
||||
// simplest case: formalType is a type paramater
|
||||
// => substitute with actualType
|
||||
// console.log(`assign ${prettyT(aType)} to ${prettyT(fType)}`);
|
||||
return {
|
||||
substitutions: new Map([[fType, aType]]),
|
||||
genericType: {
|
||||
typeVars: typeVars.difference(new Set([fType])),
|
||||
type: aType,
|
||||
},
|
||||
substitutions: new Map([[getSymbol(fType), aType]]),
|
||||
type: aType,
|
||||
};
|
||||
}
|
||||
if (typeVars.has(aType)) {
|
||||
if (isTypeVar(aType)) {
|
||||
// same as above, but in the other direction
|
||||
// console.log(`assign ${prettyT(fType)} to ${prettyT(aType)}`);
|
||||
return {
|
||||
substitutions: new Map([[aType, fType]]),
|
||||
genericType: {
|
||||
typeVars: typeVars.difference(new Set([aType])),
|
||||
type: fType,
|
||||
},
|
||||
substitutions: new Map([[getSymbol(aType), fType]]),
|
||||
type: fType,
|
||||
};
|
||||
}
|
||||
|
||||
// recursively unify
|
||||
if (fType.symbol !== aType.symbol) {
|
||||
throw new Error(`cannot unify ${prettyT(fType)} and ${prettyT(aType)}`);
|
||||
throw new UnifyError(`cannot unify ${prettyT(fType)} and ${prettyT(aType)}`);
|
||||
}
|
||||
|
||||
const fTag = fStack.length;
|
||||
|
|
@ -137,106 +120,79 @@ const __unify = (typeVars, fType, aType, fStack=[], aStack=[]) => {
|
|||
// type recursively points to an enclosing type that we've already seen
|
||||
if (fStack[fParam] !== aStack[aParam]) {
|
||||
// note that both are also allowed not to be mapped (undefined)
|
||||
throw new Error("cannot unify: types differ in their recursion");
|
||||
throw new UnifyError("cannot unify: types differ in their recursion");
|
||||
}
|
||||
if (fStack[fParam] !== undefined) {
|
||||
const type = fStack[fParam];
|
||||
return () => ({
|
||||
substitutions: new Map(),
|
||||
genericType: {
|
||||
typeVars,
|
||||
type,
|
||||
},
|
||||
type,
|
||||
});
|
||||
}
|
||||
return parent => __unify(typeVars, fParam, aParam,
|
||||
return parent => __unify(fParam, aParam,
|
||||
[...fStack, parent],
|
||||
[...aStack, parent]);
|
||||
});
|
||||
|
||||
const unifiedParams = unifications.map(getParam => {
|
||||
return parent => getParam(parent).genericType.type;
|
||||
return parent => getParam(parent).type;
|
||||
});
|
||||
const type = {
|
||||
symbol: fType.symbol,
|
||||
params: unifiedParams,
|
||||
};
|
||||
|
||||
const [unifiedSubstitutions, unifiedTypeVars] = unifications.reduce((acc, getParam) => {
|
||||
const unifiedSubstitutions = unifications.reduce((acc, getParam) => {
|
||||
const self = Symbol(); // dirty, just need something unique
|
||||
const {substitutions, deletions} = mergeTwoWay(acc[0], getParam(self).substitutions);
|
||||
return [substitutions, acc[1]
|
||||
.difference(substitutions)
|
||||
.difference(deletions)];
|
||||
}, [new Map(), typeVars]);
|
||||
const paramSubstitutions = getParam(self).substitutions;
|
||||
const substitutions = mergeTwoWay(acc, paramSubstitutions);
|
||||
return substitutions;
|
||||
}, new Map());
|
||||
|
||||
return {
|
||||
substitutions: unifiedSubstitutions,
|
||||
genericType: {
|
||||
typeVars: unifiedTypeVars,
|
||||
type,
|
||||
type: {
|
||||
symbol: fType.symbol,
|
||||
params: unifiedParams,
|
||||
},
|
||||
};
|
||||
};
|
||||
|
||||
export const unify = (fGenericType, aGenericType) => {
|
||||
let allTypeVars;
|
||||
[allTypeVars, fGenericType, aGenericType] = safeUnionTypeVars(fGenericType, aGenericType);
|
||||
const {genericType, substitutions} = __unify(allTypeVars, fGenericType.type, aGenericType.type);
|
||||
export const unify = (fType, aType) => {
|
||||
[fType, aType] = recomputeTypeVars([fType, aType]);
|
||||
const {type, substitutions} = __unify(fType, aType);
|
||||
// console.log('unification complete! substitutions:', substitutions);
|
||||
return recomputeTypeVars(genericType);
|
||||
return recomputeTypeVars([type])[0];
|
||||
};
|
||||
|
||||
export const substitute = (type, substitutions, stack=[]) => {
|
||||
// console.log('substitute...', {type, substitutions, stack});
|
||||
return substitutions.get(type)
|
||||
return substitutions.get(getSymbol(type))
|
||||
|| {
|
||||
symbol: type.symbol,
|
||||
symbol: getSymbol(type),
|
||||
params: type.params.map(getParam => parent => {
|
||||
const param = getParam(stack.length);
|
||||
const have = stack[param];
|
||||
return (have !== undefined)
|
||||
? have
|
||||
: substitute(param, substitutions, [...stack, parent]);
|
||||
return stack[param]
|
||||
|| substitute(param, substitutions, [...stack, parent]);
|
||||
}),
|
||||
};
|
||||
};
|
||||
|
||||
export const assign = (genFnType, paramType) => {
|
||||
let allTypeVars;
|
||||
[allTypeVars, genFnType, paramType] = safeUnionTypeVars(genFnType, paramType);
|
||||
const [inType, outType] = genFnType.type.params;
|
||||
const {substitutions} = __unify(allTypeVars, inType(genFnType.type), paramType.type);
|
||||
const substitutedOutType = substitute(outType(genFnType.type), substitutions);
|
||||
return recomputeTypeVars(onlyOccurring(substitutedOutType, allTypeVars));
|
||||
export const assignFn = (funType, paramType) => {
|
||||
[funType, paramType] = recomputeTypeVars([funType, paramType]);
|
||||
// console.log(prettyT(funType), prettyT(paramType));
|
||||
const [inType, outType] = funType.params.map(p => p(funType));
|
||||
const {substitutions} = __unify(inType, paramType);
|
||||
// console.log(substitutions, prettyT(outType));
|
||||
const substitutedFnType = substitute(outType, substitutions);
|
||||
return recomputeTypeVars([substitutedFnType])[0];
|
||||
};
|
||||
|
||||
export const assignFn = (genFnType, paramType) => {
|
||||
let allTypeVars;
|
||||
[allTypeVars, genFnType, paramType] = safeUnionTypeVars(genFnType, paramType);
|
||||
const [inType] = genFnType.type.params;
|
||||
const {substitutions} = __unify(allTypeVars, inType, paramType.type);
|
||||
const substitutedFnType = substitute(genFnType.type, substitutions);
|
||||
return recomputeTypeVars(onlyOccurring(substitutedFnType, allTypeVars));
|
||||
};
|
||||
|
||||
export const recomputeTypeVars = (genType) => {
|
||||
const newTypeVars = ['a', 'b', 'c', 'd', 'e', 'f', 'g'].map(Symbol);
|
||||
// Ensures that no type variables overlap
|
||||
export const recomputeTypeVars = types => {
|
||||
let nextIdx = 0;
|
||||
const subst = new Map();
|
||||
for (const typeVarA of genType.typeVars) {
|
||||
subst.set(typeVarA, newTypeVars[nextIdx++]);
|
||||
}
|
||||
const substType = {
|
||||
typeVars: new Set(subst.values()),
|
||||
type: substitute(genType.type, subst),
|
||||
};
|
||||
return substType;
|
||||
};
|
||||
|
||||
export const safeUnionTypeVars = (genTypeA, genTypeB) => {
|
||||
const substTypeA = recomputeTypeVars(genTypeA);
|
||||
const substTypeB = recomputeTypeVars(genTypeB);
|
||||
const allTypeVars = substTypeA.typeVars.union(substTypeB.typeVars);
|
||||
return [allTypeVars, substTypeA, substTypeB];
|
||||
};
|
||||
return types.map(type => {
|
||||
const substitutions = new Map();
|
||||
const typeVars = occurring(type);
|
||||
for (const typeVar of typeVars) {
|
||||
substitutions.set(typeVar, TYPE_VARS[nextIdx++]);
|
||||
}
|
||||
return substitute(type, substitutions);
|
||||
});
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue