Implicit type tag in TLA expressions

[konnov]

This PR contains a change to TlaEx. It is the core structure of the whole project, so we have to discuss the proposed solution and its impact. See the discussion below.

Apart from this change, this PR contains 130 files that import a single implicit parameter:

import at.forsyte.apalache.tla.lir.UntypedPredefs._

Unfortunately, scalafmt turned this simple change into a massive PR.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality

The problem. Having the new type checker, we have to figure out how to integrate the type information in the TLA+ expressions. The old type checker is run in the very end of the pipeline. Hence the preprocessing code does not have to care about types at all. The new type checker is run before any preprocessing, which allows us to give much better feedback to the user.

There are several issues here:

• We want to write most of the code as if TLA+ was untyped, e.g., SanyImporter should work for both typed and untyped code.
• We want to write some code as if TLA+ was typed. This is basically the code in the end of the pipeline that is implemented in the translator to SMT.
• We want to gradually transform some preprocessing code into type-aware, but we shall not do it in one hop.
• Type-unaware code should not erase types of the expressions, but it should propagate them further, without knowing how to interpret the types.

For the context, our definitions for TlaEx and its case classes looked like that before this PR:

  /**
   * An abstract TLA+ expression. Note that the class is sealed, so we allow only a limited set of values.
   */
  sealed abstract class TlaEx extends Identifiable with Serializable { ... }

  /**
   * A constant TLA+ value, which is usually a literal such as: 42, TRUE, "foo", BOOLEAN.
   */
  case class ValEx(value: TlaValue) extends TlaEx with Serializable { ... }

  /**
   * Referring by name to a variable, constant, operator, etc.
   */
  case class NameEx(name: String) extends TlaEx with Serializable { ... }

  /*
   * A let-in definition, which is part of TLA+ syntax.
   */
  case class LetInEx(body: TlaEx, decls: TlaOperDecl*) extends TlaEx with Serializable { ... }

  /**
   * Application of a built-in operator. The standard operator `TlaOper.apply` allows us
   * to apply a user-defined operator (defined with `TlaOperDecl`) or an operator that is passed via a parameter
   * (that is, `OperFormalParam`).
   */
  case class OperEx(oper: TlaOper, args: TlaEx*) extends TlaEx with Serializable { ... }

Alternative solutions. Here are the alternatives that I considered (on top of the solution proposed in this PR):

• Using a map similar to AnnotationStore. However, if we annotate every single expression, the overhead will be massive.
• Instrumenting code to produce a proxy for TlaEx that would carry the type. This solution seems to be fragile and ugly. The type-unaware code could easily erase the types.
• Inherit specialized cases classes from TlaEx, ValEx, NameEx, OperEx, and LetInEx, e.g., TypedTlaEx[T](myType: T) extends TlaEx. This would produce two parallel data structures. I am not even sure how to compose them, as OperEx receives other expressions as its arguments. Again, type-unaware code could easily erase the types.
• Use parameterized types. I do not have a clear solution here.

Proposed solution: types as implicit parameters. The most clean solution seems to be to use implicit parameters. Although we have tried to avoid implicits in Scala, it looks like the right job for them.

Below are the definitions of type tags that we introduce for annotating TLA+ expressions (see at.forsyte.apalache.tla.lir):

  /**
   * A type tag to be attached to a TLA+ language construct: an expression or a declaration.
   */
  sealed abstract class TypeTag

  /**
   * The type tag that simply indicates that the language construct is not typed.
   */
  case class Untyped() extends TypeTag

  /**
   * A type tag that carries a tag of type T, which the tag is parameterized with.
   *
   * @param myType the type that is carried by the tag
   * @tparam T the type of the tag
   */
  case class Typed[T](myType: T) extends TypeTag

  /**
   * Default settings for the untyped language layer. To use the `Untyped()` tag, import the definitions from `UntypedPredefs`.
   */
  object UntypedPredefs {
    implicit val untyped: TypeTag = Untyped()
  }

Then we introduce a type tag as an implicit parameter of TlaEx:

  /**
   * An abstract TLA+ expression. Note that the class is sealed, so we allow only a limited set of values.
   * Importantly, `TlaEx` accepts an implicit type tag.
   */
  sealed abstract class TlaEx(implicit val typeTag: TypeTag) extends Identifiable with Serializable { ... }

The case classes also carry an implicit parameter, e.g., ValEx:

  /**
   * A constant TLA+ value, which is usually a literal such as: 42, TRUE, "foo", BOOLEAN.
   * Importantly, `ValEx` accepts an implicit type tag.
   */
  case class ValEx(value: TlaValue)(implicit typeTag: TypeTag) extends TlaEx with Serializable { ... }

The cool thing about this solution is that we can introduce this change without modifying lots of code. Essentially, all users of TlaEx have to import the implicit value untyped:

import at.forsyte.apalache.tla.lir.UntypedPredefs._

(I had to extend several transformations to received an implicit parameter and pass it with implicitly.)

The pattern matching code works as before. The type-aware code can access the tag via ex.myType. The type-unaware transformations may copy the types without unpacking them. On top of that, type-aware code can work with different type systems, as Typed is parameterized. If we try to mix different type systems, the compiler will help us.

The only downside that I see is that all of us have to read the chapter on implicit parameters in Programming in Scala. But we have to understand implicits anyways, if we want to use advanced frameworks as cats.

[konnov]

@romac, you probably know Scala better than all of us. Please have a look.

[konnov]

Not so unexpectedly, Google Guice fails the integration tests. There seems to be a cure.

[shonfeder]

If the formatting is introducing a ton of noise, then could you break this into 2 PRs? 1st: reformat all the files you will touch. 2nd, once that's in add the actual feature changes here?

Since you have pulled in extra reviewers and taken the time to give such a careful explanation in the PR description, I assume this is quite subtle and deserves careful review. It would take a week or more to give a 6000+ line PR a proper review.

[konnov]

Shall I just reformat the whole codebase with make fmt-fix in a separate PR? I don't like reformatting 130 files by hand :))

[shonfeder]

Yep, makes sense to me! Thank you for taking the time to help support high quality reviews 🙏

[Kukovec]

Shall I just reformat the whole codebase with make fmt-fix in a separate PR? I don't like reformatting 130 files by hand :))

I'll just add that it's really hard to comment on file changes with PRs which include reformatting. Both the new functionality and the reformatting are part of the same commit in this case, so it's difficult to find and isolate the stuff that needs to be commented on, from the noise.

[konnov]

I am closing this PR. Let's continue the review process in #561, which has better fine-grained structure.