Implement duck typing

[theogiraudet]

Hey!

I continue my exploration of Typir by trying to understand how the class type works.
I've seen that there are four inference properties: inferenceRuleForDeclaration, inferenceRuleForConstructor, inferenceRuleForReference, and inferenceRuleForFieldAccess.
By looking at the Lox example, I'm honestly not really sure of the goal of each:

typir/examples/lox/src/language/lox-type-checking.ts

Lines 219 to 235 in 8a04e85

	inferenceRuleForDeclaration: (languageNode: unknown) => languageNode === node,
	// inference rule for constructor calls (i.e. class literals) conforming to the current class
	inferenceRuleForConstructor: { // <InferClassLiteral<MemberCall>>
	filter: isMemberCall,
	matching: (languageNode: MemberCall) => isClass(languageNode.element?.ref) && languageNode.element!.ref.name === className && languageNode.explicitOperationCall,
	inputValuesForFields: (_languageNode: MemberCall) => new Map(), // values for fields don't matter for nominal typing
	},
	inferenceRuleForReference: { // <InferClassLiteral<TypeReference>>
	filter: isTypeReference,
	matching: (languageNode: TypeReference) => isClass(languageNode.reference?.ref) && languageNode.reference!.ref.name === className,
	inputValuesForFields: (_languageNode: TypeReference) => new Map(), // values for fields don't matter for nominal typing
	},
	// inference rule for accessing fields
	inferenceRuleForFieldAccess: (languageNode: unknown) => isMemberCall(languageNode) && isFieldMember(languageNode.element?.ref) && languageNode.element!.ref.$container === node && !languageNode.explicitOperationCall
	? languageNode.element!.ref.name : InferenceRuleNotApplicable,
	associatedLanguageNode: node,
	});

If I correctly understand, here:

• inferenceRuleForConstructor is used to type an instantiation, such as Class()
• inferenceRuleForReference is used when the class is used as a type, for instance in nested: NestedClass
• inferenceRuleForFieldAccess is used when a property is accessed and it is not a method call, for instance x.a
• According to the name, I suppose that inferenceRuleForDeclaration is used to type the class declaration itself

For the first two, I see that you can specify filter, matching, and inputValuesForFields.
I suppose filter acts as a guard and matching as the actual evaluated boolean expression to infer the type.
But I don't understand what is inputValuesForFields.
In comments, you wrote you don't need this one since you are doing nominal typing (as Java, C, etc I believe).
My question is: can we do duck typing, maybe with this field, as we can have in Typescript?

Here are two scenarios I want to implement using, I believe, what it looks like duck typing:

entity A {
  prop foo: string
}

entity B {
  contains bar: A
}

new B {
  contains bar = {
    prop foo = true
  }
}

In this first scenario, I have two entities and one instance of entity B. I want to automatically infer the type of the value of bar by type A and, by deduction, infer that foo = "baz" is a type error.

entity A {
  prop foo: string
}

entity B extends A {
  prop foo: string
  prop bar: boolean
}

In this second scenario, I want to check if B overrides all the attributes of A, and trigger an error otherwise.

Honestly, there are perhaps several mixed questions in this post and I'm sorry about that, this is the first time I've tried to implement a type checker in a "non-naive" way!
For me, the first scenario is what I understand of duck typing. The second one is maybe more validation than typing, but I suppose that if I am trying to implement duck typing (so typing according to the structure of an object), then we can also consider that as a typing concern.

[JohannesMeierSE]

Hello @theogiraudet,

the short answer is, that Typir does not yet support duck typing (I call it "structurally typed classes"), but it is on our roadmap (#45).

Some more detailed answers:

• inferenceRuleForConstructor is used to type an instantiation, such as Class()

yes

• inferenceRuleForReference is used when the class is used as a type, for instance in nested: NestedClass

yes

• inferenceRuleForFieldAccess is used when a property is accessed and it is not a method call, for instance x.a

yes, we could call it "member access" as well

• According to the name, I suppose that inferenceRuleForDeclaration is used to type the class declaration itself

Yes, that is intended for cases, where declarations are used as values, like var myVarHasAClassDeclarationAsInitialValue = class MyClass { ... };.

That is the current state and understanding. However, I am reworking the API for inference rules at the moment regarding ...

• the look-up of inference rules for improved performance
• the number of supported inference rules (for different use cases)
• the use of generics in TypeScript to make their configurations type-safe

With other words: Breaking changes will occur here in following versions of Typir.

For the first two, I see that you can specify filter, matching, and inputValuesForFields.
I suppose filter acts as a guard and matching as the actual evaluated boolean expression to infer the type.
But I don't understand what is inputValuesForFields.
In comments, you wrote you don't need this one since you are doing nominal typing (as Java, C, etc I believe).
My question is: can we do duck typing, maybe with this field, as we can have in Typescript?

Your understanding is great! And I should add more comments here (and yes, we plan to provide some rough documentation for v0.2 as well 🙂):

• Beyond the filtering purpose of filter, it works as a TypeScript-type guard as well: After ensuring that the current language node has a certain TypeScript type, you can count on this TypeScript type when writing your code for matching and inputValuesForFields: You don't need to do the filtering and the TypeScript type checks again!
• inputValuesForFields is required for duck typing, since you need to look at the fields and their types/values to determine the resulting ClassType, e.g. for type MyType1 = { prop1: number; prop2: boolean; }; in TypeScript. If you write type MyType2 = { prop1: number; prop2: boolean; }; later, Typir needs to assign the same ClassType instance to both declarations! But this is not yet implemented. (It is even harder, since you might use structurally typed classes inside each other in a circular manner! In such cases, the names "MyType1" and "MyType" get a relevance ...) Beyond that, we plan to separate the implementations for nominally typed classes and for structurally typed classes.

Looking at the written program is often not enough to see, whether classes are nominally or structurally typed. Usually that is defined by the semantics of the language.

As far as I understood your scenario 1, you could do the type checking also with nominally typed classes. But yes, in both cases you want to show a validation hint to the user, that foo requires a string value and no boolean value.

In my eyes, you could validate the scenario 2 even without a type system, since you need to collect the properties of sub and super class and check, whether the sub class has a property with the same name of the super class. Or do I miss something? If you want to ensure, that the type of a sub-property is the same or a sub-type of the type of the super-property, than a type system is very helpful.

Should Typir provide a default validation for checking the conformance of sub- and super-classes? I am not sure, how different the rules for sub-classes and their properties are in practise in different languages and how much logic is reusable here.

[theogiraudet]

Thank you very much for your answer! Since I am really a newbie in this domain, I'm glad I roughly understood what is already present in the framework, thanks to the provided examples.

With other words: Breaking changes will occur here in following versions of Typir.

Yes, I'm prepared for that, as these are still very early versions! But they're already giving me an idea of how to implement type systems more declaratively.

As far as I understood your scenario 1, you could do the type checking also with nominally typed classes.

Yes, I suppose we can too. To be fair, currently, I'm not really sure how to implement that. But now I have the confirmation of the purpose of the different properties; I may have some ideas.

In my eyes, you could validate the scenario 2 even without a type system, since you need to collect the properties of sub and super class and check, whether the sub class has a property with the same name of the super class. Or do I miss something?

No, I think you are right. Sometimes, the boundary between system type and validation is unclear. When we consider the type as defined by the (inherited) structure, I suppose we can consider that as part of the typing system. But in the context of nominal type, perhaps this is more something relative to the validation?

Should Typir provide a default validation for checking the conformance of sub- and super-classes? I am not sure, how different the rules for sub-classes and their properties are in practise in different languages and how much logic is reusable here.

Yes, I totally agree with you. This may be interesting, but can this be generalized? I don't know if other type-system frameworks (e.g., in MPS) propose such features.

[JohannesMeierSE]

If you are curious how to implement type systems without a framework, have a look at this implementation of LOX. You might compare this hand-written type system with the Typir-based type system in the Typir examples.

Hints how to implement scenario 1:

• Main idea is to check the assignments (bar = ... and foo = ...) by determining the (expected) type of the left-hand side (bar, foo) and the actual type of the value/right-hand side (step 1). After that you are able to check, whether both types are the same (or whether the actual type is a sub-type of the expected type) or not (step 2).
• For step 1 (we call it "type inference"), you need to investigate the current AST node, e.g. ...
  • if it is a property of an entity, the (language) type of the property is relevant (e.g. string in case of foo)
  • if it is a language type (e.g. string), return the corresponding Typir type (which might be named "string" or different, that does not matter)
  • if it is a ..., ...
  • (Therefore it is often a good idea to implement step 1 in a recursive way.)
• For step 2 (we call it "assignability checking"), you can focus on the comparison of Typir types only. Again, several cases need to be distinguished, e.g. ...
  • primitive types and entity types are not assignable
  • If both are primitive types, they need to be the same
  • If both are entity types, the entities need to have the same name (nominal typing) or they need to have the same properties (structural typing)
  • ...

But in the context of nominal type, perhaps this is more something relative to the validation?

As far as I understood scenario 2, checking the completeness of overriding (or repeating?) the inherited properties of the super-entity in the sub-entity is independent from the question, whether entities are nominally or structurally typed, since you need to check, whether each super-property is declared in the sub-entity in any case. Therefore I recommend to implement a "usual" validation, which might use a type system to compare the types of the overridden properties.

But maybe I misunderstood the notion of "overriding properties" in your language. Is there any definition of the semantics or is the implementation of your language available?