🚧[#3] Changes unify to record explaination graph.

- Adds explain path to type variables and changes `unify`, `w` and `m`
to record them.
- Changes error messages towards something actionable and less cryptic

package.json

@@ -37,6 +37,7 @@
     "@trivago/prettier-plugin-sort-imports": "^4.1.1",
     "@types/jest": "^29.5.7",
     "@types/node": "^18",
+    "fast-check": "^3.14.0",
     "jest": "^29.7.0",
     "prettier": "^2.8.8",
     "ts-jest": "^29.1.1",

src/helper.ts

@@ -1,7 +1,17 @@
 // Copyright (c) 2023 Adam Jones
 //
 // SPDX-License-Identifier: MIT
-import {Context, MonoType, PolyType, TypeVariable, isContext, makeContext} from './models';
+import {
+  Context,
+  ExplainPath,
+  Expression,
+  MonoType,
+  PolyType,
+  TypeFunctionApplication,
+  TypeVariable,
+  isContext,
+  makeContext,
+} from './models';
 
 // substitutions
 
@@ -45,8 +55,9 @@ function apply(
   if (value.type === 'ty-quantifier') {
     return {...value, sigma: apply(s, value.sigma)};
   }
-
-  throw new Error('Unknown argument passed to substitution');
+  ((_: never): never => {
+    throw new Error('Unknown argument passed to substitution');
+  })(value);
 }
 
 const combine = (s1: Substitution, s2: Substitution): Substitution => {
@@ -84,7 +95,9 @@ export const instantiate = (
     return instantiate(type.sigma, mappings);
   }
 
-  throw new Error('Unknown type passed to instantiate');
+  ((_: never): never => {
+    throw new Error('Unknown type passed to instantiate');
+  })(type);
 };
 
 // generalise
@@ -119,30 +132,53 @@ const freeVars = (value: PolyType | Context): string[] => {
     return freeVars(value.sigma).filter(v => v !== value.a);
   }
 
-  throw new Error('Unknown argument passed to substitution');
+  ((_: never): never => {
+    throw new Error('Unknown argument passed to substitution');
+  })(value);
 };
 
 // unify
 
-export const unify = (type1: MonoType, type2: MonoType): Substitution => {
+export const unify = (
+  type1: MonoType,
+  type2: MonoType,
+  expr: Expression,
+  path1: ExplainPath = [],
+  path2: ExplainPath = []
+): 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');
-
+    if (contains(type2, type1))
+      throw new Error(`Infinite type detected: ${type1} occurs in ${type2}`);
+
+    if (type2.type === 'ty-var') {
+      // var with other name -> explain
+      // TODO? reverseAliasPath(type1);
+      type1.explain = [type2, {type: 'ExplainAlias', path1, path2, expr}];
+    } else if (type2.type === 'ty-app') {
+      // instantiation
+      // TODO? reverseAliasPath(type1);
+      type1.explain = [type2, {type: 'ExplainInstan', path: path1, expr}];
+    } else {
+      ((_: never): never => {
+        throw new Error('Unknown argument passed to unify');
+      })(type2);
+    }
     return makeSubstitution({
       [type1.a]: type2,
     });
   }
 
   if (type2.type === 'ty-var') {
-    return unify(type2, type1);
+    return unify(type2, type1, expr, path2, path1);
   }
 
   if (type1.C !== type2.C) {
-    throw new Error(`Could not unify types (different type functions): ${type1.C} and ${type2.C}`);
+    const msg = formatUnificationError(type1, type2, expr, path1, path2);
+    throw new Error(msg);
   }
 
   if (type1.mus.length !== type2.mus.length) {
@@ -151,11 +187,55 @@ export const unify = (type1: MonoType, type2: MonoType): Substitution => {
 
   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]), expr, addHist(path1, type1), addHist(path2, type2))
+    );
   }
   return s;
 };
 
+const formatUnificationError = (
+  type1: TypeFunctionApplication,
+  type2: TypeFunctionApplication,
+  expr: Expression,
+  _path1: ExplainPath,
+  _path2: ExplainPath
+): string => {
+  // console.dir({type1, type2, expr, _path1, _path2}, {depth: Infinity});
+  if (expr.type === 'app') {
+    const msg = `"${reprExpression(expr.e1)}" expects "${reprExpression(expr.e2)}" to be a ${
+      type1.C
+    }, but it is a ${type2.C}`;
+    return msg;
+  }
+  throw new Error(`Unexpected expression type ${expr}`);
+};
+
+export const reprExpression = (expr: Expression): string => {
+  if (expr.type === 'app') return reprExpression(expr.e1);
+  if (expr.type === 'var') return expr.x.startsWith('var: ') ? expr.x.substring(5) : expr.x;
+  if (expr.type === 'num') return expr.x.toString();
+  if (expr.type === 'str') return expr.x.toString();
+  if (expr.type === 'abs') return `{"${expr.x}": ${reprExpression(expr.e)}}`;
+  if (expr.type === 'let')
+    return `"${expr.x}" = ${reprExpression(expr.e1)} in ${reprExpression(expr.e2)}`;
+  ((_: never): never => {
+    throw new Error(`Unexpected expression type ${expr}`);
+  })(expr);
+};
+
+const addHist = (history: ExplainPath, root: MonoType): ExplainPath => {
+  const _addHist = (root: MonoType): ExplainPath => {
+    if (root.type === 'ty-app' || !root.explain) return [];
+    const [ty, _explain] = root.explain;
+    const explPath = _addHist(ty);
+    // root.explain = [explPath, _explain]
+    return [root, ...explPath];
+  };
+  // and return the new history
+  return history.concat(_addHist(root));
+};
+
 const contains = (value: MonoType, type2: TypeVariable): boolean => {
   if (value.type === 'ty-var') {
     return value.a === type2.a;
@@ -165,5 +245,7 @@ const contains = (value: MonoType, type2: TypeVariable): boolean => {
     return value.mus.some(t => contains(t, type2));
   }
 
-  throw new Error('Unknown argument passed to substitution');
+  ((_: never): never => {
+    throw new Error('Unknown argument passed to substitution');
+  })(value);
 };

src/m.ts

@@ -10,17 +10,29 @@ export const M = (typEnv: Context, expr: Expression, type: MonoType): Substituti
 
     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), expr);
+  }
+
+  if (expr.type === 'num') {
+    return unify(type, {type: 'ty-app', C: 'Number', mus: []}, expr);
+  }
+
+  if (expr.type === 'str') {
+    return unify(type, {type: 'ty-app', C: 'String', mus: []}, expr);
   }
 
   if (expr.type === 'abs') {
     const beta1 = newTypeVar();
     const beta2 = newTypeVar();
-    const s1 = unify(type, {
-      type: 'ty-app',
-      C: '->',
-      mus: [beta1, beta2],
-    });
+    const s1 = unify(
+      type,
+      {
+        type: 'ty-app',
+        C: '->',
+        mus: [beta1, beta2],
+      },
+      expr
+    );
     const s2 = M(
       makeContext({
         ...s1(typEnv),

src/models.ts

@@ -69,8 +69,15 @@ export type TypeFunction = '->' | 'Array' | 'Boolean' | 'Number' | 'String' | 'N
 export interface TypeVariable {
   type: 'ty-var';
   a: string;
+  explain?: [MonoType, TypeExplanation]; // Optional explanation
 }
 
+export type TypeExplanation =
+  | {type: 'ExplainAlias'; path1: ExplainPath; path2: ExplainPath; expr: Expression}
+  | {type: 'ExplainInstan'; path: ExplainPath; expr: Expression};
+
+export type ExplainPath = TypeVariable[];
+
 export interface TypeFunctionApplication {
   type: 'ty-app';
   C: TypeFunction;

src/parser.ts

@@ -97,16 +97,18 @@ export const defaultContext = makeContext({
   // TODO: overload with sum type encoding
   // "in": f(string, string, bool),
   cat: f(array(string), string),
+  // add a unary cat to cast to string
+  '1-ary cat': forall([a], f(a, string)),
   substr: f(string, number, string),
   '3-ary substr': f(string, number, number, string),
   // Miscellaneous
   log: forall([a], f(a, a)),
 });
 
-type JsonLogicParameter = JsonLogicExpression | boolean | string | number | JsonLogicParameter[];
-type JsonLogicExpression =
-  | {[operation: string]: JsonLogicParameter[]} // normal form e.g. {"var": ["path.in.data"]}
-  | {[operation: string]: JsonLogicParameter}; // unary operation e.g. {"var": "path.in.data"}
+type JsonLogicExpression = JsonLogicOperation | boolean | string | number | JsonLogicExpression[];
+type JsonLogicOperation =
+  | {[operation: string]: JsonLogicExpression[]} // normal form e.g. {"var": ["path.in.data"]}
+  | {[operation: string]: JsonLogicExpression}; // unary operation e.g. {"var": "path.in.data"}
 
 /**
  * @param json - (malformed?) JsonLogic rule
@@ -345,11 +347,15 @@ export const parseJsonLogicExpression = (
       {[varName]: {type: 'ty-var', a: varName}, ...context},
       {type: 'var', x: varName},
     ];
-  } else if (new Set(['<', '<=', 'substr']).has(operation) && args.length === 3) {
+  } else if (['<', '<=', 'substr'].includes(operation) && args.length === 3) {
     operation = `3-ary ${operation}`;
-  } else if (new Set(['-', '+']).has(operation) && args.length === 1) {
+  } else if (['-', '+'].includes(operation) && args.length === 1) {
     operation = `1-ary ${operation}`;
   } else if ((operation === '+' || operation === '*') && args.length != 2) {
+    if (args.length == 0)
+      throw Error(
+        `This ${operation} operation is incomplete ${repr(json)}.\nIt needs some arguments.`
+      );
     // NB unary + should be handled already...
     // monomorphise sum and product versions of + and *
     operation = `${args.length}-ary ${operation}`;
@@ -392,7 +398,7 @@ export const parseJsonLogicExpression = (
         a
       );
     }
-  } else if (new Set(['map', 'filter', 'all', 'some', 'none']).has(operation)) {
+  } else if (['map', 'filter', 'all', 'some', 'none'].includes(operation)) {
     const [newContext, [arrayExp, e2]] = parseValues(args, context);
     return [
       newContext,
@@ -413,7 +419,7 @@ export const parseJsonLogicExpression = (
         initialAccumulator,
       ]),
     ];
-  } else if (new Set(['cat', 'merge', 'missing', 'min', 'max']).has(operation)) {
+  } else if (['cat', 'merge', 'missing', 'min', 'max'].includes(operation)) {
     // pass all params for n-adic functions as a single array
     const [newContext, arrayExp] = parseValue(args, context);
     return [newContext, apply([{type: 'var', x: operation}, arrayExp])];
@@ -490,3 +496,33 @@ export const parseContext = (
     .map(([key, value]) => parseContext(value, context, [...path, key]))
     .reduce((acc, curr) => ({...acc, ...curr}), context);
 };
+
+export const stringify = (expr: Expression): JsonLogicExpression => {
+  switch (expr.type) {
+    case 'num':
+      return expr.x;
+    case 'str':
+      return expr.x;
+    case 'var':
+      const name = expr.x.replace(/^var: /, '');
+      return name === '[]' ? [] : {var: name}; // [] is the cons cell "nil"
+    case 'app':
+      const {e1, e2} = expr;
+      switch (e1.type) {
+        case 'var':
+          const op = e1.x.replace(/^\d+-ary /, '');
+          return {[op]: [stringify(e2)]};
+        case 'app':
+          if (e1.e1.type === 'var' && e1.e1.x == 'cons')
+            return [stringify(e1.e2)].concat(stringify(e2)); // handle cons cell
+          return Object.fromEntries(
+            Object.entries(stringify(e1)).map(([op, arg]) => [op, [...arg, stringify(e2)]])
+          );
+      }
+  }
+  const unexpectedExpression = JSON.stringify(expr);
+  ((_: never): never => {
+    throw unexpectedExpression;
+    // @ts-ignore
+  })(expr);
+};