Types
This commit is contained in:
parent
2b710602d3
commit
1f3a999092
2 changed files with 87 additions and 23 deletions
|
|
@ -90,7 +90,7 @@ filter : (a \ Bool) \ List a \ List a = f list \ list
|
|||
| True \ [x, ...filter f xs]
|
||||
| False \ filter f xs);
|
||||
|
||||
insertAt : Int \ a \ List a = idx el list \ list
|
||||
insertAt : Int \ a \ List a \ List a = idx el list \ list
|
||||
| [] \ [el]
|
||||
| [x, ...xs] \ (idx
|
||||
| 0 \ [el, x, ...xs]
|
||||
|
|
@ -196,7 +196,7 @@ range : Int \ Int \ List Int = start end \ start >= end
|
|||
| False \ [start, ...range (start + 1) end];
|
||||
|
||||
# TODO Number
|
||||
sum : List Int \ Int = list \ fold add 0 list;
|
||||
sum : List a \ a = list \ fold add 0 list;
|
||||
|
||||
any : (a \ Bool) \ List a \ Bool = f list \ fold (acc x \ or acc (f x)) False list;
|
||||
|
||||
|
|
|
|||
|
|
@ -91,12 +91,22 @@ function infer(expr: AST, env: TypeEnv, subst: Subst): TypeAST | null {
|
|||
|
||||
case 'variable': {
|
||||
const t = env.get(expr.name);
|
||||
return t ? freshen(t, subst) : null;
|
||||
if (!t) return null;
|
||||
const { type: fresh } = freshen(t, subst);
|
||||
|
||||
// If this variable has a typeclass constraint, record it
|
||||
const constraint = moduleConstraints.get(expr.name);
|
||||
if (constraint && fresh.kind === 'type-function' && fresh.param.kind === 'type-var') {
|
||||
inferredConstraints.push({ varName: fresh.param.name, className: constraint.className });
|
||||
}
|
||||
|
||||
return fresh;
|
||||
}
|
||||
|
||||
case 'constructor': {
|
||||
const t = env.get(expr.name);
|
||||
return t ? freshen(t, subst) : null;
|
||||
if (!t) return null;
|
||||
return freshen(t, subst).type;
|
||||
}
|
||||
|
||||
case 'list': {
|
||||
|
|
@ -148,7 +158,19 @@ function infer(expr: AST, env: TypeEnv, subst: Subst): TypeAST | null {
|
|||
}
|
||||
|
||||
case 'apply': {
|
||||
const funcType = infer(expr.func, env, subst);
|
||||
let funcType: TypeAST | null = null;
|
||||
let varMap: Map<string, string> | null = null;
|
||||
|
||||
if (expr.func.kind === 'variable') {
|
||||
const t = env.get(expr.func.name);
|
||||
if (t) {
|
||||
const result = freshen(t, subst);
|
||||
funcType = result.type;
|
||||
varMap = result.varMap;
|
||||
}
|
||||
} else {
|
||||
funcType = infer(expr.func, env, subst);
|
||||
}
|
||||
if (!funcType) return null;
|
||||
|
||||
let current = applySubst(funcType, subst);
|
||||
|
|
@ -162,21 +184,22 @@ function infer(expr: AST, env: TypeEnv, subst: Subst): TypeAST | null {
|
|||
// Check typeclass constraints
|
||||
if (expr.func.kind === 'variable') {
|
||||
const constraint = moduleConstraints.get(expr.func.name);
|
||||
if (constraint) {
|
||||
const argType = infer(expr.args[0], env, subst);
|
||||
if (argType) {
|
||||
const resolved = applySubst(argType, subst);
|
||||
if (resolved.kind === 'type-name') {
|
||||
const instances = moduleInstances.get(constraint.className);
|
||||
if (!instances || !instances.has(resolved.name)) {
|
||||
warn(`No instance ${constraint.className} ${resolved.name}`, expr);
|
||||
}
|
||||
} else if (resolved.kind === 'type-apply' && resolved.constructor.kind === 'type-name') {
|
||||
const instances = moduleInstances.get(constraint.className);
|
||||
if (!instances || !instances.has(resolved.constructor.name)) {
|
||||
warn(`No instance ${constraint.className} ${resolved.constructor.name}`, expr);
|
||||
}
|
||||
if (constraint && varMap) {
|
||||
const freshName = varMap.get(constraint.param) || constraint.param;
|
||||
const resolved = applySubst({ kind: 'type-var', name: freshName }, subst);
|
||||
|
||||
if (resolved.kind === 'type-name') {
|
||||
const instances = moduleInstances.get(constraint.className);
|
||||
if (!instances || !instances.has(resolved.name)) {
|
||||
warn(`No instance ${constraint.className} ${resolved.name}`, expr);
|
||||
}
|
||||
} else if (resolved.kind === 'type-apply' && resolved.constructor.kind === 'type-name') {
|
||||
const instances = moduleInstances.get(constraint.className);
|
||||
if (!instances || !instances.has(resolved.constructor.name)) {
|
||||
warn(`No instance ${constraint.className} ${resolved.constructor.name}`, expr);
|
||||
}
|
||||
} else if (resolved.kind === 'type-var') {
|
||||
inferredConstraints.push({ varName: resolved.name, className: constraint.className });
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -291,7 +314,7 @@ function bindPattern(pattern: Pattern, type: TypeAST, env: TypeEnv, subst: Subst
|
|||
// look up ctor types
|
||||
const ctorType = env.get(pattern.name);
|
||||
if (!ctorType) return null;
|
||||
const fresh = freshen(ctorType, subst);
|
||||
const fresh = freshen(ctorType, subst).type;
|
||||
|
||||
if (pattern.args.length === 0) {
|
||||
unify(fresh, t, subst);
|
||||
|
|
@ -325,7 +348,7 @@ function bindPattern(pattern: Pattern, type: TypeAST, env: TypeEnv, subst: Subst
|
|||
return null;
|
||||
}
|
||||
if (t.kind === 'type-var') return null;
|
||||
return `Connet match ${prettyPrintType(t)} against list pattern`;
|
||||
return `Connot match ${prettyPrintType(t)} against list pattern`;
|
||||
case 'record':
|
||||
if (t.kind === 'type-record') {
|
||||
for (const [key, pat] of Object.entries(pattern.fields)) {
|
||||
|
|
@ -341,6 +364,7 @@ function bindPattern(pattern: Pattern, type: TypeAST, env: TypeEnv, subst: Subst
|
|||
|
||||
let moduleConstraints = new Map<string, { param: string, className: string }>();
|
||||
let moduleInstances = new Map<string, Set<string>>();
|
||||
let inferredConstraints: { varName: string, className: string }[] = [];
|
||||
|
||||
export function typecheck(defs: Definition[], typeDefs: TypeDefinition[] = [], classDefs: ClassDefinition[] = [], instances: InstanceDeclaration[] = []) {
|
||||
const env: TypeEnv = new Map();
|
||||
|
|
@ -391,6 +415,8 @@ export function typecheck(defs: Definition[], typeDefs: TypeDefinition[] = [], c
|
|||
for (const def of defs) {
|
||||
if (def.body) {
|
||||
const subst: Subst = new Map();
|
||||
inferredConstraints = []; // reset
|
||||
|
||||
if (def.annotation) {
|
||||
const err = check(def.body, def.annotation.type, env, subst);
|
||||
if (err) warn(err, def.body);
|
||||
|
|
@ -398,6 +424,37 @@ export function typecheck(defs: Definition[], typeDefs: TypeDefinition[] = [], c
|
|||
const t = infer(def.body, env, subst);
|
||||
if (t) env.set(def.name, t);
|
||||
}
|
||||
|
||||
// Propagate inferred constraints to this definition
|
||||
if (inferredConstraints.length > 0 && def.annotation) {
|
||||
// Collect annotation var names
|
||||
const annoVars = new Set<string>();
|
||||
function collectVars(t: TypeAST) {
|
||||
if (t.kind === 'type-var') annoVars.add(t.name);
|
||||
if (t.kind === 'type-function') { collectVars(t.param); collectVars(t.result); }
|
||||
if (t.kind === 'type-apply') { collectVars(t.constructor); t.args.forEach(collectVars); }
|
||||
if (t.kind === 'type-record') t.fields.forEach(f => collectVars(f.type));
|
||||
}
|
||||
collectVars(def.annotation.type);
|
||||
|
||||
for (const ic of inferredConstraints) {
|
||||
// Walk subst chain to find which annotation var this connects to
|
||||
let found: string | null = null;
|
||||
for (const av of annoVars) {
|
||||
const resolved = applySubst({ kind: 'type-var', name: av }, subst);
|
||||
const icResolved = applySubst({ kind: 'type-var', name: ic.varName }, subst);
|
||||
// If they resolve to the same thing, this annotation var is the one
|
||||
if (unify(resolved, icResolved, new Map(subst)) === null) {
|
||||
found = av;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (found) {
|
||||
moduleConstraints.set(def.name, { param: found, className: ic.className });
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -414,8 +471,9 @@ function occursIn(name: string, type: TypeAST, subst: Subst): boolean {
|
|||
}
|
||||
|
||||
let freshCounter = 0;
|
||||
function freshen(type: TypeAST, subst: Subst): TypeAST {
|
||||
function freshen(type: TypeAST, subst: Subst): { type: TypeAST, varMap: Map<string, string> } {
|
||||
const vars = new Map<string, TypeAST>();
|
||||
|
||||
function go(t: TypeAST): TypeAST {
|
||||
const resolved = applySubst(t, subst);
|
||||
switch (resolved.kind) {
|
||||
|
|
@ -430,5 +488,11 @@ function freshen(type: TypeAST, subst: Subst): TypeAST {
|
|||
case 'type-record': return { kind: 'type-record', fields: resolved.fields.map(f => ({ name: f.name, type: go(f.type) })) };
|
||||
}
|
||||
}
|
||||
return go(type);
|
||||
|
||||
const result = go(type);
|
||||
const varMap = new Map<string, string>();
|
||||
for (const [old, fresh] of vars) {
|
||||
if (fresh.kind === 'type-var') varMap.set(old, fresh.name);
|
||||
}
|
||||
return { type: result, varMap };
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue