From 8e82d30e4d8bca88ebb61fb7036c067ac647e707 Mon Sep 17 00:00:00 2001
From: Tim Neumann <neumantm@fius.informatik.uni-stuttgart.de>
Date: Tue, 10 Oct 2023 11:11:02 +0200
Subject: [PATCH] Add some sections about the typesystem (#7)

---
 README.md     |  1 +
 typesystem.md | 77 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)
 create mode 100644 typesystem.md

diff --git a/README.md b/README.md
index 2789b7a..33541ca 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,7 @@ This repository contains some tips and tricks around JetBrains MPS, which I miss
 ## Topics
 
 - [build-language](./build-language.md)
+- [remarks on the typesystem](./typesystem.md)
 
 ### Editor
 
diff --git a/typesystem.md b/typesystem.md
new file mode 100644
index 0000000..fd1c882
--- /dev/null
+++ b/typesystem.md
@@ -0,0 +1,77 @@
+# Typesystem
+
+This file contains some remarks on the MPS typesystem.
+
+## Node whose type is set by a rule in another node
+
+Assume we have the following structure:
+
+- Interface Concept `VariableDeclaration`
+- Interface Concept `AssignmentLeftSide`
+- Concept `VariableDeclarationAssignment` implements `AssignmentLeftSide`, `VariableDeclaration`
+    - attribute(string) called `name`
+- Concept `VariableAssignment` implements `AssignmentLeftSide`
+    - reference to `VariableDeclaration` called `variable`
+- Concpet `Assignment`
+    - child(`AssignmentLeftSide`) called `leftSide`
+    - child(`Expression`) called `rightSide`
+
+Now we want to make sure the type of the left side is a supertype of the right side.
+In the case of `VariableDeclarationAssignment`, its type should also be inferred from the right side.
+
+Both can be achieved by a simple rule:
+
+```
+do {
+    infer typeof(assignment.leftSide) :>=: typeof(assignment.rightSide);
+}
+```
+
+After compiling this seems to work in the sandbox.
+
+However, there is one crucial floor:
+When trying to determine the type of a `VariableDeclarationAssignment` in isolation, the typesystem cannot infer its type because there is no typesystem rule attached to that concept.
+According to [the mps docs on typesystem dependencies], the typesystem should automatically check the parent node if the type is not concrete.
+However, in my experience this does not happen in the illustrated case (on MPS 2022.2).
+
+To fix this we need to add a typesystem rule to `VariableDeclarationAssignment`, which forces the typesystem to evaluate the rule on `Assignment`.
+This can be done with the following snippet:
+
+```
+do {
+    typeof(assignmentLeftSide.parent);
+}
+```
+
+This is also explaine in [the mps docs on typesystem dependencies]. 
+However, when I first read it, I did not understand it correctly, hence me writing this chapter. 
+
+A note on when the problem manifests:
+
+- As mentioned above the problem only occurs when the type needs to be determined in isolation
+    - In my experience that is the case when using the type (or a type which is based on that type) outside of the typesystem (e.g. for Scope Calculation)
+- According to my observation the problem does not manifest in the editor
+    - I assume in the editor the typesystem always evaluates the rules of all nodes visible within the current editor or something.
+- However the problem does manifest when running a model check (which is done on a rebuild)
+- According to [the mps docs on typesystem dependencies] it can also manifest in generators
+- It can be forced to manifest by forcing the typesystem to calculate the type in isolation (see [Getting the type of a node](#getting-the-type-of-a-node))
+
+[the mps docs on typesystem dependencies]: https://www.jetbrains.com/help/mps/typesystem.html#dependencies
+
+## Getting the type of a node
+
+To get the type of a node outside of inference rules, one can usually use the `type` operation (you need the language `jetbrains.mps.lang.typesystem`).
+This is also explained in [the mps docs on using the typesystem].
+
+However, as described in [Node whose type is set by a rule in another node](#node-whose-type-is-set-by-a-rule-in-another-node), 
+it can be the case that the type of a node differs based on whether it was calculated in isolation (e.g. during model checks or in the generator) or in a typechcking session which checked many nodes (as the one of the editor).
+
+To avoid risking to have this difference, it is possible to always force the typesystem to calculate the type in isolation:
+
+```
+node<> myType = TypecheckingFacade.getFromContext().computeIsolated({ => myNode.type; })
+```
+
+(You need the model `jetbrains.mps/typechecking@java_stub` and the language `jetbrains.mps.lang.typesystem`.)
+
+[the mps docs on using the typesystem]: https://www.jetbrains.com/help/mps/using-typesystem.html#typeoperation
\ No newline at end of file