✨[#1] Vendor hindley-milner-typescript-minimal

Vendor the meat of https://github.com/domdomegg/hindley-milner-typescript-minimal
Implementations for

- Algorithm W
  L. Damas and R. Milner, "Principal type-schemes for functional programs", Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '82, 1982. https://doi.org/10.1145/582153.582176
- Algorithm M
  O. Lee and K. Yi, "Proofs about a folklore let-polymorphic type inference algorithm", ACM Transactions on Programming Languages and Systems, vol. 20, no. 4, p. 707-723, 1998. https://doi.org/10.1145/291891.291892

Vendoring, because we will need to tailor the models to the JsonLogic language.

Code in this commit is an exact copy; just reformated with prettier.

README.md

@@ -28,3 +28,21 @@ Install with npm or yarn:
 npm install --save-dev @open-formulieren/infernologic
 yarn add -D @open-formulieren/infernologic
 ```
+
+## References
+
+Builds on implementations from
+[domdomegg/hindley-milner-typescript-minimal](https://github.com/domdomegg/hindley-milner-typescript-minimal)
+for
+
+- Algorithm W
+
+  Damas, L. and Milner, R. (1982). Principal type-schemes for functional programs. Proceedings of
+  the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '82.
+  https://doi.org/10.1145/582153.582176
+
+- Algorithm M
+
+  Lee, O. and Yi, K. (1998). Proofs about a folklore let-polymorphic type inference algorithm. ACM
+  Transactions on Programming Languages and Systems, 20(4), 707-723.
+  https://doi.org/10.1145/291891.291892

src/helper.ts

@@ -0,0 +1,170 @@
+// Copyright (c) 2023 Adam Jones
+//
+// SPDX-License-Identifier: MIT
+
+import { Context, isContext, makeContext, MonoType, PolyType, TypeVariable } from "./models";
+
+// substitutions
+
+export type Substitution = {
+  type: 'substitution',
+  (m: MonoType): MonoType;
+  (t: PolyType): PolyType;
+  (c: Context): Context;
+  (s: Substitution): Substitution;
+  raw: { [typeVariables: string]: MonoType }
+}
+
+export const makeSubstitution = (raw: Substitution["raw"]): Substitution => {
+  const fn = ((arg: MonoType | PolyType | Context | Substitution) => {
+    if (arg.type === "substitution") return combine(fn, arg)
+    return apply(fn, arg);
+  }) 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 {
+  if (isContext(value)) {
+    return makeContext(Object.fromEntries(
+      Object.entries(value)
+      .map(([k, v]) => [k, apply(s, v)])
+    ))
+  }
+
+  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-quantifier") {
+    return { ...value, sigma: apply(s, value.sigma) };
+  }
+
+  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)]))
+  })
+}
+
+// new type variable
+let currentTypeVar = 0;
+export const newTypeVar = (): TypeVariable => ({
+  type: 'ty-var',
+  a: `t${currentTypeVar++}`
+})
+
+// instantiate
+// mappings = { a |-> t0, b |-> t1 }
+// Va. Vb. a -> b
+// t0 -> t1
+export const instantiate = (
+  type: PolyType,
+  mappings: Map<string, TypeVariable> = new Map()
+): MonoType => {
+  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-quantifier") {
+    mappings.set(type.a, newTypeVar());
+    return instantiate(type.sigma, mappings);
+  }
+
+  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 }
+  })
+  return t;
+}
+
+const diff = <T>(a: T[], b: T[]): T[] => {
+  const bset = new Set(b);
+  return a.filter(v => !bset.has(v))
+}
+
+const freeVars = (value: PolyType | Context): string[] => {
+  if (isContext(value)) {
+    return Object.values(value).flatMap(freeVars)
+  }
+
+  if (value.type === "ty-var") {
+    return [value.a];
+  }
+
+  if (value.type === "ty-app") {
+    return value.mus.flatMap(freeVars)
+  }
+
+  if (value.type === "ty-quantifier") {
+    return freeVars(value.sigma).filter(v => v !== value.a)
+  }
+
+  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") {
+    if (contains(type2, type1)) throw new Error('Infinite type detected')
+
+    return makeSubstitution({
+      [type1.a]: type2
+    })
+  }
+
+  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}`)
+  }
+
+  if (type1.mus.length !== type2.mus.length) {
+    throw new Error(`Could not unify types (different argument lengths): ${type1} and ${type2}`)
+  }
+
+  let s: Substitution = makeSubstitution({})
+  for (let i = 0; i < type1.mus.length; 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") {
+    return value.a === type2.a;
+  }
+
+  if (value.type === "ty-app") {
+    return value.mus.some((t) => contains(t, type2))
+  }
+
+  throw new Error('Unknown argument passed to substitution')
+}

src/m.ts

@@ -0,0 +1,58 @@
+// Copyright (c) 2023 Adam Jones
+//
+// SPDX-License-Identifier: MIT
+
+import { generalise, instantiate, newTypeVar, Substitution, unify } from "./helper";
+import { Context, Expression, makeContext, MonoType } 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)}`)
+
+    const value = typEnv[expr.x];
+    if (value === undefined) throw new Error(`Undefined variable: ${expr.x}`);
+    return unify(type, instantiate(value))
+  }
+
+  if (expr.type === "abs") {
+    const beta1 = newTypeVar();
+    const beta2 = newTypeVar();
+    const s1 = unify(type, {
+      type: 'ty-app',
+      C: '->',
+      mus: [beta1, beta2]
+    })
+    const s2 = M(
+      makeContext({
+        ...s1(typEnv),
+        [expr.x]: s1(beta1)
+      }),
+      expr.e,
+      s1(beta2),
+    );
+    return s2(s1);
+  }
+
+  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)
+  }
+
+  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')
+}

src/models.ts

@@ -0,0 +1,88 @@
+// Copyright (c) 2023 Adam Jones
+//
+// SPDX-License-Identifier: MIT
+
+// Expressions
+
+// e ::= x
+//     | e1 e2
+//     | \x -> e
+//     | let x = e1 in e2
+
+export type Expression =
+  | VariableExpression
+  | ApplicationExpression
+  | AbstractionExpression
+  | LetExpression;
+
+export interface VariableExpression {
+  type: 'var';
+  x: string;
+}
+
+export interface ApplicationExpression {
+  type: 'app';
+  e1: Expression;
+  e2: Expression;
+}
+
+export interface AbstractionExpression {
+  type: 'abs';
+  x: string;
+  e: Expression;
+}
+
+export interface LetExpression {
+  type: 'let';
+  x: string;
+  e1: Expression;
+  e2: Expression;
+}
+
+// Types
+
+// mu ::= a
+//      | C mu_0 ... mu_n
+
+// sigma ::= mu
+//         | Va. sigma
+
+export type MonoType = TypeVariable | TypeFunctionApplication;
+
+export type PolyType = MonoType | TypeQuantifier;
+
+export type TypeFunction = '->' | 'Bool' | 'Int' | 'List';
+
+export interface TypeVariable {
+  type: 'ty-var';
+  a: string;
+}
+
+export interface TypeFunctionApplication {
+  type: 'ty-app';
+  C: TypeFunction;
+  mus: MonoType[];
+}
+
+export interface TypeQuantifier {
+  type: 'ty-quantifier';
+  a: string;
+  sigma: PolyType;
+}
+
+// Contexts
+
+export const ContextMarker = Symbol();
+export type Context = {[ContextMarker]: boolean; [variable: string]: PolyType};
+
+export const makeContext = (raw: {
+  [ContextMarker]?: boolean;
+  [variable: string]: PolyType;
+}): Context => {
+  raw[ContextMarker] = true;
+  return raw as Context;
+};
+
+export const isContext = (something: unknown): something is Context => {
+  return typeof something === 'object' && something !== null && ContextMarker in something;
+};