33 lines
1 KiB
JavaScript
33 lines
1 KiB
JavaScript
import { Bool, SymbolT, Type } from "./primitives/types.js";
|
|
import { isFunction, lsType, typedFnType } from "./structures/types.js";
|
|
import { getSymbol, getParams } from "./type_constructor.js";
|
|
import { deepEqual } from "./util/util.js";
|
|
|
|
// we can test whether types are equal:
|
|
export const eqType = t1 => t2 => deepEqual(t1, t2);
|
|
|
|
// 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
|
|
|
|
{i: Type, t: Type},
|
|
|
|
// Type -> Type -> Bool
|
|
...typedFnType(eqType, fnType =>
|
|
fnType
|
|
(Type)
|
|
(fnType
|
|
(Type)
|
|
(Bool)
|
|
)),
|
|
|
|
...typedFnType(getSymbol, fnType => fnType(Type)(SymbolT)),
|
|
...typedFnType(getParams, fnType => fnType(Type)(lsType(Type))),
|
|
|
|
...typedFnType(isFunction, fnType => fnType(Type)(Bool)),
|
|
]};
|