Skip to content
This repository has been archived by the owner on Jul 3, 2024. It is now read-only.

Commit

Permalink
🚨 Apply prettier
Browse files Browse the repository at this point in the history
  • Loading branch information
@CharString
CharString committed Nov 13, 2023
1 parent a2c1813 commit 7fc98f1
Show file tree
Hide file tree
Showing 2 changed files with 90 additions and 88 deletions.
123 changes: 61 additions & 62 deletions src/helper.ts
View file
Original file line number Diff line number Diff line change
@@ -1,68 +1,67 @@
// Copyright (c) 2023 Adam Jones
//
// SPDX-License-Identifier: MIT

import { Context, isContext, makeContext, MonoType, PolyType, TypeVariable } from "./models";
import {Context, MonoType, PolyType, TypeVariable, isContext, makeContext} from './models';

// substitutions

export type Substitution = {
type: 'substitution',
type: 'substitution';
(m: MonoType): MonoType;
(t: PolyType): PolyType;
(c: Context): Context;
(s: Substitution): Substitution;
raw: { [typeVariables: string]: MonoType }
}
raw: {[typeVariables: string]: MonoType};
};

export const makeSubstitution = (raw: Substitution["raw"]): Substitution => {
export const makeSubstitution = (raw: Substitution['raw']): Substitution => {
const fn = ((arg: MonoType | PolyType | Context | Substitution) => {
if (arg.type === "substitution") return combine(fn, arg)
if (arg.type === 'substitution') return combine(fn, arg);
return apply(fn, arg);
}) as Substitution
}) as Substitution;
fn.type = 'substitution';
fn.raw = raw;
return fn;
}
};

function apply<T extends MonoType | PolyType | Context>(substitution: Substitution, value: T): T;
function apply(s: Substitution, value: MonoType | PolyType | Context): MonoType | PolyType | Context {
function apply(
s: Substitution,
value: MonoType | PolyType | Context
): MonoType | PolyType | Context {
if (isContext(value)) {
return makeContext(Object.fromEntries(
Object.entries(value)
.map(([k, v]) => [k, apply(s, v)])
))
return makeContext(Object.fromEntries(Object.entries(value).map(([k, v]) => [k, apply(s, v)])));
}

if (value.type === "ty-var") {
if (value.type === 'ty-var') {
if (s.raw[value.a]) return s.raw[value.a];
return value;
}

if (value.type === "ty-app") {
return { ...value, mus: value.mus.map((m) => apply(s, m)) };
if (value.type === 'ty-app') {
return {...value, mus: value.mus.map(m => apply(s, m))};
}

if (value.type === "ty-quantifier") {
return { ...value, sigma: apply(s, value.sigma) };
if (value.type === 'ty-quantifier') {
return {...value, sigma: apply(s, value.sigma)};
}

throw new Error('Unknown argument passed to substitution')
throw new Error('Unknown argument passed to substitution');
}

const combine = (s1: Substitution, s2: Substitution): Substitution => {
return makeSubstitution({
...s1.raw,
...Object.fromEntries(Object.entries(s2.raw).map(([k, v]) => [k, s1(v)]))
})
}
...Object.fromEntries(Object.entries(s2.raw).map(([k, v]) => [k, s1(v)])),
});
};

// new type variable
let currentTypeVar = 0;
export const newTypeVar = (): TypeVariable => ({
type: 'ty-var',
a: `t${currentTypeVar++}`
})
a: `t${currentTypeVar++}`,
});

// instantiate
// mappings = { a |-> t0, b |-> t1 }
Expand All @@ -72,99 +71,99 @@ export const instantiate = (
type: PolyType,
mappings: Map<string, TypeVariable> = new Map()
): MonoType => {
if (type.type === "ty-var") {
if (type.type === 'ty-var') {
return mappings.get(type.a) ?? type;
}

if (type.type === "ty-app") {
return { ...type, mus: type.mus.map((m) => instantiate(m, mappings)) };
if (type.type === 'ty-app') {
return {...type, mus: type.mus.map(m => instantiate(m, mappings))};
}

if (type.type === "ty-quantifier") {
if (type.type === 'ty-quantifier') {
mappings.set(type.a, newTypeVar());
return instantiate(type.sigma, mappings);
}

throw new Error('Unknown type passed to instantiate')
}
throw new Error('Unknown type passed to instantiate');
};

// generalise
export const generalise = (ctx: Context, type: MonoType): PolyType => {
const quantifiers = diff(freeVars(type), freeVars(ctx));
let t: PolyType = type;
quantifiers.forEach(q => {
t = { type: 'ty-quantifier', a: q, sigma: t }
})
t = {type: 'ty-quantifier', a: q, sigma: t};
});
return t;
}
};

const diff = <T>(a: T[], b: T[]): T[] => {
const bset = new Set(b);
return a.filter(v => !bset.has(v))
}
return a.filter(v => !bset.has(v));
};

const freeVars = (value: PolyType | Context): string[] => {
if (isContext(value)) {
return Object.values(value).flatMap(freeVars)
return Object.values(value).flatMap(freeVars);
}

if (value.type === "ty-var") {
if (value.type === 'ty-var') {
return [value.a];
}

if (value.type === "ty-app") {
return value.mus.flatMap(freeVars)
if (value.type === 'ty-app') {
return value.mus.flatMap(freeVars);
}

if (value.type === "ty-quantifier") {
return freeVars(value.sigma).filter(v => v !== value.a)
if (value.type === 'ty-quantifier') {
return freeVars(value.sigma).filter(v => v !== value.a);
}

throw new Error('Unknown argument passed to substitution')
}
throw new Error('Unknown argument passed to substitution');
};

// unify

export const unify = (type1: MonoType, type2: MonoType): Substitution => {
if (type1.type === "ty-var" && type2.type === "ty-var" && type1.a === type2.a) {
return makeSubstitution({})
if (type1.type === 'ty-var' && type2.type === 'ty-var' && type1.a === type2.a) {
return makeSubstitution({});
}

if (type1.type === "ty-var") {
if (contains(type2, type1)) throw new Error('Infinite type detected')
if (type1.type === 'ty-var') {
if (contains(type2, type1)) throw new Error('Infinite type detected');

return makeSubstitution({
[type1.a]: type2
})
[type1.a]: type2,
});
}

if (type2.type === "ty-var") {
return unify(type2, type1)
if (type2.type === 'ty-var') {
return unify(type2, type1);
}

if (type1.C !== type2.C) {
throw new Error(`Could not unify types (different type functions): ${type1.C} and ${type2.C}`)
throw new Error(`Could not unify types (different type functions): ${type1.C} and ${type2.C}`);
}

if (type1.mus.length !== type2.mus.length) {
throw new Error(`Could not unify types (different argument lengths): ${type1} and ${type2}`)
throw new Error(`Could not unify types (different argument lengths): ${type1} and ${type2}`);
}

let s: Substitution = makeSubstitution({})
let s: Substitution = makeSubstitution({});
for (let i = 0; i < type1.mus.length; i++) {
s = s(unify(s(type1.mus[i]), s(type2.mus[i])))
s = s(unify(s(type1.mus[i]), s(type2.mus[i])));
}
return s;
}
};

const contains = (value: MonoType, type2: TypeVariable): boolean => {
if (value.type === "ty-var") {
if (value.type === 'ty-var') {
return value.a === type2.a;
}

if (value.type === "ty-app") {
return value.mus.some((t) => contains(t, type2))
if (value.type === 'ty-app') {
return value.mus.some(t => contains(t, type2));
}

throw new Error('Unknown argument passed to substitution')
}
throw new Error('Unknown argument passed to substitution');
};
55 changes: 29 additions & 26 deletions src/m.ts
View file
Original file line number Diff line number Diff line change
@@ -1,58 +1,61 @@
// Copyright (c) 2023 Adam Jones
//
// SPDX-License-Identifier: MIT

import { generalise, instantiate, newTypeVar, Substitution, unify } from "./helper";
import { Context, Expression, makeContext, MonoType } from "./models";
import {Substitution, generalise, instantiate, newTypeVar, unify} from './helper';
import {Context, Expression, MonoType, makeContext} from './models';

export const M = (typEnv: Context, expr: Expression, type: MonoType): Substitution => {
if (expr.type === "var") {
console.log(`Variable ${expr.x}: expected to have type ${JSON.stringify(type)}`)
if (expr.type === 'var') {
console.log(`Variable ${expr.x}: expected to have type ${JSON.stringify(type)}`);

const value = typEnv[expr.x];
if (value === undefined) throw new Error(`Undefined variable: ${expr.x}`);
return unify(type, instantiate(value))
return unify(type, instantiate(value));
}

if (expr.type === "abs") {
if (expr.type === 'abs') {
const beta1 = newTypeVar();
const beta2 = newTypeVar();
const s1 = unify(type, {
type: 'ty-app',
C: '->',
mus: [beta1, beta2]
})
mus: [beta1, beta2],
});
const s2 = M(
makeContext({
...s1(typEnv),
[expr.x]: s1(beta1)
[expr.x]: s1(beta1),
}),
expr.e,
s1(beta2),
s1(beta2)
);
return s2(s1);
}

if (expr.type === "app") {
const beta = newTypeVar()
if (expr.type === 'app') {
const beta = newTypeVar();
const s1 = M(typEnv, expr.e1, {
type: 'ty-app',
C: '->',
mus: [beta, type]
})
const s2 = M(s1(typEnv), expr.e2, s1(beta))
return s2(s1)
mus: [beta, type],
});
const s2 = M(s1(typEnv), expr.e2, s1(beta));
return s2(s1);
}

if (expr.type === "let") {
const beta = newTypeVar()
const s1 = M(typEnv, expr.e1, beta)
const s2 = M(makeContext({
...s1(typEnv),
[expr.x]: generalise(s1(typEnv), s1(beta))
}), expr.e2, s1(type))
if (expr.type === 'let') {
const beta = newTypeVar();
const s1 = M(typEnv, expr.e1, beta);
const s2 = M(
makeContext({
...s1(typEnv),
[expr.x]: generalise(s1(typEnv), s1(beta)),
}),
expr.e2,
s1(type)
);
return s2(s1);
}

throw new Error('Unknown expression type')
}
throw new Error('Unknown expression type');
};

0 comments on commit 7fc98f1

Please sign in to comment.