simply-typed.ts

/**
 * Copyright (c) Will Temple 2022
 *
 * # ELEMENTAL TYPE SYSTEM
 *
 * This module describes an elemental type system composed of only five
 * fundamental type forms that I find to be highly expressive in simply-typed
 * contexts.
 *
 * By simply-typed, I mean systems that do not include type-binding.
 *
 * "Non-simple" systems/features are:
 *   - parametric polymorphism
 *   - dependent typing
 *   - binding type construction (generics)
 *
 * This also isn't an attempt to implement higher-kinded types or anything of
 * that nature. It's just a simple type system with very elementary rules.
 *
 * The comments in this file essentially form a small book describing the
 * behavior of this Elemental Type System.
 *
 * ## Type Forms
 *
 * The Elemental Type System describe five simple forms:
 *   - Symbolic: types that have symbolic identity and a set of constraints that
 *               the symbolic type _satisfies_.
 *   - Associative: types that encapsulate directed arrows (morphisms) between
 *                  types
 *   - Intersection: a product type that combines several types using an
 *                   algebraic AND
 *   - Union: a sum type that combines several types using an algebraic OR
 *   - Complement: the difference between the top type and an inner type
 *
 * Additionally, the implementation provides for a special "exotic" form that
 * can specify a separate constraint and effective type as well as a custom
 * implementation of associative activation and complement resolution. For
 * example, a type that behaves like `any` in JavaScript can use `unknown` as a
 * constraint and `never` as an effective type, producing itself when activated.
 *
 * Special forms are not needed for top or bottom types or any other constructs.
 * They are expressed in terms of the above five primary forms, and I strongly
 * believe that _only_ these five forms are truly essential.
 *
 * ## Simple Type Behavior
 *
 * The core predicate of the type system is 'satisfies`. A type U _satisfies_
 * the constraint V if a value of type U may be substituted where a value of
 * type V is expected.
 *
 * Herein, the expression "U satisfies V" will be denoted as "sat(U, V)".
 *
 * U is a strict subtype of V if sat(U, V), but NOT sat(V, U).
 *
 * My implementation of 'satisfies' for the above five forms is simple enough to
 * be expressed in only a few hundred lines of code.
 *
 * ## Structural and Nominal
 *
 * Type systems can usually be described as being either primarily _structural_
 * or _nominal_. In reality this distinction is a bit facile. Many type systems
 * have both structural and nominal aspects, and this type system is one of
 * those.
 *
 * The primary nominal element is the symbolic type form. Symbolic types have
 * _identity_ and _constraints_. A symbolic type `S = Symbolic(Id, [C1, C2, ...
 * CN])` is defined such that `sat(S, Intersection(C1, C2, ... CN))`. Logically,
 * a symbolic type is therefore _defined_ to be a strict subtype of the
 * intersection of its constraints. Symbolic types therefore should not be
 * confused with type _aliases_. They are not _equivalent_ to their constraints,
 * but bounded by them.
 *
 * The primary structural element is the associative form. The essence of an
 * associative type is a _morphism_ (directed arrow) between two types. The
 * implementation actually allows for an associative type to contain a list of
 * morphisms, and it acts as an intersection between each individual morphism,
 * which is the fundamental element. Directed arrows can be used to model the
 * type characteristics of structs, arrays, and functions.
 *
 * You may therefore view an associative type or intersection of associative
 * types as a category over the class of types, where the associative arrows are
 * in the category's set of morphisms.
 */
"__module";

const debug = !!process.env.DEBUG;

/**
 * A type in the Elemental Type System.
 */
export type Type =
  | SymbolicType
  | AssociativeType
  | IntersectionType
  | ComplementType
  | UnionType
  | ExoticType;

/**
 * Constructors and aliases for types in the Elemental Type System.
 */
export const Type = (function bindTypeConstructors() {
  /**
   * Fundamental constructors for the five type forms:
   *
   * union, intersection, symbolic, associative, and complement
   */
  const base = {
    /**
     * Constructs a union type from variants.
     *
     * @param variants - the possible variants of the union
     * @returns a fundamental union type
     */
    union<Variants extends Type[]>(...variants: Variants): UnionType<Variants> {
      return { kind: "union", variants };
    },

    /**
     * Constructs an intersection type from constituents.
     *
     * @param constituents - the constituent constraints of the intersection
     * @returns a fundamental intersection type
     */
    intersection<Constituents extends Type[]>(
      ...constituents: Constituents
    ): IntersectionType<Constituents> {
      return { kind: "intersection", constituents };
    },

    /**
     * Constructs a symbolic type from parts.
     *
     * @param id - the type identity
     * @param constraints - (optional) type constraints that apply to this symbol, default empty
     * @returns a fundamental symbolic type
     */
    symbolic<T>(id: T, constraints: Iterable<Type> = []): SymbolicType<T> {
      return { kind: "symbolic", id: id, constraints: new Set(constraints) };
    },

    /**
     * Constructs a complement type from an inner type.
     * @param t - the inner type of the complement
     * @returns a fundamental complement type
     */
    complement<T extends Type>(t: T): ComplementType<T> {
      return { kind: "complement", inner: t };
    },

    /**
     * Constructs an associative type from a list of morphisms
     * @param morphisms - the morphisms (associative arrows, or (input, output) pairs) in the associative type
     * @returns a fundamental associative type
     */
    associative<Map extends [Type, Type][]>(
      ...morphisms: Map
    ): AssociativeType<Map> {
      return { kind: "associative", morphisms };
    },
  };

  const never = base.union();
  const unknown = base.intersection();

  /**
   * Aliases for common types in JavaScript.
   */
  const aliases = {
    /**
     * The bottom type.
     */
    never,

    /**
     * The top type.
     */
    unknown,

    /**
     * A type that includes all string values.
     */
    string: base.symbolic(Symbol("string"), []),

    /**
     * A type that includes all number values.
     */
    number: base.symbolic(Symbol("number"), []),

    /**
     * A type that includes all symbol values.
     *
     * Not to be confused with a symbolic type in general.
     */
    symbol: base.symbolic(Symbol("symbol"), []),

    /**
     * A type that includes all bigint literals.
     */
    bigint: base.symbolic(Symbol("bigint"), []),

    /**
     * A type that includes the two boolean true/false values.
     */
    boolean: base.symbolic(Symbol("boolean"), []),

    /**
     * A unit type that uses `undefined` as its type ID.
     */
    unit: base.symbolic(undefined, []),

    /**
     * An exotic type that behaves as a bottom type in source position and as a top type in constraint position.
     *
     * Therefore it is assignable _to_ any other type and accepts any type as a constraint (assignable _from_ any other type);
     */
    any: (function createAny() {
      return Object.freeze({
        kind: "exotic",
        name: "any",
        suppressExoticInPrint: true,
        effectiveType: never,
        effectiveConstraint: unknown,
        activate(): ExoticType {
          return aliases.any;
        },
        complement(): ExoticType {
          return aliases.any;
        },
      }) as ExoticType;
    })(),
  };

  const symbolics = {
    /**
     * Creates a new primitive (symbolic peak type) with no parent relationships.
     *
     * If the same name is passed twice, a _DIFFERENT_ primitive will be created with the same name. The two primitives
     * will have unique type identities.
     *
     * @param name - the string name of the type
     * @returns a symbolic type with a unique type ID
     */
    primitive: (name: string): SymbolicType<symbol> =>
      base.symbolic(Symbol(name), []),

    /**
     * Creates a symbolic type with a specified type ID.
     *
     * If the same value is passed twice, an _EQUIVALENT_ literal will be created with the same type ID (they will have
     * different JavaScript object identities, i.e. !==, but will compare equivalent in the type system).
     *
     * The constraints of the constructed literal type is determined by the type of the id value:
     * - "string": [Type.string]
     * - "number": [Type.number]
     * - "symbol": [Type.symbol]
     * - "bigint": [Type.bigint]
     * - "boolean": [Type.boolean]
     * - "undefined": [Type.undefined]
     *
     * - "object": []
     * - "function": []
     *
     * @param id - the exact value of the type ID
     * @returns a symbolic type with the given type id and appropriate parent constraint for the built-in primitive aliases
     */
    literal: <V>(id: V): SymbolicType<V> =>
      base.symbolic(
        id,
        typeof id in aliases ? [aliases[typeof id as keyof typeof aliases]] : []
      ),
  };

  /**
   * Helpful constructors. These create synthetic types from basic/symbolic types.
   */
  const constructors = {
    /**
     * Constructs a type that associates `number` to T. This behaves like an Array<T> in languages where array access
     * by numeric index is infallible.
     *
     * i.e. { [number] -> T }
     *
     * @param t - T
     * @returns number -> T
     */
    array: (t: Type) => base.associative([aliases.number, t]),

    /**
     * Constructs a type that associates specific, contiguous numeric literal types to individual output types, like a
     * tuple.
     *
     * @param values - the ordered list of values to include in the tuple
     * @returns an associative type mapping indices to specific values
     */
    tuple: (...values: Type[]) =>
      base.associative(
        ...values.map((t, idx) => [symbolics.literal(idx), t] as [Type, Type])
      ),

    /**
     * Constructs a type that associates string literal types (names) to specific output types, like a database record
     * or TypeScript interface.
     *
     * @param fields
     * @returns
     */
    record: <Fields extends { [k: string]: Type }>(
      fields: Fields
    ): AssociativeType =>
      base.associative(
        ...Object.entries(fields).map(([name, t]): [Type, Type] => [
          symbolics.literal(name),
          t,
        ])
      ),

    /**
     * Constructs a type that associates a specific ordered tuple of types to a given result type. This mimicks the
     * behavior of functions in many languages.
     *
     * I.e. { [tuple(...parameters)] -> result }
     *
     * @see constructors#tuple
     *
     * @param parameters - the ordered list of parameters to form the input tuple
     * @param result - the output tupe of this associative
     * @returns an associative type that relates tuple(parameters) to result, like a function
     */
    function: (parameters: Type[], result: Type) =>
      base.associative([constructors.tuple(...parameters), result]),

    /**
     * Constructs a type that represents the difference between one type and another. I.e. the subtype of `minuend` that
     * is _not_ assignable to `subtrahend`.
     *
     * I.e. A & ~B
     *
     * This is similar to the `Exclude` type constructor in TypeScript, which says:
     *
     * * Exclude<UnionType, ExcludedMembers>: Constructs a type by exlcuding from UnionType all union members that are
     *   assignable to ExcludedMembers.
     *
     * This constructor is more fundamental and uses the complement type.
     *
     * An example of a difference type would be `Type.difference(Type.string, Type.literal("foo"))`, i.e. the type of
     * strings that are not exactly "foo". Such a construct is unexpressable in TypeScript, but here it is
     * straightforward.
     *
     * @param minuend - the type to exclude
     */
    difference: (minuend: Type, subtrahend: Type) =>
      base.intersection(minuend, base.complement(subtrahend)),

    /**
     * Constructs a unique, opaque type symbol.
     *
     * This is a convenience function and is type theoretically equivalent to calling `Type.primitive`.
     *
     * @param name
     * @returns
     */
    opaque: (name?: string) => base.symbolic(Symbol(name ?? "<opaque>"), []),
  };

  return {
    ...base,
    ...aliases,
    ...symbolics,
    ...constructors,
  };
})();

/**
 * ## Symbolic Type
 *
 * An opaque type symbol carrying a type _identity_ and a set of constraints, where the type is implied to satisfy its
 * constraints.
 *
 * ### As a type
 *
 * This type is assignable to a destination constraint if:
 *  - the constraint is a symbolic type, and this type is assignable to its constraint
 *  - the _effective type_ of this symbol is assignable to the constraint
 *
 * #### Effective Type
 *
 * The effective type of a symbolic type is the intersection of all of the _effective types_ of its constraints, WHERE
 * - the effective type of a non-symbolic type is the type itself.
 *
 * ### As a constraint
 *
 * A type is assignable to this type's constraint if and only if the source is a symbolic type and:
 *   - the source is the same symbolic type (same type identity)
 *   - OR the _effective type_ of the source is assignable to this constraint.
 *
 * ### Notes
 *
 * A symbolic type is an opaque subtype of the intersection of its constraints. In other words it is assignable to the
 * intersection of its constraints, but not necessarily vice versa. A peak type symbol (no constraints) is an opaque
 * subtype of the top type, so this squares with the logic expressed in the IntersectionType notes that an empty
 * intersection is a top type.
 *
 * This type system calculus does not distinguish between opaque type symbols that may have multiple values (scalar) and
 * those that are guaranteed to only have a single value (unit/singleton). They are both simply opaque type symbols.
 */
export interface SymbolicType<Identity = unknown> {
  kind: "symbolic";

  /**
   * The identity of this type. If this value is equal (===) to another symbol's identity, they are assumed to be the
   * same type.
   */
  id: Identity;

  /**
   * The set of types whose constraints this type symbol is assumed to satisfy.
   *
   * In other words, this type's parents or supertypes.
   */
  constraints: Set<Type>;
}

/**
 * ## Associative Type
 *
 * A type that is fundamentally associative (a collection of morphisms from input types to output types).
 *
 * ### As a type
 *
 * The destination constraint must be an associative type and this type must satisfy its constraint.
 *
 * ### As a constraint
 *
 * The source type must be an associative type and:
 *
 * FOR each input type K_c *in the constraint*:
 *   K_c is assignable to *at least one* input in K_t
 *   AND
 *   FOR each type K_t in the inputs of the type where asg(K_c, K_t)
 *     LET V_t be the type activated by K_t, V_c be the constraint activated by K_c
 *       asg(V_t, V_c);
 *
 * The associative type is equivalent to an intersection of associative types each having only one of the encapsulated
 * morphisms. For example, assoc([U, V], [J, K]) is equivalent to assoc([U, V]) & assoc([J, K]).
 */
export interface AssociativeType<
  Assoc extends [Type, Type][] = [Type, Type][]
> {
  kind: "associative";
  /**
   * A list of the input, output pairs (morphisms) in this associative type.
   */
  morphisms: Assoc;
}

/**
 * ## Complement Type
 *
 * A type that represents the complement of an inner type, i.e. the set of all types that are _not_ assignable to the
 * inner type.
 *
 * ### Notation
 *
 * The complement of a type is denoted with a tilde (~) prefix. For example, the complement of a string is `~string`,
 * meaning any type that does not satisfy the string type.
 *
 * ### Satisfiability rules
 *
 * GIVEN types U and V.
 *
 * Some complement types are difficult to reason about. In the following sections we'll use a little venn-diagram
 * notation to reason about the satisfiability of complements. The venn diagram will be a pair of square brackets with
 * two sets of possibly intersecting parentheses in it. Both will be labeled `U` or `V`, and the `U` set will be on the
 * left and shaded using the `#` character.
 *
 * In all cases, we know that:
 *
 * sat(~(U | V), ~U)
 * sat(~(U | V), ~V)
 *
 * #### Disjoint (non-intersecting) types
 *
 * Diagram: [ (#U#) ( V ) ]
 *
 * GIVEN sat(U & V, never)
 *
 * sat(U, ~V)
 * sat(V, ~U)
 *
 * #### Subtypes
 *
 * GIVEN sat(U, V)
 *
 * Diagram: [ (#U#( V )#) ]
 *
 * sat(~U, ~V)
 *
 * #### Possibly-intersecting Types
 *
 * GIVEN !sat(U & V, never)
 *
 * Diagram: [ (#U#(#) V ) ]
 *
 * In this case, we aren't sure either that U or V is a subtype of the other or that they are disjoint, so we can't say
 * anything for certain about the satisfiability of these types. We therfore make no assumptions.
 */
export interface ComplementType<T extends Type = Type> {
  kind: "complement";

  /**
   * The inner type of this complement. The complement represents all types _not_ assignable to this type.
   */
  inner: T;
}

/**
 * ## Union Type
 *
 * A type that represents the union of several variants.
 *
 * ### As a type
 *
 * _Every_ variant must satisfy the destination constraint.
 *
 * ### As a constraint
 *
 * If the union is empty:
 *  - the source must also be an empty union.
 * If the union is not empty:
 *  - the source type must satisfy _some_ variant constraint.
 *
 * ### Notes
 *
 * The empty union is a bottom type (`!`). It has the property that it is assignable _to_ everything,
 * and only assignable _to_ its constraint is itself.
 *
 * You can think of adding a variant as adding possible values to the type, so having added nothing
 * should logically yield a bottom type with an empty set of possible values.
 */
export interface UnionType<Variants extends Type[] = Type[]> {
  kind: "union";

  /**
   * The possible variants of this union. The type satisfies _at least one_ of the variants.
   */
  variants: Variants;
}

/**
 * ## Intersection Type
 *
 * A type that represents the intersection of several constituents.
 *
 * ### As a type
 *
 * _Some_ constituent must satisfy the destination constraint.
 *
 * ### As a constraint
 *
 * An intersection constraint is satisfied if:
 *  - the intersection is empty.
 *  - OR the source type satisfies _every_ constituent constraint.
 *
 * ### Notes
 *
 * The empty intersection is a top type. It has the property that it is only assignable _to_ itself,
 * and any source type can be assigned _to_ its constraint.
 *
 * You can think of adding a constituent as adding a constraint to the type, so having added no constraints
 * should logically yield an unconstrained top type.
 */
export interface IntersectionType<Constituents extends Type[] = Type[]> {
  kind: "intersection";
  constituents: Constituents;
}

/**
 * ## Exotic Type
 *
 * A type that has a special implementation. This type chooses its own rules for assignment, satisfiability, associative
 * activation, and complement resolution.
 *
 * ### As a type
 *
 * The `effectiveType` specifies a type that will be used as the assigning type.
 *
 * ### As a constraint
 *
 * The `effectiveConstraint` specifies a type that will be used as the constraint.
 */
export interface ExoticType {
  kind: "exotic";

  /**
   * The display name of this type.
   */
  name: string;

  /**
   * If set to true, the display name of the type will be used verbatim when printing the type, instead of printing
   * it as `exotic(<name>)`.
   */
  suppressExoticInPrint?: true;

  /**
   * The effective type for this Exotic when assigning it to a constraint.
   */
  effectiveType: Type;

  /**
   * The effective constraint of for this Exotic when assigning another type to it.
   */
  effectiveConstraint: Type;

  /**
   * Computes the result of activating this type with a given input type.
   *
   * If this behavior is not specified, the activation will be computed using the _effective_ type or constraint,
   * whichever is appropriate depending on whether this exotic type is acting as a constraint or type.
   */
  activate?: (k: Type) => Type;

  /**
   * Computes the complement of this type.
   *
   * If this behavior is not specified, the complement will be computed using the _effective_ type or constraint,
   * whichever is contextually appropriate depending on whether this exotic type is acting as a constraint or a type.
   */
  complement?: () => Type;
}

/**
 * Checks if a given type satisfies a given constraint in the Elemental Type
 * System.
 *
 * The input types are first _resolved_ to their simplest form before checking
 * satisfiability. See {@link resolveType} for more information about type
 * resolution.
 *
 * @param source - the type to check if satisfies `constraint`
 * @param constraint - the type to check can be satisfied from `source`
 * @returns true if `source` satisfies `constraint`
 */
export function satisfies(source: Type, constraint: Type): boolean {
  // Somes types have more efficient resolutions (such as complement types) that are easier to check. We resolve the
  // types as much as possible before checking assignability.
  source = resolveType(source, false);
  constraint = resolveType(constraint, true);

  debug && console.log("Resolved:", printType(source), printType(constraint));

  if (source.kind === "complement" && constraint.kind === "complement") {
    return satisfies(constraint.inner, source.inner);
  }

  if (source.kind === "union") {
    return (
      (constraint.kind === "union" &&
        constraint.variants.length === 0 &&
        source.variants.length === 0) ||
      source.variants.every((t) => satisfies(t, constraint))
    );
  } else if (source.kind === "intersection") {
    return (
      (constraint.kind === "intersection" &&
        constraint.constituents.length === 0 &&
        source.constituents.length === 0) ||
      source.constituents.some((t) => satisfies(t, constraint))
    );
  }

  // Simple assignable-to cases
  switch (constraint.kind) {
    case "complement":
      const assignableTo = satisfies(source, constraint.inner);
      const assignableFrom = satisfies(constraint.inner, source);

      if (!assignableTo && !assignableFrom) {
        // Types are not mutually assignable or related as super/subtypes, so these types might be assignable depending
        // on the underlying types. For example, number: ~string is assignable, but cannot be expressed in terms of the
        // assignability of its operands. ~number : ~string is not assignable (not all the things that are not numbers
        // are also not strings). But, since we are sure that `dest` is not a model, union, or intersection in this case,
        // we are certain that the assignment of ~T1 to T2 is allowable in any case that T1 and T2 are not related.

        // TODO: not all satisfiability laws are implemented.
        debug &&
          console.log(
            "Assignable to complement:",
            printType(source),
            printType(constraint)
          );
        return true;
      } else {
        debug &&
          console.log(
            "Not assignable to complement:",
            printType(source),
            printType(constraint),
            assignableTo,
            assignableFrom
          );
        return false;
      }
    case "union":
      // One of empty union or empty intersection needs to special case the zero-length from/to assignment, and it's whichever one
      // cannot handle self-assignment depending on the order of assignable-to and assignable-from cases. Since assignable-to is
      // first here, we need to special case empty unions.
      return constraint.variants.some((t) => satisfies(source, t));
    case "intersection":
      return constraint.constituents.every((t) => satisfies(source, t));
  }

  // assignable-from cases
  switch (source.kind) {
    case "symbolic":
      if (constraint.kind === "symbolic" && constraint.id === source.id)
        return true;

      if (!source.constraints) return false;

      debug &&
        console.log(
          "Checking symbolic parents:",
          [...source.constraints].map(printType),
          "of",
          printType(source)
        );

      for (const parent of source.constraints) {
        if (satisfies(parent, constraint)) return true;
      }

      return false;
    case "associative":
      if (constraint.kind !== "associative") return false;

      for (const [din] of constraint.morphisms) {
        // destination inputs can match some source input, and whichever arm matches, the source output matches the destination output
        const doutActivated = activate(constraint, din);
        debug &&
          console.log(
            "Testing assignability of:",
            printType(source),
            printType(constraint)
          );
        if (
          doutActivated === null ||
          !source.morphisms.some(([sin]) => {
            const soutActivated = activate(source as AssociativeType, sin);
            debug && console.log("Wants (in):", printType(din), printType(sin));
            debug &&
              console.log(
                "Wants (out):",
                soutActivated && printType(soutActivated),
                printType(doutActivated)
              );
            return (
              soutActivated !== null &&
              satisfies(din, sin) &&
              satisfies(soutActivated, doutActivated)
            );
          })
        ) {
          debug &&
            console.log(
              "Not Assignable:",
              printType(source),
              printType(constraint)
            );
          return false;
        }
      }

      debug &&
        console.log("Assignable:", printType(source), printType(constraint));
      return true;
    default:
      throw new Error(`Not implemented: assignment from ${source.kind}`);
  }
}

/**
 * Gets the type that results from following the associative morphisms in `t`
 * that follow from `key`.
 *
 * If `t` contains multiple morphisms that follow from `key`, then the result is
 * a union of the types at the ends of all those morphisms.
 *
 * TODO: it is gross that this can return null. why did I implement it this way
 *
 * @param t - the type to activate
 * @param key - the type to activate `t` with
 * @returns the type result of activating `t[key]` or null if no activation is possible
 */
function activate(t: Type, key: Type): Type | null {
  if (t.kind === "exotic") {
    if (t.activate) return t.activate?.(key);

    // TODO: we need a way to say whether we're in constraint or type position and try activating the effective type

    throw new Error("cannot activate exotic type with no activator");
  } else if (t.kind === "associative") {
    const matching = t.morphisms
      .filter(([candidate]) => satisfies(key, candidate))
      .map(([_, value]) => value);

    if (matching.length === 1) return matching[0];
    else return Type.union(...matching);
  }

  return null;
}

// #region resolution

/**
 * Resolves `t` to a simpler form, if possible.
 *
 * In many cases, this removes complement or intersection types. It also expands exotic types to their resolved
 * effective type or constraint.
 *
 * See {@link resolveComplement} and {@link resolveIntersection} for more details.
 *
 * @param t - the type to resolve
 * @param constraint - whether or not we are resolving a constraint or a primary type
 * @returns
 */
export function resolveType(t: Type, constraint: boolean): Type {
  switch (t.kind) {
    case "exotic":
      return resolveType(
        constraint ? t.effectiveConstraint : t.effectiveType,
        constraint
      );
    case "complement":
      return resolveComplement(t, constraint);
    case "intersection":
      return resolveIntersection(t, constraint);
    case "union":
      return Type.union(...t.variants.map((t) => resolveType(t, constraint)));
    default:
      return t;
  }
}

/**
 * Iterates over all the types that are constraints of `sym`, including the constraints of all its parents, recursively,
 * not including any symbolic types themselves.
 *
 * Effectively this produces types such that the intersection of which is the full effective constraint of a given
 * symbolic type.
 *
 * @param sym - the symbolic type to get the effective constraints of
 * @param visited - a set of types that have already been visited, initialized to the empty set if not provided
 */
function* bfqSymbolicParents(
  sym: SymbolicType,
  visited: WeakSet<Type> = new WeakSet()
): Iterable<Type> {
  visited.add(sym);

  if (sym.constraints) {
    const next = [];
    for (const parent of sym.constraints) {
      if (!visited.has(parent)) {
        visited.add(parent);

        if (parent.kind === "symbolic") {
          next.push(parent);
        } else {
          yield parent;
        }
      }
    }

    for (const parent of next) {
      yield* bfqSymbolicParents(parent, visited);
    }
  }
}

/**
 * Gets the effective constraint of `sym`.
 *
 * This is the intersection of the effective constraints of all of `sym`s constraints.
 */
function getEffectiveSymbolicConstraint(sym: SymbolicType): Type {
  return resolveIntersection(
    {
      kind: "intersection",
      constituents: [...bfqSymbolicParents(sym)],
    },
    false
  );
}

/**
 * Get the effective intersection of two types `x` and `y`.
 *
 * This returns one of:
 *
 * - `[x]` if x is identical to y (i.e. x === y)
 * - `[x, y]` if either of x or y is not a symbolic type
 * - `[x]` if sat(x, y)
 * - `[y]` if sat(y, x)
 * - `[]` if neither sat(x, y) nor sat(y, x) and either of x or y is a peak type (i.e. has no constraints), indicating
 *   that the types are disjoint
 * - `[x, y]` otherwise (i.e. there is no known simplification)
 *
 * NOTE: if both sat(x, y) AND sat(y, x), then it will still return only `[x]`. This is okay because if `x` and `y` are
 * mutually satisfiable, then they are equivalent in an effective sense, even though they may not be _identical_.
 *
 * @param x
 * @param y
 * @returns
 */
function getEffectiveTypeIntersection(x: Type, y: Type): Type[] {
  if (x === y) return [x];

  if (x.kind === "symbolic" && y.kind === "symbolic") {
    debug &&
      console.log(
        "Computing effective intersection of:",
        printType(x),
        printType(y)
      );

    const xPeak = x.constraints.size === 0;
    const yPeak = y.constraints.size === 0;

    const xConstraint = xPeak ? x : getEffectiveSymbolicConstraint(x);
    const yConstraint = yPeak ? y : getEffectiveSymbolicConstraint(y);

    if (satisfies(x, yConstraint)) return [x];
    if (satisfies(y, xConstraint)) return [y];

    // If either is a peak type, we'll optimize this intersection down to nothing since it wasn't assignable in either
    // direction.
    // TODO: this optimization can be extended if neither type has a common peak ancestor.
    if (xPeak || yPeak) return [];

    return [x, y];
  } else return [x, y];
}

/**
 * Resolves an intersection type to a simpler form if possible.
 *
 * This resolution will:
 * - flatten nested intersections
 * - simplify intersections of one constituent to just that constituent
 * - optimize cases where the intersection contains two disjoint types
 * - optimize cases where the intersection contains two types that are satisfiable in either direction
 *
 * @param t - the intersection type to resolve
 * @param constraint - whether or not we are resolving a constraint or a primary type
 * @returns a simpler type, if possible
 */
function resolveIntersection(t: IntersectionType, constraint: boolean): Type {
  // Discard unknowns
  const constituents = t.constituents
    .map((t) => resolveType(t, constraint))
    .flatMap((t) => {
      if (t.kind === "intersection") {
        return t.constituents;
      } else {
        return t;
      }
    });

  if (constituents.length === 1) {
    return constituents[0];
  }

  let final: Type[] = [];

  debug && console.log("Resolving intersection:", printType(t));

  // TODO: this algorithm is a little wild. It could be bootstrapped immediately
  // with the first item in the intersection and then some code could be removed
  for (const cons of constituents) {
    // Early exit if any constituent is a bottom type
    if (isBottom(cons)) return cons;

    debug && console.log("Considering constituent:", printType(cons));

    if (final.length === 0) {
      // Bootstrap the iteration.
      final = [cons];
      continue;
    }

    // Clone final so we don't modify it during iteration
    const iter = [...final];
    final = [];

    for (const f of iter) {
      const pairwise = getEffectiveTypeIntersection(cons, f);

      debug &&
        console.log("Pairwise result:", cons, f, pairwise?.map(printType));

      // If we got an empty list, the types are disjoint and the result is never.
      if (pairwise.length === 0) return Type.never;

      // Otherwise, we got an array of 1-2 constituents that should be included in the type
      final = [...final, ...pairwise];
    }
  }

  const result = final.length === 1 ? final[0] : Type.intersection(...final);

  debug && console.log("Resolved intersection:", printType(result));

  return result;
}

/**
 * Resolves a complement type to a simpler form if possible.
 *
 * This resolution will:
 * - flatten nested complements
 * - apply DeMorgan's laws to complements of unions and intersections, resulting in:
 *   - `~(T1 | T2)` -> `~T1 & ~T2`
 *   - `~(T1 & T2)` -> `~T1 | ~T2`
 * - expand exotic types to their defined complements or to the complement of their effective type or constraint
 * - attempt to resolve the inner type and then try once more to resolve the outer complement replaced with the resolved
 *   inner type
 *
 * @param t - the complement type to resolve
 * @param constraint - whether or not we are resolving a constraint or a primary type
 * @returns a simpler type, if possible
 */
function resolveComplement(
  t: ComplementType,
  constraint: boolean,
  recur: boolean = true
): Type {
  switch (t.inner.kind) {
    case "complement":
      // resolve(~~T) -> resolve(T)
      return resolveType(t.inner.inner, constraint);
    case "union":
      // resolve(~(T1 | T2)) -> resolve(~T1) & resolve(~T2)
      return Type.intersection(
        ...t.inner.variants.map((t) =>
          resolveType({ kind: "complement", inner: t }, constraint)
        )
      );
    case "intersection":
      // resolve(~(T1 & T2)) -> resolve(~T1) | resolve(~T2)
      return Type.union(
        ...t.inner.constituents.map((t) =>
          resolveType({ kind: "complement", inner: t }, constraint)
        )
      );
    case "exotic":
      if (t.inner.complement) {
        return t.inner.complement();
      } else if (constraint) {
        return resolveComplement(
          Type.complement(t.inner.effectiveConstraint),
          constraint
        );
      } else {
        return resolveComplement(
          Type.complement(t.inner.effectiveType),
          constraint
        );
      }
    default:
      // Otherwise, resolve the complement of the inner type and disallow recursion
      const withResolvedInner = Type.complement(
        resolveType(t.inner, constraint)
      );

      return recur
        ? resolveComplement(withResolvedInner, constraint, false)
        : withResolvedInner;
  }
}

// #endregion

// #region utils

/**
 * Writes a string representation of a type.
 *
 * @param t - the type to write
 * @returns a string representation of the type.
 */
export function printType(t: Type): string {
  switch (t.kind) {
    case "exotic":
      return t.suppressExoticInPrint ? t.name : `exotic(${t.name})`;
    case "union":
      return t.variants.length == 0
        ? "!"
        : t.variants.map((v) => printType(v)).join(" | ");
    case "intersection":
      return t.constituents.length == 0
        ? "_"
        : t.constituents.map((v) => printType(v)).join(" & ");
    case "associative":
      if (t.morphisms.length === 0) return "{}";
      return `{ ${t.morphisms
        .map(([i, o]) => `[${printType(i)}] -> ${printType(o)}`)
        .join(", ")} }`;
    case "complement":
      return `~${printType(t.inner)}`;
    case "symbolic":
      return `${
        typeof t.id === "symbol"
          ? t.id.description
          : typeof t.id === "string"
          ? `"${t.id}"`
          : t.id
      }`;
  }
}

/**
 * @param t - the type to test for top
 * @returns true if `t` is the top type (empty intersection)
 */
function isTop(t: Type): t is IntersectionType<[]> {
  return t.kind === "intersection" && t.constituents.length === 0;
}

/**
 * @param t - the type to test for bottom
 * @returns true if `t` is the bottom type (empty union)
 */
function isBottom(t: Type): t is UnionType<[]> {
  return t.kind === "union" && t.variants.length === 0;
}

// #endregion

// #region tests

const tuple = Type.tuple(Type.literal("test"), Type.literal("value"));

const Foo = Type.record({
  a: Type.string,
});

const Bar = Type.record({
  b: Type.number,
});

console.log("RUNNING ALL TESTS: ...");

console.assert(satisfies(Type.never, Type.unknown), "bottom to top");
console.assert(satisfies(Type.never, Type.never), "bottom to bottom");
console.assert(!satisfies(Type.unknown, Type.never), "negative top to bottom");
console.assert(satisfies(Type.unknown, Type.unknown), "top to top");

console.assert(!satisfies(Type.unknown, Type.string), "negative top to mono");
console.assert(satisfies(Type.string, Type.unknown), "mono to top");
console.assert(satisfies(Type.never, Type.string), "bottom to mono");
console.assert(!satisfies(Type.string, Type.never), "negative mono to bottom");

console.assert(!satisfies(Type.string, Type.number), "negative unrelated mono");

console.assert(
  satisfies(Type.literal("test"), Type.string),
  "singleton to mono"
);
console.assert(
  !satisfies(Type.literal(1), Type.string),
  "negative singleton to mono"
);
console.assert(
  !satisfies(Type.string, Type.complement(Type.literal("test"))),
  "negative mono to complement related singleton"
);
console.assert(
  satisfies(Type.string, Type.complement(Type.literal(0))),
  "mono to complement unrelated singleton"
);

console.assert(
  satisfies(Type.string, Type.union(Type.string, Type.number)),
  "mono to union"
);
console.assert(
  !satisfies(Type.union(Type.string, Type.number), Type.string),
  "negative union to mono"
);
console.assert(
  !satisfies(Type.string, Type.intersection(Type.string, Type.number)),
  "negative mono to intersection"
);

console.assert(
  satisfies(Type.intersection(Type.string, Type.number), Type.string),
  "intersection to mono"
);

console.assert(
  satisfies(
    Type.union(Type.string, Type.number),
    Type.union(Type.string, Type.number, Type.boolean)
  ),
  "union to superunion"
);

console.assert(
  !satisfies(
    Type.union(Type.string, Type.number, Type.boolean),
    Type.union(Type.string, Type.number)
  ),
  "negative union to subunion"
);

console.assert(
  satisfies(
    Type.intersection(Type.string, Type.number),
    Type.intersection(Type.string, Type.number, Type.boolean)
  ),
  "disjoint intersection to subintersection"
);
console.assert(
  !satisfies(
    Type.intersection(Type.string, Type.literal("test")),
    Type.intersection(Type.string, Type.number)
  ),
  "negative intersection to subintersection"
);

console.assert(
  !satisfies(
    Type.string,
    Type.complement(Type.union(Type.string, Type.number))
  ),
  "negative mono to complement union"
);
console.assert(
  !satisfies(
    Type.union(Type.string, Type.number),
    Type.complement(Type.string)
  ),
  "negative union to complement mono"
);
console.assert(
  satisfies(
    Type.string,
    Type.complement(Type.intersection(Type.string, Type.number))
  ),
  "mono to complement disjoint intersection"
);
console.assert(
  satisfies(
    Type.intersection(Type.string, Type.number),
    Type.complement(Type.string)
  ),
  "disjoint intersection to complement related mono"
);

console.assert(
  satisfies(
    Type.intersection(Type.boolean, Type.number),
    Type.complement(Type.string)
  ),
  "disjoint intersection to complement unrelated mono"
);

// This works naturally because L contains number
console.assert(
  satisfies(Type.intersection(Type.boolean, Type.number), Type.number),
  "disjoint intersection to related mono"
);
// However, it is a desirable optimization to recognize that an intersection of two unrelated mono types is empty
console.assert(
  satisfies(Type.intersection(Type.boolean, Type.number), Type.string),
  "disjoint intersection to unrelated mono"
);

console.assert(
  !satisfies(Type.tuple(Type.string), Type.array(Type.string)),
  "negative tuple to array"
);

console.assert(
  satisfies(Type.array(Type.string), Type.tuple(Type.string)),
  "array to tuple"
);

console.assert(
  !satisfies(tuple, Type.array(Type.string)),
  "negative tuple of singletons to array"
);

console.assert(
  satisfies(tuple, Type.complement(Type.array(Type.string))),
  "tuple to array complement"
);

console.assert(
  !satisfies(
    Type.function([], Type.string),
    Type.function([], Type.literal("test"))
  ),
  "function result super"
);
console.assert(
  satisfies(
    Type.function([], Type.literal("test")),
    Type.function([], Type.string)
  ),
  "function result sub"
);
console.assert(
  satisfies(
    Type.array(Type.never),
    Type.array(Type.union(Type.string, Type.number))
  ),
  "empty array to array of union"
);

// Contravariance
console.assert(
  !satisfies(
    Type.function([Type.string], Type.unknown),
    Type.function([Type.union(Type.string, Type.number)], Type.unknown)
  ),
  "negative contravariant function parameters (narrows preconditions)"
);

console.assert(
  satisfies(
    Type.function([Type.union(Type.string, Type.number)], Type.unknown),
    Type.function([Type.string], Type.unknown)
  ),
  "contravariant function parameters (widens preconditions)"
);

console.assert(
  satisfies(
    Type.function([], Type.never),
    Type.function([Type.string], Type.unknown)
  ),
  "empty parameters to some params"
);

console.assert(
  !satisfies(
    Type.function([Type.string], Type.unknown),
    Type.function([], Type.unknown)
  ),
  "negative some parameters to empty params"
);

console.assert(
  satisfies(
    Type.function([Type.string, Type.number], Type.unit),
    Type.function([Type.string, Type.number, Type.boolean], Type.unknown)
  ),
  "many parameters tuple contravariance"
);

console.assert(
  satisfies(Type.tuple(Type.string, Type.number), Type.tuple(Type.string))
);

console.log(
  activate(
    Type.associative([Type.string, Type.number], [Type.bigint, Type.boolean]),
    Type.any
  )
);

// Some OO stuff

const _object = Type.symbolic(Symbol("Object"));
const IFoo = Type.symbolic(Symbol("IFoo"), [
  _object,
  Type.associative([Type.string, Type.number]),
]);
const FooImpl = Type.symbolic(Symbol("Foo"), [_object, IFoo]);

console.assert(satisfies(FooImpl, IFoo), "impl to interface");
console.assert(satisfies(FooImpl, _object), "impl to peak");
console.assert(
  satisfies(FooImpl, Type.associative([Type.string, Type.number])),
  "impl to assoc"
);
console.assert(satisfies(FooImpl, Type.unknown), "impl to top");
console.assert(
  satisfies(IFoo, Type.associative([Type.string, Type.number])),
  "interface to assoc"
);
console.assert(satisfies(IFoo, _object), "interface to peak");

console.assert(!satisfies(IFoo, FooImpl), "negative interface to impl");
console.assert(!satisfies(_object, FooImpl), "negative peak to impl");
console.assert(
  !satisfies(Type.associative([Type.string, Type.number]), FooImpl),
  "negative assoc to impl"
);
console.assert(!satisfies(Type.unknown, FooImpl), "negative top to impl");
console.assert(
  !satisfies(Type.associative([Type.string, Type.number]), IFoo),
  "negative assoc to interface"
);
console.assert(!satisfies(_object, IFoo), "negative peak to interface");

console.log("DONE");

// #endregion