Reworked the sub-type relationship infrastructure

README.md

@@ -40,9 +40,12 @@ Typir provides these core features:
 
 Typir does intentionally _not_ include ...
 
-- Rule engines and constraint solving
+- Rule engines and constraint solving,
+  since type inference is calculate in a recursive manner and does not use unification/substitution
 - Formal proofs
 - External DSLs for formalizing types
+- Support for dynamic type systems, which do typing during the execution of the DSL.
+  Typir aims at static type systems, which do typing during the writing of the DSL.
 
 
 ## NPM workspace
@@ -109,7 +112,7 @@ typir.factory.Operators.createBinary({ name: '-', signatures: [{ left: numberTyp
 As we'd like to be able to convert numbers to strings implicitly, we add the following line. Note that this will for example make it possible to concatenate numbers and strings with the `+` operator, though it has no signature for a number and a string parameter in the operator definition above.
 
 ```typescript
-typir.Conversion.markAsConvertible(numberType, stringType,'IMPLICIT_EXPLICIT');
+typir.Conversion.markAsConvertible(numberType, stringType, 'IMPLICIT_EXPLICIT');
 ```
 
 Furthermore we can specify how Typir should infer the variable type. We decided that the type of the variable should be the type of its initial value. Typir internally considers the inference rules for primitives and operators as well, when recursively inferring the given AstElement.

examples/lox/src/language/lox-module.ts

@@ -18,7 +18,7 @@ import { LoxLinker } from './lox-linker.js';
  */
 export type LoxAddedServices = {
     validation: {
-        LoxValidator: LoxValidator
+        LoxValidator: LoxValidator,
     },
     typir: LangiumServicesForTypirBinding,
 }
@@ -38,7 +38,7 @@ export function createLoxModule(shared: LangiumSharedCoreServices): Module<LoxSe
     return {
         validation: {
             ValidationRegistry: (services) => new LoxValidationRegistry(services),
-            LoxValidator: () => new LoxValidator()
+            LoxValidator: () => new LoxValidator(),
         },
         // For type checking with Typir, inject and merge these modules:
         typir: () => inject(Module.merge(
@@ -73,7 +73,7 @@ export function createLoxServices(context: DefaultSharedModuleContext): {
 } {
     const shared = inject(
         createDefaultSharedModule(context),
-        LoxGeneratedSharedModule
+        LoxGeneratedSharedModule,
     );
     const Lox = inject(
         createDefaultCoreModule({ shared }),

packages/typir/src/graph/graph-algorithms.ts

@@ -0,0 +1,122 @@
+/******************************************************************************
+ * Copyright 2025 TypeFox GmbH
+ * This program and the accompanying materials are made available under the
+ * terms of the MIT License, which is available in the project root.
+ ******************************************************************************/
+
+import { TypirServices } from '../typir.js';
+import { TypeEdge } from './type-edge.js';
+import { TypeGraph } from './type-graph.js';
+import { Type } from './type-node.js';
+
+export interface GraphAlgorithms {
+    collectReachableTypes(from: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): Set<Type>;
+    existsEdgePath(from: Type, to: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): boolean;
+    getEdgePath(from: Type, to: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): TypeEdge[];
+}
+
+export class DefaultGraphAlgorithms implements GraphAlgorithms {
+    protected readonly graph: TypeGraph;
+
+    constructor(services: TypirServices) {
+        this.graph = services.infrastructure.Graph;
+    }
+
+    collectReachableTypes(from: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): Set<Type> {
+        const result: Set<Type> = new Set();
+        const remainingToCheck: Type[] = [from];
+
+        while (remainingToCheck.length > 0) {
+            const current = remainingToCheck.pop()!;
+            const outgoingEdges = $relations.flatMap(r => current.getOutgoingEdges(r));
+            for (const edge of outgoingEdges) {
+                if (filterEdges === undefined || filterEdges(edge)) {
+                    if (result.has(edge.to)) {
+                        // already checked
+                    } else {
+                        result.add(edge.to); // this type is reachable
+                        remainingToCheck.push(edge.to); // check it for recursive conversions
+                    }
+                }
+            }
+        }
+
+        return result;
+    }
+
+    existsEdgePath(from: Type, to: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): boolean {
+        const visited: Set<Type> = new Set();
+        const stack: Type[] = [from];
+
+        while (stack.length > 0) {
+            const current = stack.pop()!;
+            visited.add(current);
+
+            const outgoingEdges = $relations.flatMap(r => current.getOutgoingEdges(r));
+            for (const edge of outgoingEdges) {
+                if (filterEdges === undefined || filterEdges(edge)) {
+                    if (edge.to === to) {
+                        /* It was possible to reach our goal type using this path.
+                         * Base case that also catches the case in which start and end are the same
+                         * (is there a cycle?). Therefore it is allowed to have been "visited".
+                         * True will only be returned if there is a real path (cycle) made up of edges
+                         */
+                        return true;
+                    }
+                    if (!visited.has(edge.to)) {
+                        /* The target node of this edge has not been visited before and is also not our goal node
+                         * Add it to the stack and investigate this path later.
+                         */
+                        stack.push(edge.to);
+                    }
+                }
+            }
+        }
+
+        // Fall through means that we could not reach the goal type
+        return false;
+    }
+
+    getEdgePath(from: Type, to: Type, $relations: Array<TypeEdge['$relation']>, filterEdges?: (edgr: TypeEdge) => boolean): TypeEdge[] {
+        const visited: Map<Type, TypeEdge|undefined> = new Map(); // the edge from the parent to the current node
+        visited.set(from, undefined);
+        const stack: Type[] = [from];
+
+        while (stack.length > 0) {
+            const current = stack.pop()!;
+
+            const outgoingEdges = $relations.flatMap(r => current.getOutgoingEdges(r));
+            for (const edge of outgoingEdges) {
+                if (filterEdges === undefined || filterEdges(edge)) {
+                    if (edge.to === to) {
+                        /* It was possible to reach our goal type using this path.
+                         * Base case that also catches the case in which start and end are the same
+                         * (is there a cycle?). Therefore it is allowed to have been "visited".
+                         * True will only be returned if there is a real path (cycle) made up of edges
+                         */
+                        const result: TypeEdge[] = [edge];
+                        // collect the path of used edges, from "to" back to "from"
+                        let backNode = edge.from;
+                        while (backNode !== from) {
+                            const backEdge = visited.get(backNode)!;
+                            result.unshift(backEdge);
+                            backNode = backEdge.from;
+                        }
+                        return result;
+                    }
+                    if (!visited.has(edge.to)) {
+                        /* The target node of this edge has not been visited before and is also not our goal node
+                         * Add it to the stack and investigate this path later.
+                         */
+                        stack.push(edge.to);
+                        visited.set(edge.to, edge);
+                    }
+                }
+            }
+        }
+
+        // Fall through means that we could not reach the goal type
+        return [];
+    }
+
+}

packages/typir/src/initialization/type-selector.ts

@@ -23,7 +23,7 @@ export type BasicTypeSelector =
  */
 export type TypeSelector =
     | BasicTypeSelector             // all base type selectors
-    | (() => BasicTypeSelector)    // all type selectors might be given as functions as well, in order to ease delayed specifications
+    | (() => BasicTypeSelector)     // all type selectors might be given as functions as well, in order to ease delayed specifications
     ;
 
 
@@ -33,7 +33,7 @@ export interface TypeResolvingService {
      * This method does not care about the initialization state of the found type,
      * this method is restricted to just search and find any type according to the given TypeSelector.
      * @param selector the specification for the desired type
-     * @returns the found type or undefined, it there is no such type in the type system
+     * @returns the found type; or undefined, it there is no such type in the type system
      */
     tryToResolve<T extends Type = Type>(selector: TypeSelector): T | undefined;
 

packages/typir/src/kinds/bottom/bottom-type.ts

@@ -5,19 +5,49 @@
  ******************************************************************************/
 
 import { TypeEqualityProblem } from '../../services/equality.js';
-import { SubTypeProblem } from '../../services/subtype.js';
+import { SubTypeProblem, SubTypeResult } from '../../services/subtype.js';
 import { isType, Type } from '../../graph/type-node.js';
 import { TypirProblem } from '../../utils/utils-definitions.js';
 import { createKindConflict } from '../../utils/utils-type-comparison.js';
 import { BottomKind, BottomTypeDetails, isBottomKind } from './bottom-kind.js';
+import { TypeGraphListener } from '../../graph/type-graph.js';
+import { TypeEdge } from '../../graph/type-edge.js';
 
-export class BottomType extends Type {
+export class BottomType extends Type implements TypeGraphListener {
     override readonly kind: BottomKind;
 
     constructor(kind: BottomKind, identifier: string, typeDetails: BottomTypeDetails) {
         super(identifier, typeDetails);
         this.kind = kind;
         this.defineTheInitializationProcessOfThisType({}); // no preconditions
+
+        // ensure, that this Bottom type is a sub-type of all (other) types:
+        const graph = kind.services.infrastructure.Graph;
+        graph.getAllRegisteredTypes().forEach(t => this.markAsSubType(t)); // the already existing types
+        graph.addListener(this); // all upcomping types
+    }
+
+    override dispose(): void {
+        this.kind.services.infrastructure.Graph.removeListener(this);
+    }
+
+    protected markAsSubType(type: Type): void {
+        if (type !== this) {
+            this.kind.services.Subtype.markAsSubType(this, type, { checkForCycles: false });
+        }
+    }
+
+    addedType(type: Type, _key: string): void {
+        this.markAsSubType(type);
+    }
+    removedType(_type: Type, _key: string): void {
+        // empty
+    }
+    addedEdge(_edge: TypeEdge): void {
+        // empty
+    }
+    removedEdge(_edge: TypeEdge): void {
+        // empty
     }
 
     override getName(): string {
@@ -53,8 +83,10 @@ export class BottomType extends Type {
         } else {
             return [<SubTypeProblem>{
                 $problem: SubTypeProblem,
+                $result: SubTypeResult,
                 superType: this,
                 subType: subType,
+                result: false,
                 subProblems: [createKindConflict(this, subType)],
             }];
         }

packages/typir/src/kinds/class/class-type.ts

@@ -5,7 +5,7 @@
  ******************************************************************************/
 
 import { TypeEqualityProblem } from '../../services/equality.js';
-import { SubTypeProblem } from '../../services/subtype.js';
+import { SubTypeProblem, SubTypeResult } from '../../services/subtype.js';
 import { isType, Type } from '../../graph/type-node.js';
 import { TypeReference } from '../../initialization/type-reference.js';
 import { TypirProblem } from '../../utils/utils-definitions.js';
@@ -55,13 +55,16 @@ export class ClassType extends Type {
             const superRef = new TypeReference<ClassType>(superr, kind.services);
             superRef.addListener({
                 onTypeReferenceResolved(_reference, superType) {
-                    // after the super-class is complete, register this class as sub-class for that super-class
-                    superType.subClasses.push(thisType);
+                    // after the super-class is complete ...
+                    superType.subClasses.push(thisType); // register this class as sub-class for that super-class
+                    kind.services.Subtype.markAsSubType(thisType, superType, // register the sub-type relationship in the type graph
+                        { checkForCycles: false }); // ignore cycles in sub-super-class relationships for now, since they are reported with a dedicated validation for the user
                 },
                 onTypeReferenceInvalidated(_reference, superType) {
                     if (superType) {
-                        // if the superType gets invalid, de-register this class as sub-class of the super-class
-                        superType.subClasses.splice(superType.subClasses.indexOf(thisType), 1);
+                        // if the superType gets invalid ...
+                        superType.subClasses.splice(superType.subClasses.indexOf(thisType), 1); // de-register this class as sub-class of the super-class
+                        // TODO unmark sub-type relationship (or already done automatically, since the type is removed from the graph?? gibt es noch andere Möglichkeiten eine Reference zu invalidieren außer dass der Type entfernt wurde??)
                     } else {
                         // initially do nothing
                     }
@@ -185,8 +188,10 @@ export class ClassType extends Type {
         } else {
             return [<SubTypeProblem>{
                 $problem: SubTypeProblem,
+                $result: SubTypeResult,
                 superType,
                 subType: this,
+                result: false,
                 subProblems: [createKindConflict(this, superType)],
             }];
         }
@@ -198,8 +203,10 @@ export class ClassType extends Type {
         } else {
             return [<SubTypeProblem>{
                 $problem: SubTypeProblem,
+                $result: SubTypeResult,
                 superType: this,
                 subType,
+                result: false,
                 subProblems: [createKindConflict(subType, this)],
             }];
         }

packages/typir/src/kinds/class/class-validation.ts

@@ -181,7 +181,7 @@ export class UniqueMethodValidation<T> implements ValidationRuleWithBeforeAfter
 /**
  * Predefined validation to produce errors for all those class declarations, whose class type have cycles in their super-classes.
  * @param isRelevant helps to filter out declarations of classes in the user AST,
- * is parameter is the reasons, why this validation cannot be registered by default by Typir for classes, since this parameter is DSL-specific
+ * this parameter is the reasons, why this validation cannot be registered by default by Typir for classes, since this parameter is DSL-specific
  * @returns a validation rule which checks for any class declaration/type, whether they have no cycles in their sub-super-class-relationships
  */
 export function createNoSuperClassCyclesValidation(isRelevant: (languageNode: unknown) => boolean): ValidationRule {

packages/typir/src/kinds/class/top-class-type.ts

@@ -5,20 +5,50 @@
  ******************************************************************************/
 
 import { TypeEqualityProblem } from '../../services/equality.js';
-import { SubTypeProblem } from '../../services/subtype.js';
+import { SubTypeProblem, SubTypeResult } from '../../services/subtype.js';
 import { isType, Type } from '../../graph/type-node.js';
 import { TypirProblem } from '../../utils/utils-definitions.js';
 import { createKindConflict } from '../../utils/utils-type-comparison.js';
 import { TopClassKind, TopClassTypeDetails, isTopClassKind } from './top-class-kind.js';
 import { isClassType } from './class-type.js';
+import { TypeGraphListener } from '../../graph/type-graph.js';
+import { TypeEdge } from '../../graph/type-edge.js';
 
-export class TopClassType extends Type {
+export class TopClassType extends Type implements TypeGraphListener {
     override readonly kind: TopClassKind;
 
     constructor(kind: TopClassKind, identifier: string, typeDetails: TopClassTypeDetails) {
         super(identifier, typeDetails);
         this.kind = kind;
         this.defineTheInitializationProcessOfThisType({}); // no preconditions
+
+        // ensure, that all (other) Class types are a sub-type of this TopClass type:
+        const graph = kind.services.infrastructure.Graph;
+        graph.getAllRegisteredTypes().forEach(t => this.markAsSubType(t)); // the already existing types
+        graph.addListener(this); // all upcomping types
+    }
+
+    override dispose(): void {
+        this.kind.services.infrastructure.Graph.removeListener(this);
+    }
+
+    protected markAsSubType(type: Type): void {
+        if (type !== this && isClassType(type)) {
+            this.kind.services.Subtype.markAsSubType(type, this, { checkForCycles: false });
+        }
+    }
+
+    addedType(type: Type, _key: string): void {
+        this.markAsSubType(type);
+    }
+    removedType(_type: Type, _key: string): void {
+        // empty
+    }
+    addedEdge(_edge: TypeEdge): void {
+        // empty
+    }
+    removedEdge(_edge: TypeEdge): void {
+        // empty
     }
 
     override getName(): string {
@@ -49,8 +79,10 @@ export class TopClassType extends Type {
         } else {
             return [<SubTypeProblem>{
                 $problem: SubTypeProblem,
+                $result: SubTypeResult,
                 superType,
                 subType: this,
+                result: false,
                 subProblems: [createKindConflict(superType, this)],
             }];
         }
@@ -63,8 +95,10 @@ export class TopClassType extends Type {
         } else {
             return [<SubTypeProblem>{
                 $problem: SubTypeProblem,
+                $result: SubTypeResult,
                 superType: this,
                 subType,
+                result: false,
                 subProblems: [createKindConflict(this, subType)],
             }];
         }