type inferencing "unifying" operation is now bi-directional + begin writing generic version of "unifying" operation (that should work on all types)

generics/generics.js

@@ -48,6 +48,75 @@ export const occurring = (type, typeVars) => {
   return new Set();
 }
 
+export const properUnify = eqDict => (
+  {typeVars: formalTypeVars, type: formalType},
+  {typeVars: actualTypeVars, type: actualType},
+) => {
+  if (getEq(eqDict)(formalType)(actualType)) {
+    return {
+      substitutions: new Map(),
+      typeVars: new Set([
+        ...actualTypeVars,
+        // ...formalTypeVars, // <- i don't think we need these?
+      ]),
+      type: actualType,
+    }
+  }
+
+  if (formalTypeVars.has(formalType)) {
+    // formalType is type variable -> substitute it by actualType
+    return {
+      substitutions: new Map([[formalType, actualType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars,
+      ].filter(a => a !== formalType)),
+      type: actualType,
+    }
+  }
+  if (actualTypeVars.has(actualType)) {
+    // same as above, but in opposite direction:
+    // actualType is type variable -> substitute it by formalType
+    return {
+      substitutions: new Map([[actualType, formalType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars,
+      ].filter(a => a !== actualType)),
+      type: formalType,
+    }
+  }
+  
+  // WIP...
+}
+
+const mergeOneWay = (m1, m2) => {
+  const m1copy = new Map(m1);
+  const m2copy = new Map(m2);
+  for (const [key1, val1] of m1copy.entries()) {
+    if (m2copy.has(val1)) {
+      m1copy.set(key1, m2.get(val1));
+      m2copy.delete(val1);
+      return [false, m1copy, m2copy, new Set([val1])];
+    }
+  }
+  return [true, m1copy, m2copy, new Set()]; // stable
+}
+
+export const mergeSubstitutions = (m1, m2) => {
+  let stable = false;
+  let deletedTypeVars = new Set();
+  while (!stable) {
+    let d;
+    // notice we swap m2 and m1, so the rewriting can happen both ways:
+    [stable, m2, m1, d] = mergeOneWay(m1, m2);
+    if (!stable) {
+      deletedTypeVars = deletedTypeVars.union(d);
+    }
+  }
+  return [new Map([...m1, ...m2]), deletedTypeVars];
+}
+
 // Currently very ad-hoc.
 
 // Thanks to Hans for pointing out that this algorithm exactly like "Unification" in Prolog (hence the function name):
@@ -77,6 +146,17 @@ export const unify = (
     };
   }
 
+  if (actualTypeVars.has(actualType)) {
+    // same as above, but in the other direction
+    return {
+      substitutions: new Map([[actualType, formalType]]),
+      typeVars: new Set([
+        ...actualTypeVars,
+        ...formalTypeVars].filter(a => a !== actualType)),
+      type: formalType,
+    };
+  }
+
   if (formalType.in !== undefined) {
     // function type
     if (actualType.in === undefined) {
@@ -95,13 +175,15 @@ export const unify = (
         }
       }
       // merge substitutions
-      const newSubstitutions = new Map([
-        ...inType.substitutions,
-        ...outType.substitutions,
-      ]);
+      const [newSubstitutions, deletedTypeVars] = mergeSubstitutions(
+        inType.substitutions, outType.substitutions);
+      // const newSubstitutions = new Map([
+      //   ...inType.substitutions,
+      //   ...outType.substitutions,
+      // ]);
       const newTypeVars = new Set([
         ...actualTypeVars,
-        ...formalTypeVars].filter(a => !newSubstitutions.has(a)));
+        ...formalTypeVars].filter(a => !newSubstitutions.has(a) && !deletedTypeVars.has(a)));
       return {
         substitutions: newSubstitutions,
         typeVars: newTypeVars,

generics/generics.test.js

@@ -1,20 +1,21 @@
 import { Bool, Int } from "../primitives/symbols.js";
 import { lsType } from "../structures/list_common.js";
 import { fnType } from "../metacircular.js";
-import { assign, makeGeneric, unify } from "./generics.js";
+import { assign, makeGeneric, mergeSubstitutions, unify } from "./generics.js";
+import { select } from "@inquirer/prompts";
 
 // a -> Int
 const a_to_Int = makeGeneric(a => fnType({in: a, out: Int}));
 // Bool -> Int
 const Bool_to_Int = makeGeneric(() => fnType({in: lsType(Bool), out: Int}));
-// should be: Bool -> Int
+console.log("should be: Bool -> Int")
 console.log(unify(a_to_Int, Bool_to_Int));
 
 // (a -> a) -> b
 const fnType2 = makeGeneric((a,b) => fnType({in: fnType({in: a, out: a}), out: b}));
 // (Bool -> Bool) -> a
 const fnType3 = makeGeneric(a => fnType({in: fnType({in: Bool, out: Bool}), out: a}));
-// should be: (Bool -> Bool) -> a
+console.log("should be: (Bool -> Bool) -> a");
 console.log(unify(fnType2, fnType3));
 
 // (a -> b) -> [a] -> [b]
@@ -26,5 +27,14 @@ const mapFnType = makeGeneric((a,b) =>
 // a -> a
 const idFnType = makeGeneric(a =>
   fnType({in: a, out: a}));
-// should be: [a] -> [a]
+console.log("should be: [a] -> [a]");
 console.log(assign(mapFnType, idFnType));
+
+// (a -> Int) -> [a] -> a
+const weirdFnType = makeGeneric(a =>
+  fnType({
+    in: fnType({in: a, out: Int}),
+    out: fnType({in: lsType(a), out: a}),
+  }));
+console.log("should be: [Int] -> Int");
+console.log(assign(weirdFnType, idFnType));