dope2/generics/generics.js

import { lsType } from "../structures/list_common.js";
import { fnType } from "../metacircular.js";
import { deepEqual, DefaultMap, pretty } from "../util.js";
import { numDictType } from "../typeclasses/num_type.js";

const genericTypeRegistry = new DefaultMap(underlyingType => ({ generic: underlyingType }));

// type constructor for generic kinds,
//   for instance:
//     a -> a -> Bool
//   is typed by
//     genericType(Function)
export const genericType = underlyingType => genericTypeRegistry.getdefault(underlyingType, true);

// constructor for generic types
//   for instance, the type:
//     a -> a -> Bool
//   is created by
//     makeGeneric(a => fnType({in: a, out: fnType({in: a, out: Bool})}))
export const makeGeneric = callback => {
  // type variables to make available:
  const a = Symbol('a');
  const b = Symbol('b');
  const c = Symbol('c');
  const d = Symbol('d');
  const e = Symbol('e');
  const type = callback(a, b, c, d, e);
  return {
    typeVars: occurring(type, new Set([a, b, c, d, e])),
    type,
  };
};

// From the given set of type variables, return only those that occur in the given type.
export const occurring = (type, typeVars) => {
  if (typeVars.has(type)) {
    return new Set([type]);
  }
  if (type.in !== undefined) {
    // function type
    return new Set([
      ...occurring(type.in, typeVars),
      ...occurring(type.out, typeVars)]);
  }
  if (type.listOf !== undefined) {
    return occurring(type.listOf, typeVars);
  }
  return new Set();
}

// Currently very ad-hoc.

// Thanks to Hans for pointing out that this algorithm exactly like "Unification" in Prolog (hence the function name):
//  https://www.dai.ed.ac.uk/groups/ssp/bookpages/quickprolog/node12.html
export const unify = (
  {typeVars: formalTypeVars, type: formalType},
  {typeVars: actualTypeVars, type: actualType},
) => {
  if (deepEqual(formalType, actualType)) {
    return {
      substitutions: new Map(),
      typeVars: new Set([
        ...actualTypeVars,
        ...formalTypeVars]),
      type: actualType,
    }
  }

  if (formalTypeVars.has(formalType)) {
    // simplest case: substitute formal type param
    return {
      substitutions: new Map([[formalType, actualType]]),
      typeVars: new Set([
        ...actualTypeVars,
        ...formalTypeVars].filter(a => a !== formalType)),
      type: actualType,
    };
  }

  if (formalType.in !== undefined) {
    // function type
    if (actualType.in === undefined) {
      throw new Error(`cannot assign ${pretty(actualType)} to ${pretty(formalType)}`);
    }
    else {
      // both are function type
      const inType = unify({typeVars: formalTypeVars, type: formalType.in}, {typeVars: actualTypeVars, type: actualType.in});
      const outType = unify({typeVars: formalTypeVars, type: formalType.out}, {typeVars: actualTypeVars, type: actualType.out});
      // check for conflicts between 'in' and 'out' subsitutions
      for (const [typeVar, actual] of inType.substitutions) {
        if (outType.substitutions.has(typeVar)) {
          if (!deepEqual(actual, outType.substitutions.get(typeVar))) {
            throw new Error(`conflicting assignment for ${pretty(typeVar)}: ${pretty(a)}`);
          }
        }
      }
      // merge substitutions
      const newSubstitutions = new Map([
        ...inType.substitutions,
        ...outType.substitutions,
      ]);
      const newTypeVars = new Set([
        ...actualTypeVars,
        ...formalTypeVars].filter(a => !newSubstitutions.has(a)));
      return {
        substitutions: newSubstitutions,
        typeVars: newTypeVars,
        type: fnType({in: inType.type, out: outType.type}),
      };
    }
  }

  if (formalType.listOf !== undefined) {
    // list type
    if (actualType.listOf === undefined) {
      throw new Error(`cannot assign ${pretty(actualType)} to ${pretty(formalType)}`);
    }
    else {
      // both are list type
      const elementType = unify(
        {typeVars: formalTypeVars, type: formalType.listOf},
        {typeVars: actualTypeVars, type: actualType.listOf});
      return {
        substitutions: elementType.substitutions,
        typeVars: new Set([
          ...actualTypeVars,
          ...formalTypeVars].filter(a => !elementType.substitutions.has(a))),
        type: lsType(elementType.type),
      };
    }
  }

  if (formalType.numDict !== undefined) {
    if (actualType.numDict === undefined) {
      throw new Error(`cannot assign ${pretty(actualType)} to ${pretty(formalType)}`);
    }
    else {
      // both are NumDict type
      const underlyingType = unify(
        {typeVars: formalTypeVars, type: formalType.numDict},
        {typeVars: actualTypeVars, type: actualType.numDict});
      return {
        substitutions: underlyingType.substitutions,
        typeVars: new Set([
          ...actualTypeVars,
          ...formalTypeVars].filter(a => !underlyingType.substitutions.has(a))),
        type: numDictType(underlyingType.type),
      };
    }
  }
  throw new Error("i don't know what to do :(");
};

// export const matchConcrete = ({typeVars, type: formalType}, actualType) => {
//   return unify({typeVars, type: formalType}, {typeVars: new Set(), type: actualType});
// };

export const substitute = (type, substitutions) => {
  if (substitutions.has(type)) {
    return substitutions.get(type);
  }
  if (type.listOf !== undefined) {
    // list type
    return lsType(substitute(type.listOf, substitutions));
  }
  if (type.in !== undefined) {
    // function type
    return fnType({
      in: substitute(type.in, substitutions),
      out: substitute(type.out, substitutions),
    })
  }
  return type;
}

export const assign = (genFnType, paramType) => {
  const matchedInType = unify({
    typeVars: genFnType.typeVars,
    type: genFnType.type.in,
  }, paramType);
  const substitutedOutType = substitute(genFnType.type.out, matchedInType.substitutions);
  return {
    typeVars: matchedInType.typeVars,
    type: substitutedOutType,
  };
};