From c3f7cea310b42569648a527c0499d5b016de94db Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Wed, 21 May 2025 00:13:17 +0200 Subject: [PATCH] fix bug in type inferencing --- src/App.tsx | 4 +- src/EnvContext.ts | 3 + src/ExprBlock.css | 24 +++- src/ExprBlock.tsx | 5 +- src/Input.tsx | 1 + src/LambdaBlock.tsx | 18 +-- src/configurations.ts | 4 +- src/eval.ts | 301 +++++++++++++++++++++++------------------- 8 files changed, 205 insertions(+), 155 deletions(-) diff --git a/src/App.tsx b/src/App.tsx index c571039..d36970d 100644 --- a/src/App.tsx +++ b/src/App.tsx @@ -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 = { diff --git a/src/EnvContext.ts b/src/EnvContext.ts index 9717ae4..a23d4c4 100644 --- a/src/EnvContext.ts +++ b/src/EnvContext.ts @@ -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]) diff --git a/src/ExprBlock.css b/src/ExprBlock.css index 97e0ea3..e579fcd 100644 --- a/src/ExprBlock.css +++ b/src/ExprBlock.css @@ -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 { diff --git a/src/ExprBlock.tsx b/src/ExprBlock.tsx index e702b7f..0967780 100644 --- a/src/ExprBlock.tsx +++ b/src/ExprBlock.tsx @@ -51,8 +51,11 @@ export function ExprBlock(props: ExprBlockProps) { return {renderBlock[props.state.kind]()} -
+ {/* @ts-ignore */} +
 ::  + {/* @ts-ignore */} + {resolved.__debug &&
{resolved.__debug}
}
{ if (text.length === 0) { onCancel(); + focusPrevElement(); e.preventDefault(); } }, diff --git a/src/LambdaBlock.tsx b/src/LambdaBlock.tsx index f5ddbab..f969b9a 100644 --- a/src/LambdaBlock.tsx +++ b/src/LambdaBlock.tsx @@ -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,20 +36,10 @@ 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 = lambdaResolved.t.params[0](lambdaResolved.t); - 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? - }); - return λ   @@ -71,7 +61,7 @@ export function LambdaBlock({state, setState, score}: LambdaBlockProps) { :  
- + 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("", fnResolved, env2); } - return evalCallBlock2(fnResolved, inputResolved, env3); + let [inputResolved, env3] = evalExprBlock(input, env2); + if (inputResolved.kind === "value") { + [inputResolved, env3] = recomputeTypeVarsForEnv("", 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; 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, ""); 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, @@ -196,26 +214,25 @@ function evalCallBlock3(fnResolved: ResolvedType, inputResolved: ResolvedType, e // we don't want to 'bubble up' our outType substitution, because it's just a temporary variable 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; @@ -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) => { 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 + + 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, + } + } - if (VERBOSE) { - console.log('====== begin evalLambdaBlock ======') - console.log('paramName :', paramName); - console.log('paramType :', prettyT(paramType)); - console.log('staticInnerEnv:', staticInnerEnv); - console.log('===================================') - } + const [betterResolved, newInnerEnv] = recomputeTypeVarsForEnv("", lambdaResolved, env); - 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 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] { @@ -413,23 +448,17 @@ 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! } }