Initial draft of the type system API

[msujew]

For anyone who wants to see how this API is supposed to look like. I will accept feedback on the API direction and then start implementing the library.

[Lotes]

readonly && writeonly? Maybe use an enum/string union

[montymxb]

I would agree as well.

[montymxb]

Went through several iterations of points, going back & forth to compare what's written in the proposal vs. the API spec here. The goal of this feedback is to help align the API to the desired spec & intended breadth of the Typir library (focusing less on inference & checking, more on type system structural foundation stuff). Hopefully the feedback is helpful!

There are some questions as well, as I'm interpreting what the intended API will look like. I'm also definitely open for discussion on suggestions, questions, etc., but as is this is already looking quite interesting 👀 .

Here are some general points I would like to add, in addition to the more targeted feedback.

• A list-type type would be great to add, same as function-type has been added already.
• Feels like typeParams & args are duplicated throughout, I feel this can be factored out to just 'types'
• Options interfaces duplicate a lot of information, I would consider revising this, or at least refactoring in order to remove the overlap between options and the corresponding type/type constructor.
• Type constructor variance could be extended to apply more generally to type constructors (especially if List is added, this could also benefit from variance)
• I would consider adding a TypeRule interface. There's already several instances of type judgements which describe the form that rules can take (assignable, castable). Making it easier to define rules more generally would allow a greater degree of flexibility in the system design. We could still abstract away the finer details using this API, but all rules could then be changed if needed to customize behavior. Note this does not require adding a type checking system, but it would provide a nice form that a checker could then consume to perform inference & checking.
• Adding to the point above, getting all types & rules (relationships) between types would be a nice feature to add to the type system foundation.
• TypeSystem is not entirely accurate for what this does, but it makes the most sense when describing what this will be used for. This almost feels like a TypeGraph already, since we're defining nodes (types, categories, etc.), and then defining relationships on those nodes (edges). However, this naming can also lead to misconceptions, so it would be worthwhile to think about a name that indicates we're building a foundation for a type system to be built off of, rather than the complete type system itself.

[montymxb]

Members appear to be annotated types, with name & optional in addition. This could extend Type, and supplement with additional properties to give it the same look & feel.

[montymxb]

This allows adding multiple members that share the same name. It might be easier to instead go with a map/record.

[JohannesMeierSE]

But the order of members is important, isn't it?

[montymxb]

This would be nice to have at the level of all types, and not just functions. This would go along with the notion that a type may or may not be generic, but is still a type. The API could be retained like so, but it may help to then be able to invoke the same constraints on the param & return types.

[montymxb]

Hmm, this feels like a specialized case of a function parameter. Internally this also places a constraint on the kinds of types this parameter can match with, feels like defining a typing rule before actually writing one. Not necessarily bad, but it may make it difficult to reason about typing rules/relationships later.

[montymxb]

A thought, do we really want to support the spread operator? I'm sure the case comes up, but is it often enough to really need to support it directly, rather than having it be implemented by devs when needed themselves. How often does this come up in languages that are expressed in Langium?

[JohannesMeierSE]

I would like to see support for the spread operator by Typir in general, but I am not sure, how to integrate it. Maybe as an add-on?

[montymxb]

Hmm, interesting, so does this imply types are capable of being modified in this system? If so, we're working with open types, which is more like interfaces than types, and will greatly complicate reasoning about them.

[montymxb]

This looks nice from API perspective, but I'm curious how this would be implemented internally. Is the plan to have relationships for types stored on types, or higher up within the system itself. The latter would make it much easier to get information about all relationships/rules.

[montymxb]

I'm a little confused by the usage of a 'category' of things, as this is very general.

If this is being used to express classes, structs, and interfaces, why not provide a more direct representation to express classes, structs, and interfaces directly? Unless there's a concrete motivation to making a general type category, I would lean on keeping it simple and targeting known cases first. If it turns out we need something more general, we can always add it in later.

This would also be good considering the audience, which is likely not so versed in type theory, or type systems in general. Keeping to familiar terms & type forms will help users to leverage this library as intended, and effectively.

[montymxb]

Type constructors in general can exhibit variance, not just parameters. Might be worthwhile considering this, especially if we add a generic List type.

[montymxb]

Question for the choice of naming TypeSystem here. A complete type system would describe the types, judgement forms, rules, and logic for resolving types using these rules. This implementation allows defining types, and has some judgement forms already (assignable, castable), and will probably have a bit of logic there, but it's incomplete. There's no functionality to infer/typecheck expressions, which should be provided by the user. It's more of a structure for a system to be built on top of, maybe TypeSystemStructure or TypeFoundation would more clearly convey this aspect.

[trusktr]

Can we see the proposal of what is being implemented somewhere? Or is it all in code only so far?

[msujew]

@trusktr I've created an internal document that shows potential usage of this API before I started working on this. Note that the API has changed a bit while developing this PR, but the main ideas are still there.

// A typed function that initializes a whole generic type system
// Every type has a `literal` that can be seen as its "source"
// We clarify that each literal is of type `AstNode`
const typeSystem = createTypeSystem<AstNode>();

// primitives
const stringType = typeSystem.primitive('string');
const numberType = typeSystem.primitive('number');
// Create an `any` type and set is as the top type of the type system
const anyType = typeSystem.primitive('any').top();

// operators
const plus = typeSystem.operator('+');
// the 'operate' function returns a `Disposable`
// In case we allow user-contributed operator overloads, these need to be deleted at some point
plus.operate({
	operands: stringType,
  result: stringType
});

plus.operate({
  operands: [stringType, numberType],
  order: 'flexible' // 'strict' would mean that number + string would not be valid here
  result: stringType
});

// 
plus.operate({
  operands: [stringType, anyType],
  result: stringType,
  priority: -1
});

// classes, structs, interfaces
// These structures are classified as "categories"
const classType = typeSystem.category('class');
const interfaceType = typeSystem.category('interface');
const structType = typeSystem.category('struct');

classType.assignable(classType, (from, to) => {
  // This is likely the default implementation for any complex type structure
  // This will likely be exposed as `defaultNamedAssignability`
  if (from.literal === to.literal) {
	  return true;
  }
  if (from.super.some(e => typeSystem.isAssignable(e, to)) {
    return true;
  }
  return false;
});
classType.assignable(interfaceType, defaultNamedAssignability);
structType.assignable(structType, defaultNamedAssignability);
structType.assignable(interfaceType, defaultNamedAssignability);
interfaceType.assignable(interfaceType, defaultNamedAssignability);
// In addition, the library also exports a `defaultStructuralAssignability` function
// This allows for example for a fully structural type system (such as TypeScript) or a partially structural type system
// Such a type system can for example use named assignability for classes, while using structural assignability for interfaces

// These types can then be specialized to create their class/struct/interface instances
const classInstance = classType.get(classLiteral);
// `classInstance` is an disposable instance of the type system.
// It features the same API and can be used to implement more complex type behavior

// This is an example of a user defined implicit casting function
// Like most things, it returns a disposable
classInstance.assignable((from, to) => {
  return typeSystem.isAssignable(implicitCastingType, to);
});

// Example of a user defined explicit casting function
classInstance.castable((from, to) => {
  return typeSystem.isAssignable(explicitCastingLiteral, to);
});

// Complex type instances can also be generic
// We first have to define the type parameters
const genericSimpleType = typeSystem.typeParameter({
  name: 'T';
});

const genericConstraintType = typeSystem.typeParameter({
  name: 'T2',
  // A constraint if effectively just a function with (Type) => boolean
  // The type system object provides a few default constraints (such as `extends`)
  contraints: [
    typeSystem.extends(someClassLiteral)
  ]
});

const genericInstance = classType.get({
 literal: classLiteral
 parameters: [genericSimpleType, genericConstraintType]
});

// The generic types can be accessed using the `genericInstance`
const typeParameters = genericInstance.typeParameters

// A generic class can be specialized with type instances
const genericInstanceWithArguments = genericInstance.typeArguments([
  T1Instance,
  T2Instance 
});

// Language validators need to assert that T2Instance fits the constraints
typeSystem.assertConstraints(typeParameters[1], T2Instance);

// All types can have members
// push also returns a disposable
// This allows to declare partial classes or extension functions/properties
// And also remove them on an update of their declaring document/class
classInstance.members.push(...members);

// Delegate types
const delegateInstance = typeSystem.delegate({
  // names are usually optional throughout the whole type system
  // The type system needs to support inline types
  name: '...',
  literal: delegateLiteral,
  parameters: [],
  returnType: ...,
  generics: []
});

// Union types
const unionInstance = typeSystem.union({
  literal: unionLiteral,
  generics: [ /** can also support generics */ ]
});

[JohannesMeierSE]

Here are my general thoughts about this API proposal:

• I am thinking of splitting the "type graph" (as mentioned by Ben above) and functionalities working on the type information. Maybe, we could apply the "service-oriented" design of Langium here as well. That would ease to exchange, configure and replace implementations depending on customer needs.
• Additionally, we could separate higher-level features (e.g. isAssignable) and lower-level algorithms (e.g. getCommonSuperType) for better reuse and customization.
• I propose to integrate at least one simple application example for the API as early as possible and directly into the source code, e.g. the pasted code snippet or another simple application.

Some more things we probably need:

• functions to produce nice error messages
• a nice API for ..., depending on the customer's DSL:
  • mapping terms/expressions with types
  • relating types to each other, e.g. sub/super types