import { makeGeneric } from "../generics/generics"; import { addDouble, mulDouble } from "../primitives/double"; import { addInt, mulInt } from "../primitives/int"; import { typedFnType, typedFnType2 } from "../metacircular"; const numDictTypeRegistry = new DefaultMap(a => ({numDict: a})); export const numDictType = a => numDictTypeRegistry.getdefault(a, true); export const getAdd = numDict => numDict.add; export const getMul = numDict => numDict.mul; // getAdd and getMul have same (generic) type: const [getAddMulFnType, typesOfFns] = typedFnType2(fnType => makeGeneric(a => fnType({ in: numDictType(a), out: fnType({ in: a, out: fnType({in: a, out: a}), }), }))); export const ModuleNum = {l:[ ...typedFnType(numDictType, fnType => fnType({in: Type, out: Type})), {i: getAdd, t: getAddMulFnType}, {i: getMul, t: getAddMulFnType}, ...typesOfFns, ]}; const IntNumDict = { add: addInt, mul: mulInt, }; const DoubleNumDict = { add: addDouble, mul: mulDouble, } export const ModuleNumInstances = {l:[ {i: IntNumDict , t: NumDict}, {i: DoubleNumDict, t: NumDict}, ]}; // mapping from type to type class implementation // in Haskell, such a mapping is global (for the entire application being compiled), and every type can implement every type class at most once. // in Lean, such mappings can be local, and there can be multiple implementations per (type, type class). // We have to follow Lean's approach, because in DOPE, there is no such thing as a "global scope". Every dependency is explicit, and type class resolution is just a function that always depends on a specific mapping: export const NumInstances = new Map([ [Int , IntNumDict ], [Double, DoubleNumDict], ]);