54 lines
No EOL
1.7 KiB
JavaScript
54 lines
No EOL
1.7 KiB
JavaScript
import { makeGeneric } from "../generics/generics.js";
|
|
import { addDouble, mulDouble } from "../primitives/double.js";
|
|
import { addInt, mulInt } from "../primitives/int.js";
|
|
import { Type } from "../type.js";
|
|
import { typedFnType, typedFnType2 } from "../structures/types.js";
|
|
import { Double, Int } from "../primitives/types.js";
|
|
import { numDictType } from "./num_type.js";
|
|
|
|
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: numDictType(Int)},
|
|
{i: DoubleNumDict, t: numDictType(Double)},
|
|
]};
|
|
|
|
// 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],
|
|
]); |