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

fix bug in type inferencing

Browse source
This commit is contained in:
Joeri Exelmans 2025-05-21 00:13:17 +02:00
parent bb6e742f5f
commit c3f7cea310
8 changed files with 205 additions and 155 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/App.tsx
View file

@ -2,10 +2,9 @@ import { useEffect, useState } from 'react';
import './App.css';
import { ExprBlock, type ExprBlockState } from './ExprBlock';
import { GlobalContext } from './GlobalContext';
import { biggerExample, emptySet, higherOrder, higherOrder2Params, inc, initialEditorState, lambda2Params, nonEmptyEditorState, pushBool, tripleFunctionCallEditorState } from "./configurations";
import { biggerExample, emptySet, factorial, higherOrder, higherOrder2Params, inc, initialEditorState, lambda2Params, nonEmptyEditorState, pushBool, tripleFunctionCallEditorState } from "./configurations";
import { actionShortcuts } from './actions';
import { scoreResolved, type ResolvedType } from './eval';
import type { InputBlockState } from './InputBlock';
const examples: [string, ExprBlockState][] = [
@ -19,6 +18,7 @@ const examples: [string, ExprBlockState][] = [
["push Bool" , pushBool ],
["inc" , inc ],
["empty set" , emptySet ],
["factorial" , factorial ],
];
type AppState = {

3
src/EnvContext.ts
View file

@ -9,6 +9,9 @@ const mkType = getDefaultTypeParser();
export const extendedEnv: Environment = {
names: module2Env(ModuleStd.concat([
["true", {i: true, t: mkType("Bool")}],
["false", {i: false, t: mkType("Bool")}],
["leqZero", {i: n => leq => otherwise => (n<=0)?leq({}):otherwise({}), t: mkType("Int -> (Unit -> a) -> (Unit -> a) -> a")}],
["functionWith3Params", { i: functionWith3Params, t: mkType("Int->Int->Int->Int") }],
["functionWith4Params", { i: functionWith4Params, t: mkType("Int->Int->Int->Int->Int")}]
]).map(([name, {i,t}]) => [name, { kind: "value", i, t, unification: new Map() }] as [string, Dynamic])

24
src/ExprBlock.css
View file

@ -21,7 +21,29 @@
.typeSignature {
display: inline-block;
z-index: 1;
/* z-index: 1; */
position: relative;
}
.typeSignature.gotDebug {
background-color: gold;
padding: 2px;
}
.typeDebug {
display: none;
}
.typeSignature:hover > .typeDebug {
display: inline-block;
position: absolute;
white-space-collapse: preserve;
width: max-content;
background-color: #d2ebf1e0;
color: black;
font-family: var(--my-monospace-font);
padding: 4px;
z-index: 1000;
}
.editor:hover > .typeSignature {

5
src/ExprBlock.tsx
View file

@ -51,8 +51,11 @@ export function ExprBlock(props: ExprBlockProps) {
return <span className={"editor" + ((resolved.kind!=="value") ? " "+resolved.kind : "")}>
{renderBlock[props.state.kind]()}
<div className="typeSignature">
{/* @ts-ignore */}
<div className={"typeSignature" + (resolved.__debug ? ' gotDebug' : '')}>
&nbsp;::&nbsp;<Type type={getType(resolved)} />
{/* @ts-ignore */}
{resolved.__debug && <div className="typeDebug">{resolved.__debug}</div>}
</div>
<Input
placeholder="<c>"

1
src/Input.tsx
View file

@ -94,6 +94,7 @@ export function Input({placeholder, text, suggestion, onTextChange, onEnter, onC
Backspace: () => {
if (text.length === 0) {
onCancel();
focusPrevElement();
e.preventDefault();
}
},

18
src/LambdaBlock.tsx
View file

@ -4,7 +4,7 @@ import { eqType, getSymbol, reduceUnification } from "dope2";
import { ExprBlock, type ExprBlockState, type State2Props } from "./ExprBlock";
import { EnvContext } from "./EnvContext";
import { evalExprBlock, makeInnerEnv, makeTypeVar } from "./eval";
import { evalExprBlock, evalLambdaBlock, makeInnerEnv, makeTypeVar } from "./eval";
import "./LambdaBlock.css";
import { Type } from "./Type";
@ -36,19 +36,9 @@ export function LambdaBlock({state, setState, score}: LambdaBlockProps) {
expr: callback(state.expr),
}));
const [paramType, staticInnerEnv] = makeTypeVar(env, state.paramName);
const [lambdaResolved, _, innerEnv] = evalLambdaBlock(state.paramName, state.expr, env);
const [exprResolved] = evalExprBlock(state.expr, staticInnerEnv);
const inferredParamType = reduceUnification(exprResolved.unification).get(getSymbol(paramType)) || paramType;
const betterInnerEnv = eqType(paramType)(inferredParamType)
? staticInnerEnv
: makeInnerEnv(env, state.paramName, {
kind: "unknown",
t: inferredParamType,
unification: new Map(), // <- is this correct?
});
const inferredParamType = lambdaResolved.t.params[0](lambdaResolved.t);
return <span className="lambdaBlock">
<span className="keyword">&#955;</span>
@ -71,7 +61,7 @@ export function LambdaBlock({state, setState, score}: LambdaBlockProps) {
<span className="keyword">:</span>
&nbsp;
<div className="lambdaInner">
<EnvContext value={betterInnerEnv}>
<EnvContext value={innerEnv}>
<ExprBlock
state={state.expr}
setState={setExpr}

2
src/configurations.ts
View file

@ -140,3 +140,5 @@ export const pushBool: ExprBlockState = {"kind":"call","fn":{"kind":"call","fn":
export const inc: ExprBlockState = {"kind":"let","focus":false,"inner":{"kind":"input","text":"","value":{"kind":"name"},"focus":false},"name":"inc","value":{"kind":"lambda","focus":false,"paramName":"x","expr":{"kind":"call","fn":{"kind":"call","fn":{"kind":"input","text":"addInt","value":{"kind":"name"},"focus":false},"input":{"kind":"input","text":"x","value":{"kind":"name"},"focus":false}},"input":{"kind":"input","text":"1","value":{"kind":"literal","type":"Int"},"focus":true}}}};
export const emptySet: ExprBlockState = {"kind":"call","fn":{"kind":"input","text":"set.emptySet","value":{"kind":"name"},"focus":false},"input":{"kind":"input","text":"","value":{"kind":"text"},"focus":true}};
export const factorial: ExprBlockState = {"kind":"lambda","paramName":"factorial","focus":true,"expr":{"kind":"lambda","paramName":"n","focus":true,"expr":{"kind":"call","fn":{"kind":"call","fn":{"kind":"call","fn":{"kind":"input","text":"leqZero","value":{"kind":"name"},"focus":false},"input":{"kind":"input","text":"n","value":{"kind":"name"},"focus":false}},"input":{"kind":"lambda","paramName":"_","focus":false,"expr":{"kind":"input","text":"1","value":{"kind":"literal","type":"Int"},"focus":false}}},"input":{"kind":"lambda","paramName":"_","focus":false,"expr":{"kind":"call","fn":{"kind":"call","fn":{"kind":"input","text":"mulInt","value":{"kind":"name"},"focus":false},"input":{"kind":"input","text":"n","value":{"kind":"name"},"focus":true}},"input":{"kind":"call","fn":{"kind":"input","text":"factorial","value":{"kind":"name"},"focus":true},"input":{"kind":"call","fn":{"kind":"call","fn":{"kind":"input","text":"addInt","value":{"kind":"name"},"focus":false},"input":{"kind":"input","text":"n","value":{"kind":"name"},"focus":false}},"input":{"kind":"input","text":"-1","value":{"kind":"literal","type":"Int"},"focus":false}}}}}}}};

299
src/eval.ts
View file

@ -1,10 +1,10 @@
import { Double, fnType, getHumanReadableName, getSymbol, Int, isTypeVar, mergeUnifications, NotAFunctionError, occurring, prettyT, prettyU, recomputeTypeVarsWithInverse, reduceUnification, substitute, symbolFunction, trie, TYPE_VARS, UNBOUND_SYMBOLS, UnifyError, unifyLL } from "dope2";
import { Double, eqType, fnType, getHumanReadableName, getSymbol, Int, isTypeVar, mergeUnifications, NotAFunctionError, occurring, prettyT, prettyU, recomputeTypeVarsWithInverse, reduceUnification, substitute, symbolFunction, transitivelyGrow, trie, TYPE_VARS, UNBOUND_SYMBOLS, UnifyError, unifyLL } from "dope2";
import type { ExprBlockState } from "./ExprBlock";
import type { InputValueType } from "./InputBlock";
const IS_DEV = (import.meta.env.MODE === "development");
const VERBOSE = true;
const VERBOSE = true && IS_DEV;
export interface Environment {
names: any;
@ -57,7 +57,8 @@ export const evalExprBlock = (s: ExprBlockState, env: Environment): [ResolvedTyp
return evalLetInBlock(s.value, s.name, s.inner, env);
}
else { // (s.kind === "lambda")
return evalLambdaBlock(s.paramName, s.expr, env);
const [resolved, env2] = evalLambdaBlock(s.paramName, s.expr, env);
return [resolved, env2];
}
};
@ -68,15 +69,9 @@ export function evalInputBlock(text: string, value: InputValueType, env: Environ
else if (value.kind === "name") {
const found = trie.get(env.names)(text);
if (found) {
if (found.kind === "unknown") {
// console.log('returning', text, 'as-is');
return [found, env]; // don't rewrite lambda parameters
}
// console.log('rewriting', text);
return recomputeTypeVarsForEnv(text, found, env);
return [found, env]; // don't rewrite lambda parameters
}
}
// kind === "text" -> unresolved
const [t, env2] = makeTypeVar(env, 'err')
return [{
kind: "error",
@ -88,24 +83,35 @@ export function evalInputBlock(text: string, value: InputValueType, env: Environ
}
export function evalCallBlock(fn: ExprBlockState, input: ExprBlockState, env: Environment): [ResolvedType,Environment] {
const [fnResolved, env2] = evalExprBlock(fn, env);
const [inputResolved, env3] = evalExprBlock(input, env2);
if (VERBOSE) {
console.log('==== evalCallBlock ====');
console.log('env :', env);
console.log('fnResolved :', fnResolved);
console.log('env2 :', env2);
console.log('inputResolved:', inputResolved);
console.log('env3 :', env3);
console.log('=======================');
let [fnResolved, env2] = evalExprBlock(fn, env);
if (fnResolved.kind === "value") {
[fnResolved, env2] = recomputeTypeVarsForEnv("<name unused>", fnResolved, env2);
}
return evalCallBlock2(fnResolved, inputResolved, env3);
let [inputResolved, env3] = evalExprBlock(input, env2);
if (inputResolved.kind === "value") {
[inputResolved, env3] = recomputeTypeVarsForEnv("<name unused>", inputResolved, env3);
}
const result = evalCallBlock2(fnResolved, inputResolved, env3);
if (VERBOSE) {
// @ts-ignore
result[0].__debug = (result[0].__debug || '') + `
==== evalCallBlock ====
env.typeVars : ${[...env.typeVars].map(getHumanReadableName)}
env.nextFreeTypeVar: ${getHumanReadableName(UNBOUND_SYMBOLS[env.nextFreeTypeVar])}
fn.kind : ${fn.kind}
fn.t : ${prettyT(fnResolved.t)}
env2.typeVars : ${[...env2.typeVars].map(getHumanReadableName)}
env2.nextFreeTypeVar: ${getHumanReadableName(UNBOUND_SYMBOLS[env2.nextFreeTypeVar])}
input.kind : ${input.kind}
input.t : ${prettyT(inputResolved.t)}
env3.typeVars : ${[...env3.typeVars].map(getHumanReadableName)}
env3.nextFreeTypeVar: ${getHumanReadableName(UNBOUND_SYMBOLS[env3.nextFreeTypeVar])}
=======================`;
}
return result;
}
export function evalCallBlock2(fnResolved: ResolvedType, inputResolved: ResolvedType, env: Environment): [ResolvedType,Environment] {
if (occurring(fnResolved.t).intersection(occurring(inputResolved.t)).size > 0) {
throw new Error(`Precondition failed: function (${prettyT(fnResolved.t)}) and its input (${prettyT(inputResolved.t)}) have overlapping typevars!`);
}
if (getSymbol(fnResolved.t) !== symbolFunction) {
// not a function...
if (isTypeVar(fnResolved.t)) {
@ -157,7 +163,8 @@ export function recomputeTypeVarsForEnv(name: string, resolved: ResolvedType, en
// hacky
const typeVars = env.typeVars.union(occurring(newType)) as Set<string>;
const newEnv: Environment = {
names: trie.insert(env.names)(name)(newResolved),
// names: trie.insert(env.names)(name)(newResolved),
names: env.names,
typeVars,
nextFreeTypeVar: highestTypeVar2(typeVars) + 1,
};
@ -166,24 +173,35 @@ export function recomputeTypeVarsForEnv(name: string, resolved: ResolvedType, en
}
function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, env: Environment): [ResolvedType,Environment] {
let __debug = '';
try {
if (occurring(fnResolved.t).intersection(occurring(inputResolved.t)).size > 0) {
throw new Error(`Precondition failed: function (${prettyT(fnResolved.t)}) and its input (${prettyT(inputResolved.t)}) have overlapping typevars!`);
}
// turn input in to a function
const [abstractOutputType, env2] = makeTypeVar(env, "<out>");
const matchFnType = fnType(_ => inputResolved.t)(_ => abstractOutputType);
if (VERBOSE) {
console.log('========= evalCallBlock3 =========')
console.log('env :', env);
console.log('fnKind :', fnResolved.kind);
console.log('inputKind :', inputResolved.kind);
console.log('fnType :', prettyT(fnResolved.t));
console.log('inputType :', prettyT(inputResolved.t));
console.log('matchFnType :', prettyT(matchFnType));
__debug += `========= evalCallBlock3 =========
env.typeVars : ${[...env.typeVars].map(getHumanReadableName)}
nextFreeTypeVar: ${getHumanReadableName(UNBOUND_SYMBOLS[env.nextFreeTypeVar])}
fnKind : ${fnResolved.kind}
inputKind : ${inputResolved.kind}
fnType : ${prettyT(fnResolved.t)}
inputType : ${prettyT(inputResolved.t)}
matchFnType : ${prettyT(matchFnType)}`;
}
// unify both functions
const unification = /*transitivelyGrow*/(unifyLL(fnResolved.t, matchFnType));
if (VERBOSE) {
__debug += `
unification : ${prettyU(unification)}`;
}
const unificationR = reduceUnification(unification);
const unifiedFnType = substitute(
// matchFnType,
@ -198,25 +216,24 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e
const unificationWithoutOutType = new Map([...unification].filter(([symbol]) => symbol !== abstractOutputType.symbol));
if (VERBOSE) {
console.log('unification :', prettyU(unification));
console.log('unificationInvR :', prettyRU(unificationR));
console.log('unifiedFnType :', prettyT(unifiedFnType));
console.log('outType :', prettyT(outType));
console.log('fn.unification :', prettyU(fnResolved.unification));
console.log('input.unification :', prettyU(inputResolved.unification));
console.log('unificationWithoutOutType:', prettyU(unificationWithoutOutType));
__debug += `
unificationInvR : ${prettyRU(unificationR)}
unifiedFnType : ${prettyT(unifiedFnType)}
outType : ${prettyT(outType)}
fn.unification : ${prettyU(fnResolved.unification)}
input.unification : ${prettyU(inputResolved.unification)}
unificationWithoutOutType: ${prettyU(unificationWithoutOutType)}`;
}
const grandUnification = [fnResolved.unification, inputResolved.unification]
.reduce(mergeUnifications, unificationWithoutOutType);
// const grandUnification = unificationWithoutOutType;
const grandUnification = transitivelyGrow([fnResolved.unification, inputResolved.unification]
.reduce(mergeUnifications, unificationWithoutOutType));
if (VERBOSE) {
console.log('grandUnification :', prettyU(grandUnification));
console.log('==================================')
__debug += `
grandUnification : ${prettyU(grandUnification)}`;
}
if (inputResolved.kind === "error") {
// throw inputResolved.e;
return [{
@ -225,6 +242,8 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e
depth: 0,
t: outType,
unification: grandUnification,
// @ts-ignore
__debug,
}, newEnv];
}
if (fnResolved.kind === "error") {
@ -236,6 +255,8 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e
depth: fnResolved.depth+1,
t: outType,
unification: grandUnification,
// @ts-ignore
__debug,
}, newEnv];
}
// if the above statement did not throw => types are compatible...
@ -247,6 +268,8 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e
i: outValue,
t: outType,
unification: grandUnification,
// @ts-ignore
__debug,
}, newEnv];
}
else {
@ -255,31 +278,22 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e
kind: "unknown",
t: outType,
unification: grandUnification,
// @ts-ignore
__debug,
}, newEnv];
}
}
catch (e) {
// if ((e instanceof UnifyError)) {
if (VERBOSE) {
console.log('UnifyError!', (e as Error).message);
}
// even though fn was incompatible with the given parameter, we can still suppose that our output-type will be that of fn...?
const outType = fnResolved.t.params[1](fnResolved.t);
try {
return [{
kind: "error",
e: e as Error,
depth: 0,
t: outType,
unification: mergeUnifications(fnResolved.unification, inputResolved.unification), // may throw!
}, env];
}
catch (e) {
if ((e instanceof UnifyError)) {
return makeError(env, e);
}
throw e;
__debug += '\n\nUnifyError! ' + (e as Error).message;
}
const err = makeError(env, e as Error);
// @ts-ignore
err[0].__debug = __debug;
return err;
// }
throw e;
}
}
@ -293,74 +307,95 @@ const prettyRU = (rUni: Map<string, Type>) => {
return '{'+[...rUni].map(([symbol,type]) => `${getHumanReadableName(symbol)} => ${prettyT(type)}`).join(', ')+'}';
}
export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env: Environment): [ResolvedType,Environment] {
const [paramType, staticInnerEnv] = makeTypeVar(env, paramName);
export function evalLambdaBlock(paramName: string, expr: ExprBlockState, env: Environment): [ResolvedType,Environment,Environment] {
let [paramType, innerEnv] = makeTypeVar(env, paramName);
let round = 0;
let __debug = '';
while (true) {
// fixpoint computation...
const [exprResolved] = evalExprBlock(expr, innerEnv);
const lambdaT = fnType(_ => paramType)(_ => exprResolved.t);
// This is the only place in the code where we actually do something with the 'substitutions'. We compute the type of our lambda function:
const reduced = reduceUnification(exprResolved.unification);
const lambdaTSubstituted = substitute(
lambdaT,
reduced,
[]); // <- not important
if (VERBOSE) {
console.log('====== begin evalLambdaBlock ======')
console.log('paramName :', paramName);
console.log('paramType :', prettyT(paramType));
console.log('staticInnerEnv:', staticInnerEnv);
console.log('===================================')
}
let lambdaResolved: ResolvedType;
if (exprResolved.kind === "error") {
lambdaResolved = {
kind: "error",
t: lambdaTSubstituted,
depth: 0,
e: exprResolved.e,
unification: exprResolved.unification,
}
}
else {
lambdaResolved = {
kind: "value",
t: lambdaTSubstituted,
i: (x: any) => {
const innerEnv = makeInnerEnv(env, paramName, {
kind: "value",
i: x,
t: lambdaTSubstituted,
unification: new Map(),
});
const [result] = evalExprBlock(expr, innerEnv);
if (result.kind === "value") {
return result.i;
}
},
unification: exprResolved.unification,
}
}
const [exprResolved] = evalExprBlock(expr, staticInnerEnv);
const lambdaT = fnType(_ => paramType)(_ => exprResolved.t);
// This is the only place in the code where we actually do something with the 'substitutions'. We compute the type of our lambda function:
const reduced = reduceUnification(exprResolved.unification);
const lambdaTSubstituted = substitute(
lambdaT,
reduced,
[]); // <- not important
let lambdaResolved: ResolvedType;
if (exprResolved.kind === "error") {
lambdaResolved = {
kind: "error",
t: lambdaTSubstituted,
depth: 0,
e: exprResolved.e,
unification: exprResolved.unification,
const [betterResolved, newInnerEnv] = recomputeTypeVarsForEnv("<name unused>", lambdaResolved, env);
const inferredParamType = betterResolved.t.params[0](betterResolved.t);
if (VERBOSE) {
__debug += `
====== evalLambdaBlock (round ${round}) ======
env.typeVars : ${[...env.typeVars].map(getHumanReadableName)}
nextFreeTypeVar: ${getHumanReadableName(UNBOUND_SYMBOLS[env.nextFreeTypeVar])}
paramName : ${paramName}
paramType : ${prettyT(paramType)}
staticInnerEnv: ${innerEnv}
paramType : ${prettyT(paramType)}
exprType : ${prettyT(exprResolved.t)}
exprUnification : ${prettyU(exprResolved.unification)}
exprUnificationR : ${prettyRU(reduced)}
lambdaType : ${prettyT(lambdaT)}
lambdaTypeSubsituted: ${prettyT(lambdaTSubstituted)}
betterResolvedT : ${prettyT(betterResolved.t)}
inferredParamType : ${prettyT(inferredParamType)}`;
}
if (eqType(paramType)(inferredParamType)) {
// reached fixpoint
// @ts-ignore
lambdaResolved.__debug = __debug;
return [lambdaResolved, env, innerEnv];
}
else {
paramType = inferredParamType;
innerEnv = {
...newInnerEnv,
names: trie.insert(newInnerEnv.names)(paramName)({
kind: "unknown",
t: inferredParamType,
unification: new Map(), // <-- ??
}),
};
round++;
if (round === 10) {
throw new Error("too many rounds!");
}
}
}
else {
const paramTypeSubstituted = lambdaTSubstituted.params[0](lambdaTSubstituted);
lambdaResolved = {
kind: "value",
t: lambdaTSubstituted,
i: (x: any) => {
const innerEnv = makeInnerEnv(env, paramName, {
kind: "value",
i: x,
t: paramTypeSubstituted,
unification: new Map(),
});
const [result] = evalExprBlock(expr, innerEnv);
if (result.kind === "value") {
return result.i;
}
},
unification: exprResolved.unification,
}
}
// const [lambdaResolvedNormalized, resultEnv] = recomputeTypeVarsForEnv(paramName, lambdaResolved, env);
if (VERBOSE) {
console.log('======= end evalLambdaBlock =======')
console.log('paramType :', prettyT(paramType));
console.log('exprType :', prettyT(exprResolved.t));
console.log('exprUnification :', prettyU(exprResolved.unification));
console.log('exprUnificationR :', prettyRU(reduced));
console.log('lambdaType :', prettyT(lambdaT));
console.log('lambdaTypeSubsituted:', prettyT(lambdaTSubstituted));
console.log('===================================')
}
return [lambdaResolved, env];
}
export function haveValue(resolved: ResolvedType) {
// return resolved && !(resolved instanceof DeepError);
return resolved.kind === "value";
}
function parseLiteral(text: string, type: string, env: Environment): [ResolvedType,Environment] {
@ -414,22 +449,16 @@ export function attemptParseLiteral(text: string, env: Environment): Dynamic[] {
export function scoreResolved(resolved: ResolvedType, outPriority: (s:ResolvedType) => number) {
const bias = outPriority(resolved);
console.log('scoreResolved...', resolved);
if (resolved.kind === "value") {
console.log('best:', 2, bias);
return 2 + bias;
return bias;
}
else if (resolved.kind === "unknown") {
console.log('ok:', 1, bias);
return 1 + bias;
return bias;
}
if (resolved.e instanceof UnifyError) {
console.log('bad:', -1, bias);
return -1 + bias; // parameter doesn't match
}
else {
console.log('worst:', -2, bias);
return -2 + bias; // even worse: fn is not a function!
}
}