From afd78c3b3e43c92ec4c2d9185e0b18af803e6202 Mon Sep 17 00:00:00 2001
From: Joeri Exelmans <joeri.exelmans@gmail.com>
Date: Sat, 22 Mar 2025 10:33:35 +0100
Subject: [PATCH] progress

---
 generics/generics.js      |  4 +---
 generics/generics.test.js |  1 -
 main.js                   |  2 +-
 progress.txt              | 50 ++++++++++++++++++++++++++++++++++++++-
 typeclasses/num.test.js   |  5 ++--
 5 files changed, 54 insertions(+), 8 deletions(-)

diff --git a/generics/generics.js b/generics/generics.js
index 2318d69..7f73206 100644
--- a/generics/generics.js
+++ b/generics/generics.js
@@ -110,9 +110,7 @@ export const mergeSubstitutions = (m1, m2) => {
     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);
-    }
+    deletedTypeVars = deletedTypeVars.union(d);
   }
   return [new Map([...m1, ...m2]), deletedTypeVars];
 }
diff --git a/generics/generics.test.js b/generics/generics.test.js
index 182e52b..86df9c8 100644
--- a/generics/generics.test.js
+++ b/generics/generics.test.js
@@ -2,7 +2,6 @@ import { Bool, Int } from "../primitives/symbols.js";
 import { lsType } from "../structures/list_common.js";
 import { fnType } from "../metacircular.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}));
diff --git a/main.js b/main.js
index a006b0f..d6a6b73 100644
--- a/main.js
+++ b/main.js
@@ -131,7 +131,7 @@ const makeChoice = ([i, t]) => {
   return {
     value: {i, t: t[0]},
     name: pretty(i),
-    description: `${pretty(i)} :: ${pretty(t[0])}`,
+    description: ` :: ${pretty(t[0])}`,
     short: `${pretty(i)} :: ${pretty(t[0])}`,
   };
 }
diff --git a/progress.txt b/progress.txt
index 60346f5..3fe64bb 100644
--- a/progress.txt
+++ b/progress.txt
@@ -10,8 +10,56 @@ status:
       2) experimental implementation of polymorphic types and type inferencing
          values currently treated as white-box, hardcoded generic types (e.g., list, function) in type inferencing algorithm
 
-todo:
+wip:
   - interfaces via typeclasses?
 
+  - revise the way types are encoded
+     we need only one 'type of type' (called 'kind' in Haskell), and we can call it 'Type'.
+     types explicitly contain their underlying types. the type inferencing algorithm needs this information.
+
+      Int
+       { symbol: Int, params: [] }
+
+      [Int]
+       { symbol: List, params: [{ symbol: Int, params: [] }] }
+
+      [[Int]]
+       { symbol: List,
+         params: [{ symbol: List, params: [{symbol: Int, params: []}]}]}
+
+      Int -> Bool
+       { symbol: Function, params: [
+            { symbol: Int, params: [] },
+            { symbol: Bool, params: [] },
+         ]
+       }
+
+      Int | Bool
+       { symbol: Sum, params: [
+            { symbol: Int, params: [] },
+            { symbol: Bool, params: [] },
+         ]
+       }
+
+      (Int, Bool)
+       { symbol: Product, params: [
+            { symbol: Int, params: [] },
+            { symbol: Bool, params: [] },
+         ]
+       }
+
+      Point2D   <-- custom nominal type! maybe it contains two Doubles, but we don't expose this
+       { symbol: Point2D, params: [] }
+
+      Type constructors are just functions that return a 'Type'.
+         For instance:
+         lsType :: Type -> Type
+         fnType :: Type -> Type -> Type
+
+      The sad(?) part about all of this, is that I'm converging with Haskell/Lean.
+
+  - treat all values as polymorphic? (non-polymorphic values simply have empty set of type variables)
+
+todo:
   - type inferencing can be reduced to finding a graph isomorphism?
 
diff --git a/typeclasses/num.test.js b/typeclasses/num.test.js
index f05b31a..ffbb70c 100644
--- a/typeclasses/num.test.js
+++ b/typeclasses/num.test.js
@@ -16,13 +16,14 @@ const squareFnType = makeGeneric(a =>
     }),
   }));
 
-// should be: Int -> Int
+console.log("should be: Int -> Int");
 console.log(assign(squareFnType, makeGeneric(() => numDictType(Int))));
 
-// should be: Double -> Double
+console.log("should be: Double -> Double");
 console.log(assign(squareFnType, makeGeneric(() => numDictType(Double))));
 
 // to call 'square' we need:
 //   - access to a mapping from types to their typeclass instantiation
 //   - to know that our argument is 'Int'
+console.log("");
 console.log(square(NumInstances.get(Int))(42n)); // 1764n