Announcing Typir

We present our latest open source project: Typir!

Typir is a TypeScript library for building type systems for the web platform without any dependencies. It helps to implement type checking for languages by providing core type checking features out-of-the-box and predefined types to reuse. Instead of hand-writing the type system for your language from scratch, just describe it by reusing predefined types and by declaring rules for inference and validation with Typir!

Motivation for type checking

Type systems are central for implementing general purpose programming languages and domain-specific languages (DSLs) using expressions, operators, data types, functions and so on. They enrich languages with a description of their static semantics and enable advanced features for linking, validation and language processing, as motivated in the following.

Type systems enable you to write type-related checks during validation: You can implement assignability checking and provide type errors, for example if the inferred type of a value is not assignable to the declared type of the variable it is written to. Another standard check is that the condition of if statements needs to evaluate to a boolean value and not to a number value. As an example, 2 * 3 is a syntactically valid expression, but semantically it is valid only in certain contexts, e.g. it is valid as a value for a number variable (var v1: number = 2 * 3;), but it is not valid as a condition (if (2 * 3) { ... }).

The linking of calls of overloaded functions also depends on type checking since the types of the given arguments are required to identify the called function via the types of their declared input parameters. Another example might be accessing members on variables with complex data types, e.g. to resolve links in an expression like instance1.member1, the type of instance1 needs to be inferred as starting point to search for its members in order to resolve member1.

Language processors including interpreters and code generators might use type systems to map the types from the source language to the types of the target language.

All these three use cases for type checking for linking, validation and language processing require helpful error messages in order to support users to fix occurred typing issues.

Objectives

The objective of Typir is to support language engineering and modelling projects with type checking for the web platform. Typir is designed as stand-alone library providing core type checking features and predefined, reusable types for less hand-written code. Typir provides an easy starting point for developing type systems as well as solutions for recurring challenges including overloading, caching, type interdependencies, supports writing meaningful error messages, and helps to customize and extend the provided default features. Typir focuses more on providing pragmatic solutions for recurring type checking challenges in practice and less on constraint solving or formal proofs.

Design decisions

Typir is developed open-source on GitHub under the MIT licence, which allows to use Typir even in commercial and closed-source projects. Completely written in TypeScript, Typir is ready for the web platform and provides a TypeScript-based API for developers to define type systems. Therefore, developers don’t need to learn another external DSL and are able to smoothly integrate Typir with their existing code base.

We designed Typir to be independent from any language workbench for the following reasons:

• Type checking is helpful for various language engineering projects
• Types and other type-related information don’t need to be weaved into existing AST data structures since they form a separate type graph
• Type-related algorithms work on this type graph and are independent from the AST in principle

Nevertheless, since Langium is used in many projects for textual languages in the web, Typir provides the dedicated binding Typir-Langium, which extends the core Typir library and provides a smooth integration for Langium-based language projects.

Typir predefines the following types, which can be reused and configured:

• Primitives
• Functions with overloading
• Operators with overloading
• Nominally typed classes (like in Java)
• Top and bottom types (like unknown and never in TypeScript)

Typir provides the following core features for type systems:

• Assignability (to check whether a type is assignable to another type)
• Equality (to check whether two types are equal)
• Conversion (to define rules for implicit conversion and explicit casting between types)
• Type inference (to infer the type from a given language node like a node from an AST)
• Sub-typing (to define sub-type relationships between types)
• Validation (to define and evaluate type-related validations for ASTs)

Typir provides default implementations for these features, which might be customized to project-specific needs by dependency injection. Additionally, Typir is open to support project-specific types in general.

Tiny Typir

To get a first impression for the Typir API, it is helpful to look at a small example. We created the small expression language Tiny Typir for this purpose and encourage you to check out the full example. Here we provide a small sneak peek, already.

As mentioned above, one thing to be implemented for most languages is the support of assignability checks. The language Tiny Typir has only a few concepts, among them numbers (NumberLiteral), strings (StringLiteral), variables (Variable), and assignments (AssignmentStatement). All are implemented in a simple way as AstElements.

The following code snippet shows the way you set up the Typir type system and create the primitive types for NumberLiteral and StringLiteral, including their inference rules, with the help of Typir’s predefined Primitives factory service.

const typir = createTypirServices<AstElement>(); // <AstElement> specifies the root type

const numberType = typir.factory.Primitives.create({ primitiveName: 'number' })
    .inferenceRule({ filter: node => node instanceof NumberLiteral }).finish();

const stringType = typir.factory.Primitives.create({ primitiveName: 'string' })
    .inferenceRule({ filter: node => node instanceof StringLiteral }).finish();

As we’d like to be able to convert numbers to strings implicitly, we add the following line to introduce this:

typir.Conversion.markAsConvertible(numberType, stringType, 'IMPLICIT_EXPLICIT');

Getting back to our goal of checking types for assignments, we specify how Typir should infer the variable type, asking it to use the type of the variable’s initial value for this. Typir recursively applies all defined inference rules on the variable’s initial value to identify its type.

typir.Inference.addInferenceRule(node => {
    if (node instanceof Variable) {
        return node.initialValue; // the type of the variable is the type of its initial value
    }
    return InferenceRuleNotApplicable;
});

Now we can add the desired validation rule for the AssignmentStatement. We check whether the type to be assigned is an assignable match for the variable type and show an error with the specified custom message when the types don’t match.

typir.validation.Collector.addValidationRule((node, accept) => {
    if (node instanceof AssignmentStatement) {
        typir.validation.Constraints.ensureNodeIsAssignable(node.right, node.left, accept, (actual, expected) => ({ message:
            `The type '${actual.name}' is not assignable to the type '${expected.name}'.` }));
    }
});

For example, this error will show up, if we try to assign "hello" to a number variable. But this error will not be displayed, if we assign the number literal 123 to a string variable, the latter due to our conversion definition above.

If you are interested to see the test examples for this and learn how to support BinaryExpressions including overloads, refer to the full example, please.

The main README file also is a good starting point for a deeper dive into Typir, including a number of helpful links. Also there is a video of Johannes’ OCX talk about Typir available in case you prefer this format. If you are interested in Typir support for languages developed with Langium, the lead example applications for OX and LOX will see you covered.

The future

We at TypeFox started the development of Typir in 2024 and are investing continuously into Typir in order to bring type checking to the next level. The roadmap for the upcoming versions includes, among others, the following features and integrations:

• Structurally typed classes (like in TypeScript)
• Simplified API for custom types
• More integrations for Typir, e.g. a binding for LionWeb, as sketched in this blog post
• Website with documentation
• … and more based on your feedback!

Try out Typir and send us feedback on GitHub:

• Discussions for questions and discussions
• Issues for bug reports and feature suggestions

Happy typing with Typir!