interactive prompt can handle polymorphic types

This commit is contained in:
Joeri Exelmans 2025-04-02 15:49:43 +02:00
parent a0e3aa0cb3
commit 4a4983f693
20 changed files with 485 additions and 276 deletions

View file

@ -0,0 +1,21 @@
import { constructorLeft, constructorRight } from "../structures/sum.js";
import { fnType, setType, sumType, typedFnType } from "../structures/types.js";
import { GenericType, SymbolT, Type, Unit } from "./types.js";
import { unit } from "./unit.js";
export const getType = genericType => genericType.type;
export const getTypeVars = genericType => genericType.typeVars;
export const toNonGeneric = genericType => (genericType.typeVars.size === 0)
? constructorRight(genericType.type)
: constructorLeft(unit);
export const ModuleGenericType = {l:[
{i: GenericType, t: Type},
...typedFnType(getType, fnType => fnType(GenericType)(Type)),
...typedFnType(getTypeVars, fnType => fnType(GenericType)(setType(SymbolT))),
...typedFnType(toNonGeneric, fnType => fnType(GenericType)(sumType(Unit)(Type))),
]};

33
primitives/type.js Normal file
View file

@ -0,0 +1,33 @@
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)),
]};

View file

@ -10,6 +10,7 @@ const SymbolChar = Symbol('Char');
const SymbolUnit = Symbol('Unit');
const SymbolSymbol = Symbol('Symbol');
const SymbolType = Symbol('Type');
const SymbolGenericType = Symbol('GenericType');
export const Int = makeTypeConstructor(SymbolInt)(0);
export const Bool = makeTypeConstructor(SymbolBool)(0);
@ -24,6 +25,8 @@ export const SymbolT = makeTypeConstructor(SymbolSymbol)(0);
export const Type = makeTypeConstructor(SymbolType)(0);
export const GenericType = makeTypeConstructor(SymbolGenericType)(0);
export const ModuleSymbols = {l:[
{i: SymbolInt , t: SymbolT},
@ -34,4 +37,5 @@ export const ModuleSymbols = {l:[
{i: SymbolUnit , t: SymbolT},
{i: SymbolSymbol, t: SymbolT},
{i: SymbolType , t: SymbolT},
]};
{i: SymbolGenericType, t: SymbolT},
]};

View file

@ -1,10 +1,12 @@
import { typedFnType } from "../structures/types.js";
import { Bool, Type, Unit } from "./types.js";
const eqUnit = x => y => x === y;
export const eqUnit = x => y => x === y;
export const unit = {};
export const ModuleUnit = {l:[
{i: {}, t: Unit},
{i: unit, t: Unit},
{i: Unit, t: Type},