From 635f12490daf075543ccf849dd51779092f80a8b Mon Sep 17 00:00:00 2001 From: Dustin Swan Date: Thu, 26 Mar 2026 19:16:48 -0600 Subject: [PATCH] Adding some sigs. Fixing recrusion in type checking --- src/cg/01-stdlib.cg | 10 ++++------ src/typechecker.ts | 47 +++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 47 insertions(+), 10 deletions(-) diff --git a/src/cg/01-stdlib.cg b/src/cg/01-stdlib.cg index fa8f8b3..1a6866d 100644 --- a/src/cg/01-stdlib.cg +++ b/src/cg/01-stdlib.cg @@ -21,14 +21,12 @@ map : (a \ b) \ List a \ List b = f list \ list | [] \ [] | [x, ...xs] \ [f x, ...map f xs]; -# mapWithIndex : (a \ Number \ b) \ List a \ List b -mapWithIndex = f list \ +mapWithIndex : (a \ Number \ b) \ List a \ List b = f list \ init = { i = 0, result = [] }; f2 = acc x \ { i = acc.i + 1, result = [...acc.result, f x acc.i] }; (fold f2 init list).result; -# index : a \ List a \ Maybe Int -index = x xs \ +index : a \ List a \ Maybe Int = x xs \ go = i rest \ rest | [] \ None | [y, ...ys] \ (x == y @@ -36,8 +34,8 @@ index = x xs \ | False \ go (i + 1) ys); go 0 xs; -# filter : (a \ Bool) \ List a \ List a -filter = f list \ list +# filter +filter : (a \ Bool) \ List a \ List a = f list \ list | [] \ [] | [x, ...xs] \ (f x | True \ [x, ...filter f xs] diff --git a/src/typechecker.ts b/src/typechecker.ts index 49d349a..fa0e83c 100644 --- a/src/typechecker.ts +++ b/src/typechecker.ts @@ -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; // Type var binds to anything - if (a.kind === 'type-var') { subst.set(a.name, b); return null; } - if (b.kind === 'type-var') { subst.set(b.name, a); return null; } + if (a.kind === 'type-var') { + 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 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': { const t = env.get(expr.name); - return t ? applySubst(t, subst) : null; + return t ? freshen(t, subst) : null; } case 'constructor': { const t = env.get(expr.name); - return t ? applySubst(t, subst) : null; + return t ? freshen(t, subst) : null; } 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(); + 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); +}