basic functionality, no generics
This commit is contained in:
commit
a8260f2afb
17 changed files with 615 additions and 0 deletions
31
metacircular.js
Normal file
31
metacircular.js
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
import { getFnType } from "./function_registry.js";
|
||||
|
||||
export const Type = Symbol('Type');
|
||||
export const Function = Symbol('Function');
|
||||
|
||||
// Implementation of 'in' and 'out' functions,
|
||||
// to get input/output type of a function signature:
|
||||
export const getIn = fn => fn.in;
|
||||
export const getOut = fn => fn.out;
|
||||
|
||||
// a module is just a set of typed objects
|
||||
// each 'typed object' is implicitly an instance of TypeLink (defined below)
|
||||
export const ModuleMetaCircular = [
|
||||
// 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},
|
||||
|
||||
// Function : Type
|
||||
{i: Function, t: Type},
|
||||
|
||||
// (Function -> Type) : Function
|
||||
{i: getFnType(Function, Type), t: Function},
|
||||
|
||||
{i: getIn , t: getFnType(Function, Type)},
|
||||
{i: getOut, t: getFnType(Function, Type)},
|
||||
];
|
||||
Loading…
Add table
Add a link
Reference in a new issue