lotta progress

type.js

@@ -0,0 +1,39 @@
+import { Bool } from "./primitives/types.js";
+import { typedFnType } from "./structures/types.js";
+import { deepEqual } from "./util.js";
+
+// TODO: 'Type' (and its instances) are itself instances of (String,[Type]) (=the product type of String and list of Type)
+//   so is 'Type' just an alias for (String, [Type])
+export const Type = { symbol: Symbol('Type'), params: [] };
+
+export const getSymbol = type => type.symbol;
+export const getParams = type => type.params;
+
+// we can test whether types are equal:
+export const eqType = deepEqual;
+
+// a module is just a set of typed objects
+// each 'typed object' is implicitly an instance of TypeLink (defined below)
+export const ModuleType = {l:[  
+  // TODO? maybe follow Lean so
+  //    Type.{0} : Type.{1}
+  //    Type.{1} : Type.{2}
+  //    ...
+  // see: https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/universes.html
+
+  // Type :: Type
+  {i: Type, t: Type},
+
+  // ...typedFnType(getSymbol, fnType => fnType({in: Type, out: Int})),
+
+  // ...typedFnType(getParams, fnType => fnType({in: Type, out: lsType(Type)})),
+
+  // Type -> Type -> Bool
+  ...typedFnType(eqType, fnType =>
+    fnType
+      (Type)
+      (fnType
+        (Type)
+        (Bool)
+      )),
+]};