research/dope2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

create 'Ordering' type

Browse source
This commit is contained in:
Joeri Exelmans 2025-05-09 16:35:26 +02:00
parent 77dfc8b182
commit b0023afe8c
15 changed files with 158 additions and 117 deletions
Download patch file Download diff file Expand all files Collapse all files

15
examples/environment.js
View file

@ -1,9 +1,18 @@
import { module2Env } from "../lib/environment/env.js";
import { newDynamic } from "../lib/primitives/dynamic.js";
import { Dynamic } from "../lib/primitives/primitive_types.js";
import { TYPE_VARS } from "../lib/primitives/typevars.js";
import { ModuleStd } from "../lib/stdlib.js";
import { listInstances } from "./prompt/prompt.js";
import { emptyList } from "../lib/structures/list.js";
import { lsType } from "../lib/structures/type_constructors.types.js";
import { listInstances, transform } from "./prompt/prompt.js";
const typeDict = module2Env(ModuleStd);
const env = module2Env(ModuleStd);
await listInstances(typeDict, Dynamic);
await listInstances(env, Dynamic);
await transform(
env,
newDynamic(emptyList)(lsType(_ => TYPE_VARS[0])),
);

35
examples/prompt/prompt.js
View file

@ -1,13 +1,9 @@
import { number, select } from "@inquirer/prompts";
import { makeCompareFn } from "../../lib/compare/dynamic.js";
import { getFunctions, getInstances, getTypes, growEnv } from "../../lib/environment/env.js";
import { assignFn } from "../../lib/generics/generics.js";
import { getCompatibleInputTypes, getEnabledFunctions, getInstances, growEnv } from "../../lib/environment/env.js";
import { getInst, getType, newDynamic } from "../../lib/primitives/dynamic.js";
import { Bool, Double, Int, SymbolDynamic, Type, UUID } from "../../lib/primitives/primitive_types.js";
import { eqType, getSymbol } from "../../lib/primitives/type.js";
import { ModuleStd } from "../../lib/stdlib.js";
import { fold as foldList } from "../../lib/structures/list.js";
import { fold as foldSet } from "../../lib/structures/set.js";
import { symbolFunction } from "../../lib/structures/type_constructors.js";
import { pretty, prettyT } from "../../lib/util/pretty.js";
@ -168,20 +164,10 @@ const createInstance = async (type) => {
console.log("no prompt handler for creating new", prettyT(type));
};
const transform = async (env, dynamic) => {
const allFunctions = getFunctions(env);
const enabled = foldList(enabled => fun => {
try {
const outType = assignFn(getType(fun), getType(dynamic));
return [...enabled, {fun, outType}];
} catch (e) {
// console.log('warning:', e);
return enabled;
}
})([])(allFunctions);
export const transform = async (env, dynamic) => {
const enabled = getEnabledFunctions(env)(dynamic);
const choice = await select({
message: `select:`,
message: `select transformation:`,
choices: [
"(go back)",
...enabled.map(({fun, outType}) => ({
@ -203,18 +189,7 @@ const transform = async (env, dynamic) => {
const call = async (env, funDynamic) => {
const funType = getType(funDynamic);
const allTypes = getTypes(env);
// compatible input types
const inTypes = foldSet(types => inType => {
try {
const outType = assignFn(funType, inType); // may throw
return [...types, {inType, outType}];
} catch (e) {
return types;
}
})([])(allTypes);
const inTypes = getCompatibleInputTypes(env)(funType);
const choice = inTypes.length === 1
? inTypes[0]
: await select({

35
lib/compare/dynamic.js
View file

@ -1,9 +1,9 @@
import { getInst, getType } from "../primitives/dynamic.js";
import { SymbolBool, SymbolBottom, SymbolByte, SymbolChar, SymbolDouble, SymbolDynamic, SymbolInt, SymbolUUID, SymbolType, SymbolUnit } from "../primitives/primitive_types.js";
import { SymbolBool, SymbolBottom, SymbolByte, SymbolChar, SymbolDouble, SymbolDynamic, SymbolInt, SymbolUUID, SymbolType, SymbolUnit, SymbolOrdering } from "../primitives/primitive_types.js";
import { UNBOUND_SYMBOLS } from "../primitives/typevars.js";
import { symbolDict, symbolFunction, symbolList, symbolProduct, symbolSet, symbolSum } from "../structures/type_constructors.js";
import { prettyT } from "../util/pretty.js";
import { compareBools, compareNumbers, compareStrings, compareSymbols, compareUnits } from "./primitives.js";
import { compareBools, compareDoubles, compareOrderings, compareStrings, compareSymbols, compareUnits } from "./primitives.js";
import { compareDicts, compareFunctions, compareLists, compareProducts, compareSets, compareSums } from "./structures.js";
import { compareTypes } from "./type.js";
@ -14,25 +14,26 @@ export const compareDynamic = x => y =>
const cannotCompareTypeVarInstances = _ => _ => { throw new Error("Cannot compare instance of type variables"); }
const typeSymbolToCmp = new Map([
[SymbolInt , compareNumbers],
[SymbolBool , compareBools],
[SymbolDouble , compareNumbers],
[SymbolByte , compareNumbers],
[SymbolChar , compareStrings],
[SymbolUnit , compareUnits],
[SymbolBottom , _ => _ => { throw new Error("Bottom!"); }],
[SymbolUUID , compareSymbols],
[SymbolInt , compareDoubles ],
[SymbolBool , compareBools ],
[SymbolDouble , compareDoubles ],
[SymbolByte , compareDoubles ],
[SymbolChar , compareStrings ],
[SymbolUnit , compareUnits ],
[SymbolBottom , _ => _ => { throw new Error("Bottom!"); }],
[SymbolUUID , compareSymbols ],
// [SymbolGenericType, ?] TODO
[SymbolType , compareTypes],
[SymbolDynamic, compareDynamic],
[SymbolType , compareTypes ],
[SymbolDynamic , compareDynamic ],
[SymbolOrdering, compareOrderings],
// these functions take extra comparison callbacks:
[symbolFunction, compareFunctions],
[symbolSum , compareSums],
[symbolProduct , compareProducts],
[symbolList , compareLists],
[symbolSet , compareSets],
[symbolDict , compareDicts],
[symbolSum , compareSums ],
[symbolProduct , compareProducts ],
[symbolList , compareLists ],
[symbolSet , compareSets ],
[symbolDict , compareDicts ],
// even though we cannot compare typevar instances,
// we still need to give a function or shit will break

5
lib/compare/dynamic.types.js
View file

@ -1,9 +1,10 @@
import { getDefaultTypeParser } from "../parser/type_parser.js";
import { newDynamic } from "../primitives/dynamic.js";
import { compareDynamic, makeCompareFn } from "./dynamic.js";
const mkType = getDefaultTypeParser();
export const ModuleCompareDynamic = [
newDynamic(makeCompareFn )(mkType("Type -> a -> a -> Int")),
newDynamic(compareDynamic)(mkType("Dynamic -> Dynamic -> Int")),
newDynamic(makeCompareFn )(mkType("Type -> a -> a -> Ordering")),
newDynamic(compareDynamic)(mkType("Dynamic -> Dynamic -> Ordering")),
];

15
lib/compare/primitives.js
View file

@ -1,18 +1,25 @@
// Total ordering of primitive types
export const compareNumbers = x => y => {
export const compareInts = x => y => {
if (typeof(x) !== 'bigint' || typeof(y) !== 'bigint') {
throw new Error(`was only meant to compare bigints! got ${x} and ${y}`);
}
return (x < y) ? -1 : (x > y) ? 1 : 0;
};
export const compareDoubles = x => y => {
if (typeof(x) !== 'number' || typeof(y) !== 'number') {
throw new Error(`was only meant to compare numbers! got ${x} and ${y}`);
}
return (x < y) ? -1 : (x > y) ? 1 : 0;
}
};
export const compareStrings = x => y => {
if (typeof(x) !== 'string' || typeof(y) !== 'string') {
throw new Error(`was only meant to compare strings! got ${x} and ${y}`);
}
return (x < y) ? -1 : (x > y) ? 1 : 0;
}
};
export const compareBools = x => y => {
if (typeof(x) !== 'boolean' || typeof(y) !== 'boolean') {
@ -26,3 +33,5 @@ export const compareUnits = _ => _ => 0;
// Symbols are encoded as strings
export const compareSymbols = a => b => compareStrings(a)(b);
export const compareOrderings = a => b => compareDoubles(a)(b);

12
lib/compare/primitives.types.js
View file

@ -1,12 +1,14 @@
import { getDefaultTypeParser } from "../parser/type_parser.js";
import { newDynamic } from "../primitives/dynamic.js";
import { compareBools, compareNumbers, compareSymbols, compareUnits } from "./primitives.js";
import { compareBools, compareDoubles, compareInts, compareOrderings, compareSymbols, compareUnits } from "./primitives.js";
const mkType = getDefaultTypeParser();
export const ModuleComparePrimitives = [
newDynamic(compareNumbers)(mkType("Double -> Double -> Int")),
newDynamic(compareBools )(mkType("Bool -> Bool -> Int")),
newDynamic(compareUnits )(mkType("Unit -> Unit -> Int")),
newDynamic(compareSymbols)(mkType("UUID -> UUID -> Int")),
newDynamic(compareInts )(mkType("Int -> Int -> Ordering" )),
newDynamic(compareDoubles )(mkType("Double -> Double -> Ordering" )),
newDynamic(compareBools )(mkType("Bool -> Bool -> Ordering" )),
newDynamic(compareUnits )(mkType("Unit -> Unit -> Ordering" )),
newDynamic(compareSymbols )(mkType("UUID -> UUID -> Ordering" )),
newDynamic(compareOrderings)(mkType("Ordering -> Ordering -> Ordering")),
];

8
lib/compare/structures.js
View file

@ -1,6 +1,6 @@
// Total ordering of composed types
import { compareNumbers, compareStrings } from "./primitives.js"
import { compareDoubles, compareStrings } from "./primitives.js"
import { get, length as lengthLs } from "../structures/list.js";
import { read as readSet, length as lengthSet, first as firstSet } from "../structures/set.js";
import { read as readDict, length as lengthDict, first as firstDict } from "../structures/dict.js";
@ -13,7 +13,7 @@ export const compareFunctions = _compareInput => _compareOutput => x => y => {
}
export const compareLists = compareElems => x => y => {
return compareNumbers(lengthLs(x))(lengthLs(y))
return compareDoubles(lengthLs(x))(lengthLs(y))
|| (() => {
for (let i=0; i<lengthLs(x); i++) {
const elemCmp = compareElems(get(x)(i))(get(y)(i));
@ -50,7 +50,7 @@ export const compareSums = compareLeft => compareRight => x => y => {
};
export const compareSets = compareElems => x => y => {
return compareNumbers(lengthSet(x))(lengthSet(y))
return compareDoubles(lengthSet(x))(lengthSet(y))
|| (() => {
// sets have same size -> iterate over both sets and compare their elements pairwise
// because of the underlying red-black tree, iteration happens in ordered fashion
@ -71,7 +71,7 @@ export const compareSets = compareElems => x => y => {
};
export const compareDicts = compareKeys => compareValues => x => y => {
return compareNumbers(lengthDict(x))(lengthDict(y))
return compareDoubles(lengthDict(x))(lengthDict(y))
|| (() => {
// dicts have same size -> iterate over both and compare their entries pairwise
// because of the underlying red-black tree, iteration happens in ordered fashion

10
lib/compare/structures.types.js
View file

@ -5,13 +5,13 @@ import { compareDicts, compareLists, compareProducts, compareSets, compareSums }
const mkType = getDefaultTypeParser();
export const ModuleCompareStructures = [
newDynamic(compareLists)(mkType("(a -> a -> Int) -> [a] -> [a] -> Int")),
newDynamic(compareLists)(mkType("(a -> a -> Ordering) -> [a] -> [a] -> Ordering")),
newDynamic(compareProducts)(mkType("(a -> a -> Int) -> (b -> b -> Int) -> (a*b) -> (a*b) -> Int")),
newDynamic(compareProducts)(mkType("(a -> a -> Ordering) -> (b -> b -> Ordering) -> (a*b) -> (a*b) -> Ordering")),
newDynamic(compareSums)(mkType("(a -> a -> Int) -> (b -> b -> Int) -> (a+b) -> (a+b) -> Int")),
newDynamic(compareSums)(mkType("(a -> a -> Ordering) -> (b -> b -> Ordering) -> (a+b) -> (a+b) -> Ordering")),
newDynamic(compareSets)(mkType("(a -> a -> Int) -> {a} -> {a} -> Int")),
newDynamic(compareSets)(mkType("(a -> a -> Ordering) -> {a} -> {a} -> Ordering")),
newDynamic(compareDicts)(mkType("(a -> a -> Int) -> (b -> b-> Int) -> (a => b) -> (a => b) -> Int"))
newDynamic(compareDicts)(mkType("(a -> a -> Ordering) -> (b -> b-> Ordering) -> (a => b) -> (a => b) -> Ordering"))
];

4
lib/compare/type.js
View file

@ -1,5 +1,5 @@
import { getParams, getSymbol } from "../primitives/type.js";
import { compareBools, compareNumbers, compareSymbols } from "./primitives.js";
import { compareBools, compareDoubles, compareSymbols } from "./primitives.js";
import { compareLists } from "./structures.js";
const __compareTypes = state => typeX => typeY => {
@ -20,7 +20,7 @@ const __compareTypes = state => typeX => typeY => {
// both sub-types have been visited already in an enclosing call
// if they were being compared in the same enclosing call, we assume they are equal!
// (we cannot compare them, that would result in endless recursion)
return compareNumbers(state.comparing.get(pX))(pY);
return compareDoubles(state.comparing.get(pX))(pY);
}
// none have been visited -> recursively compare
return __compareTypes(state)(pX)(pY);

2
lib/compare/type.types.js
View file

@ -5,5 +5,5 @@ import { compareTypes } from "./type.js";
const mkType = getDefaultTypeParser();
export const ModuleCompareTypes = [
newDynamic(compareTypes)(mkType("Type -> Type -> Int")),
newDynamic(compareTypes)(mkType("Type -> Type -> Ordering")),
];

38
lib/environment/env.js
View file

@ -1,5 +1,6 @@
import { makeCompareFn } from "../compare/dynamic.js";
import { compareTypes } from "../compare/type.js";
import { assignFn, UnifyError } from "../generics/generics.js";
import { getInst, getType, newDynamic } from "../primitives/dynamic.js";
import { Dynamic, Type } from "../primitives/primitive_types.js";
import { getSymbol } from "../primitives/type.js";
@ -26,7 +27,7 @@ export const module2Env = module => {
try {
return growEnv(typeDict)(dynamic);
} catch (e) {
console.log('warning:', e.message);
console.log('skip:', e.message);
return typeDict;
}
})(emptyDict(compareTypes))(module);
@ -57,4 +58,37 @@ export const getFunctions = env => {
}
return types;
})([])(types);
};
};
// return list of functions that can be called on 'dynamic'
export const getEnabledFunctions = env => dynamic => {
const allFunctions = getFunctions(env);
const enabled = foldList(enabled => fun => {
try {
const outType = assignFn(getType(fun), getType(dynamic));
return [...enabled, {fun, outType}];
} catch (e) {
if (!(e instanceof UnifyError)) {
throw e;
}
return enabled;
}
})([])(allFunctions);
return enabled;
};
export const getCompatibleInputTypes = env => funType => {
const allTypes = getTypes(env);
const inTypes = foldSet(types => inType => {
try {
const outType = assignFn(funType, inType); // may throw
return [...types, {inType, outType}];
} catch (e) {
if (!(e instanceof UnifyError)) {
throw e;
}
return types;
}
})([])(allTypes);
return inTypes;
}

41
lib/parser/type_parser.js
View file

@ -1,6 +1,6 @@
// A simple, hacked-together recursive parser for types.
import { Bool, Char, Double, Int, UUID, Type, Unit } from "../primitives/primitive_types.js";
import { Bool, Char, Double, Int, UUID, Type, Unit, Ordering } from "../primitives/primitive_types.js";
import { Dynamic } from "../primitives/primitive_types.js";
import { getHumanReadableName } from "../primitives/symbol.js";
import { getSymbol } from "../primitives/type.js";
@ -21,16 +21,17 @@ export const makeTypeParser = ({
extraInfixOperators=[],
}) => {
const primitives = new Map([
['Int', Int],
['Double', Double],
['Bool', Bool],
['Char', Char],
['String', lsType(_ => Char)],
['Module', lsType(_ => Dynamic)],
['Unit', Unit],
['Type', Type],
['Dynamic', Dynamic],
['UUID', UUID],
['Int' , Int ],
['Double' , Double ],
['Bool' , Bool ],
['Char' , Char ],
['String' , lsType(_ => Char) ],
['Module' , lsType(_ => Dynamic)],
['Unit' , Unit ],
['Type' , Type ],
['Dynamic' , Dynamic ],
['UUID' , UUID ],
['Ordering', Ordering ],
...TYPE_VARS.map(type => [getHumanReadableName(getSymbol(type)), type]),
@ -38,21 +39,21 @@ export const makeTypeParser = ({
]);
const bracketOperators = new Map([
['(', [')', null]],
['[', [']', lsType]],
['(', [')', null ]],
['[', [']', lsType ]],
['{', ['}', setType]],
...extraBracketOperators,
]);
const infixOperators = new Map([
['+', sumType],
['|', sumType],
['⨯', prodType],
['*', prodType],
['→', fnType],
['->', fnType],
['⇒', dictType],
['+' , sumType ],
['|' , sumType ],
['⨯' , prodType],
['*' , prodType],
['→' , fnType ],
['->', fnType ],
['⇒' , dictType],
['=>', dictType],
...extraInfixOperators,

5
lib/primitives/primitive_types.js
View file

@ -14,6 +14,9 @@ export const SymbolType = "Type__fdbea309d66f49b483b0dd4ceb785f7d";
export const SymbolTop = "⊤__38709c3c0039468782103256d4730d1f";
export const SymbolDynamic = "Dynamic__3c16c415dba94228ada37dc9d446f54f";
export const SymbolOrdering = "Ordering__a11578cc83352023f16ffa2d060c52c2";
export const Int = makeTypeConstructor(SymbolInt)(0);
export const Bool = makeTypeConstructor(SymbolBool)(0);
export const Double = makeTypeConstructor(SymbolDouble)(0);
@ -35,3 +38,5 @@ export const Type = makeTypeConstructor(SymbolType)(0);
export const Top = makeTypeConstructor(SymbolTop)(0);// A type-link, connecting a value to its Type.
export const Dynamic = makeTypeConstructor(SymbolDynamic)(0);
export const Ordering = makeTypeConstructor(SymbolOrdering)(0);

48
lib/primitives/primitive_types.types.js
View file

@ -1,30 +1,32 @@
import { newDynamic } from "./dynamic.js";
import { SymbolInt, UUID, SymbolBool, SymbolDouble, SymbolByte, SymbolChar, SymbolUnit, SymbolBottom, SymbolUUID, SymbolType, SymbolTop, Type, Int, Bool, Double, Byte, Char, Unit, Bottom, Top, SymbolDynamic, Dynamic } from "./primitive_types.js";
import { SymbolInt, UUID, SymbolBool, SymbolDouble, SymbolByte, SymbolChar, SymbolUnit, SymbolBottom, SymbolUUID, SymbolType, SymbolTop, Type, Int, Bool, Double, Byte, Char, Unit, Bottom, Top, SymbolDynamic, Dynamic, SymbolOrdering, Ordering } from "./primitive_types.js";
export const ModulePrimitiveSymbols = [
newDynamic(SymbolInt )(UUID),
newDynamic(SymbolBool )(UUID),
newDynamic(SymbolDouble )(UUID),
newDynamic(SymbolByte )(UUID),
newDynamic(SymbolChar )(UUID),
newDynamic(SymbolUnit )(UUID),
newDynamic(SymbolBottom )(UUID),
newDynamic(SymbolUUID )(UUID),
newDynamic(SymbolType )(UUID),
newDynamic(SymbolTop )(UUID),
newDynamic(SymbolDynamic)(UUID),
newDynamic(SymbolInt )(UUID),
newDynamic(SymbolBool )(UUID),
newDynamic(SymbolDouble )(UUID),
newDynamic(SymbolByte )(UUID),
newDynamic(SymbolChar )(UUID),
newDynamic(SymbolUnit )(UUID),
newDynamic(SymbolBottom )(UUID),
newDynamic(SymbolUUID )(UUID),
newDynamic(SymbolType )(UUID),
newDynamic(SymbolTop )(UUID),
newDynamic(SymbolDynamic )(UUID),
newDynamic(SymbolOrdering)(UUID),
];
export const ModulePrimitiveTypes = [
newDynamic(Int )(Type),
newDynamic(Bool )(Type),
newDynamic(Double )(Type),
newDynamic(Byte )(Type),
newDynamic(Char )(Type),
newDynamic(Unit )(Type),
newDynamic(Bottom )(Type),
newDynamic(UUID )(Type),
newDynamic(Type )(Type),
newDynamic(Top )(Type),
newDynamic(Dynamic)(Type),
newDynamic(Int )(Type),
newDynamic(Bool )(Type),
newDynamic(Double )(Type),
newDynamic(Byte )(Type),
newDynamic(Char )(Type),
newDynamic(Unit )(Type),
newDynamic(Bottom )(Type),
newDynamic(UUID )(Type),
newDynamic(Type )(Type),
newDynamic(Top )(Type),
newDynamic(Dynamic )(Type),
newDynamic(Ordering)(Type),
];

2
lib/stdlib.js
View file

@ -16,6 +16,7 @@ import { ModuleStructuralSymbols, ModuleTypeConstructors } from "./structures/ty
import { ModuleCompareTypes } from "./compare/type.types.js";
import { ModuleComparePrimitives } from "./compare/primitives.types.js";
import { ModuleCompareStructures } from "./compare/structures.types.js";
import { ModuleCompareDynamic } from "./compare/dynamic.types.js";
export const ModuleStd = [
// Symbols (for nominal types)
@ -45,4 +46,5 @@ export const ModuleStd = [
...ModuleCompareTypes,
...ModuleComparePrimitives,
...ModuleCompareStructures,
...ModuleCompareDynamic,
];