Adding some sigs. Fixing recrusion in type checking

This commit is contained in:
Dustin Swan 2026-03-26 19:16:48 -06:00
parent b97eb52c21
commit 635f12490d
No known key found for this signature in database
GPG key ID: 30D46587E2100467
2 changed files with 47 additions and 10 deletions

View file

@ -21,14 +21,12 @@ map : (a \ b) \ List a \ List b = f list \ list
| [] \ [] | [] \ []
| [x, ...xs] \ [f x, ...map f xs]; | [x, ...xs] \ [f x, ...map f xs];
# mapWithIndex : (a \ Number \ b) \ List a \ List b mapWithIndex : (a \ Number \ b) \ List a \ List b = f list \
mapWithIndex = f list \
init = { i = 0, result = [] }; init = { i = 0, result = [] };
f2 = acc x \ { i = acc.i + 1, result = [...acc.result, f x acc.i] }; f2 = acc x \ { i = acc.i + 1, result = [...acc.result, f x acc.i] };
(fold f2 init list).result; (fold f2 init list).result;
# index : a \ List a \ Maybe Int index : a \ List a \ Maybe Int = x xs \
index = x xs \
go = i rest \ rest go = i rest \ rest
| [] \ None | [] \ None
| [y, ...ys] \ (x == y | [y, ...ys] \ (x == y
@ -36,8 +34,8 @@ index = x xs \
| False \ go (i + 1) ys); | False \ go (i + 1) ys);
go 0 xs; go 0 xs;
# filter : (a \ Bool) \ List a \ List a # filter
filter = f list \ list filter : (a \ Bool) \ List a \ List a = f list \ list
| [] \ [] | [] \ []
| [x, ...xs] \ (f x | [x, ...xs] \ (f x
| True \ [x, ...filter f xs] | True \ [x, ...filter f xs]

View file

@ -33,8 +33,16 @@ function unify(t1: TypeAST, t2: TypeAST, subst: Subst): string | null {
if (a.kind === 'type-name' && b.kind === 'type-name' && a.name === b.name) return null; if (a.kind === 'type-name' && b.kind === 'type-name' && a.name === b.name) return null;
// Type var binds to anything // Type var binds to anything
if (a.kind === 'type-var') { subst.set(a.name, b); return null; } if (a.kind === 'type-var') {
if (b.kind === 'type-var') { subst.set(b.name, a); return null; } if (occursIn(a.name, b, subst)) return `Infinite type: ${a.name} occurs in ${prettyPrintType(b)}`;
subst.set(a.name, b);
return null;
}
if (b.kind === 'type-var') {
if (occursIn(b.name, a, subst)) return `Infinite type: ${b.name} occurs in ${prettyPrintType(a)}`;
subst.set(b.name, a);
return null;
}
// Functions: unify param & result // Functions: unify param & result
if (a.kind === 'type-function' && b.kind === 'type-function') { if (a.kind === 'type-function' && b.kind === 'type-function') {
@ -80,12 +88,12 @@ function infer(expr: AST, env: TypeEnv, subst: Subst): TypeAST | null {
case 'variable': { case 'variable': {
const t = env.get(expr.name); const t = env.get(expr.name);
return t ? applySubst(t, subst) : null; return t ? freshen(t, subst) : null;
} }
case 'constructor': { case 'constructor': {
const t = env.get(expr.name); const t = env.get(expr.name);
return t ? applySubst(t, subst) : null; return t ? freshen(t, subst) : null;
} }
case 'list': { case 'list': {
@ -285,3 +293,34 @@ export function typecheck(defs: Definition[]) {
} }
} }
} }
function occursIn(name: string, type: TypeAST, subst: Subst): boolean {
const t = applySubst(type, subst);
switch (t.kind) {
case 'type-var': return t.name === name;
case 'type-name': return false;
case 'type-function': return occursIn(name, t.param, subst) || occursIn(name, t.result, subst);
case 'type-apply': return occursIn(name, t.constructor, subst) || t.args.some(a => occursIn(name, a, subst));
case 'type-record': return t.fields.some(f => occursIn(name, f.type, subst));
}
}
let freshCounter = 0;
function freshen(type: TypeAST, subst: Subst): TypeAST {
const vars = new Map<string, TypeAST>();
function go(t: TypeAST): TypeAST {
const resolved = applySubst(t, subst);
switch (resolved.kind) {
case 'type-var':
if (!vars.has(resolved.name)) {
vars.set(resolved.name, { kind: 'type-var', name: `_t${freshCounter++}` });
}
return vars.get(resolved.name)!;
case 'type-name': return resolved;
case 'type-function': return { kind: 'type-function', param: go(resolved.param), result: go(resolved.result) };
case 'type-apply': return { kind: 'type-apply', constructor: go(resolved.constructor), args: resolved.args.map(go) };
case 'type-record': return { kind: 'type-record', fields: resolved.fields.map(f => ({ name: f.name, type: go(f.type) })) };
}
}
return go(type);
}