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

Type inference for recursive let...in... working. Update factorial example.

Browse source
This commit is contained in:
Joeri Exelmans 2025-05-26 14:59:17 +02:00
parent d000839878
commit 2279c54229
5 changed files with 62 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

50
src/eval/infer_type.ts
View file

@ -1,10 +1,11 @@
import { Double, eqType, fnType, IncompatibleTypesError, Int, mergeSubstitutionsN, occurring, prettyS, prettySS, prettyT, recomputeTypeVars, substitute, SubstitutionCycle, trie, TYPE_VARS, UNBOUND_SYMBOLS, unify } from "dope2";
import { Double, eqType, fnType, IncompatibleTypesError, Int, mergeSubstitutionsN, occurring, recomputeTypeVars, substitute, SubstitutionCycle, trie, TYPE_VARS, UNBOUND_SYMBOLS, unify } from "dope2";
import type { CallBlockState } from "../component/expr/CallBlock";
import type { ExprBlockState } from "../component/expr/ExprBlock";
import type { InputBlockState } from "../component/expr/InputBlock";
import type { LambdaBlockState } from "../component/expr/LambdaBlock";
import type { LetInBlockState } from "../component/expr/LetInBlock";
import { memoize } from "../util/memoize";
export interface Environment {
names: any;
@ -48,7 +49,7 @@ export interface TypeInfoLambda extends TypeInfoCommon {
export type TypeInfo = TypeInfoInput | TypeInfoCall | TypeInfoLet | TypeInfoLambda;
export function inferType(s: ExprBlockState, env: Environment): TypeInfo {
export const inferType = memoize(function inferType(s: ExprBlockState, env: Environment): TypeInfo {
if (s.kind === "input") {
return inferTypeInput(s, env);
}
@ -61,9 +62,9 @@ export function inferType(s: ExprBlockState, env: Environment): TypeInfo {
else { // (s.kind === "lambda")
return inferTypeLambda(s, env);
}
}
});
export function inferTypeInput(s: InputBlockState, env: Environment): TypeInfoInput {
export const inferTypeInput = memoize(function inferTypeInput(s: InputBlockState, env: Environment): TypeInfoInput {
if (s.value.kind === "literal") {
const type = {
Int: Int,
@ -99,9 +100,9 @@ export function inferTypeInput(s: InputBlockState, env: Environment): TypeInfoIn
newEnv,
err: new Error("Gibberish"),
}
}
});
export function inferTypeCall(s: CallBlockState, env: Environment): TypeInfoCall {
export const inferTypeCall = memoize(function inferTypeCall(s: CallBlockState, env: Environment): TypeInfoCall {
const fnTypeInfo = inferType(s.fn, env);
const inputEnv = fnTypeInfo.newEnv;
const inputTypeInfo = inferType(s.input, inputEnv);
@ -159,46 +160,55 @@ export function inferTypeCall(s: CallBlockState, env: Environment): TypeInfoCall
}
throw e;
}
}
});
export function inferTypeLet(s: LetInBlockState, env: Environment): TypeInfoLet {
const valTypeInfo = inferType(s.value, env);
export const inferTypeLet = memoize(function inferTypeLet(s: LetInBlockState, env: Environment): TypeInfoLet {
const recursiveTypeInfo = iterateRecursiveType(s.name, s.value, env);
// to eval the 'inner' expr, we only need to add our parameter to the environment:
const innerEnv = {
names: trie.insert(env.names)(s.name)({kind: "value", t: valTypeInfo.type}),
names: trie.insert(env.names)(s.name)({kind: "value", t: recursiveTypeInfo.paramType}),
typevars: env.typevars,
};
const innerTypeInfo = inferType(s.inner, innerEnv);
return {
kind: "let",
type: innerTypeInfo.type,
value: recursiveTypeInfo.inner,
subs: innerTypeInfo.subs,
newEnv: env,
value: valTypeInfo,
newEnv: innerTypeInfo.newEnv,
inner: innerTypeInfo,
innerEnv,
};
}
});
export const inferTypeLambda = memoize(function inferTypeLambda(s: LambdaBlockState, env: Environment): TypeInfoLambda {
const recursiveTypeInfo = iterateRecursiveType(s.paramName, s.expr, env);
return {
kind: "lambda",
type: fnType(_ => recursiveTypeInfo.paramType)(_ => recursiveTypeInfo.inner.type),
...recursiveTypeInfo,
};
});
export function inferTypeLambda(s: LambdaBlockState, env: Environment): TypeInfoLambda {
// Given a named value whose type we know nothing about, and an expression that computes the value (which may recursively contain the value), compute the type of the value.
// Why? Both lambda functions and let-expressions can refer to themselves recursively. To infer their type, we need to recompute the type and feed it back to itself until some fixed point is reached.
function iterateRecursiveType(paramName: string, expr: ExprBlockState, env: Environment) {
let [paramType] = typeUnknown(env);
const paramTypeVar = paramType.symbol;
let iterations = 1;
while (true) {
const innerEnv = {
names: trie.insert(env.names)(s.paramName)({kind: "unknown", t: paramType}),
names: trie.insert(env.names)(paramName)({kind: "unknown", t: paramType}),
typevars: env.typevars.union(occurring(paramType) as Set<string>),
};
const innerTypeInfo = inferType(s.expr, innerEnv);
const innerTypeInfo = inferType(expr, innerEnv);
const subsWithoutPType = new Map(innerTypeInfo.subs);
subsWithoutPType.delete(paramTypeVar);
const inferredPType = substitute(paramType, innerTypeInfo.subs, []);
const [inferredPType2, newEnv] = rewriteInferredType(inferredPType, env);
if (eqType(inferredPType2)(paramType)) {
return {
kind: "lambda",
type: fnType(_ => paramType)(_ => innerTypeInfo.type),
subs: subsWithoutPType,
newEnv,
paramType,
@ -206,8 +216,8 @@ export function inferTypeLambda(s: LambdaBlockState, env: Environment): TypeInfo
innerEnv,
};
}
if ((iterations++) == 10) {
throw new Error("too many iterations!");
if ((iterations++) == 100) {
throw new Error("too many iterations! something's wrong!");
}
// console.log("-----------------", iterations);
// console.log("paramType:", prettyT(paramType));