Joeri Exelmans
8eec5b9239
big part of the code base still needs to be 'ported' to the updated type constructors.
33 lines
No EOL
1.1 KiB
JavaScript
33 lines
No EOL
1.1 KiB
JavaScript
import { Bool, SymbolT, Type } from "./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)),
|
|
]}; |