35 lines
1,009 B
JavaScript
35 lines
1,009 B
JavaScript
import { Bool, Type } from "./primitives/types.js";
|
|
import { typedFnType } from "./structures/types.js";
|
|
import { deepEqual } from "./util.js";
|
|
|
|
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)
|
|
)),
|
|
]};
|