Introduce new syntax for type aliases #1977

konnov · 2022-07-13T17:27:33Z

Closes #1843. As we have found, the users are confused by missing type aliases, which default to uninterpreted types. This PR introduces new syntax for type aliases:

\* @typeAlias: newAlias = Set(Int);
\* @type: Set($newAlias);
Foo == { 0 }

The benefit of having special syntax for type aliases and references is that the type checker can now complain about missing type aliases. Compare TestAliasOld.tla to TestAliasNew.tla and TestAliasNewMissing.tla.

The documentation is postponed for a follow-up 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
Entries added to ./unreleased/ for any new functionality

codecov-commenter · 2022-07-13T17:43:10Z

Codecov Report

Merging #1977 (e8a96a1) into unstable (80a82c1) will increase coverage by 0.02%.
The diff coverage is 92.10%.

@@             Coverage Diff              @@
##           unstable    #1977      +/-   ##
============================================
+ Coverage     77.81%   77.84%   +0.02%     
============================================
  Files           418      418              
  Lines         12789    12813      +24     
  Branches        566      603      +37     
============================================
+ Hits           9952     9974      +22     
- Misses         2837     2839       +2

Impacted Files	Coverage Δ
...forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala	`94.95% <ø> (ø)`
...n/scala/at/forsyte/apalache/tla/lir/TlaType1.scala	`83.15% <75.00%> (+0.01%)`	⬆️
...ache/tla/typecheck/etc/TypeAliasSubstitution.scala	`60.97% <90.90%> (ø)`
...lache/io/typecheck/parser/DefaultType1Parser.scala	`94.89% <100.00%> (-0.56%)`	⬇️
...syte/apalache/io/typecheck/parser/Type1Lexer.scala	`95.65% <100.00%> (+0.09%)`	⬆️
.../forsyte/apalache/io/typecheck/parser/tokens.scala	`93.10% <100.00%> (+0.24%)`	⬆️
...rsyte/apalache/tla/typecheck/TypeCheckerTool.scala	`92.68% <100.00%> (+0.37%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 80a82c1...e8a96a1. Read the comment docs.

shonfeder

One question posed about the limit on cases.

I also have a proposal for an alternative solution: why not require users declare uninterpreted types up front with an annotation? It seems that this be a more robust solution, as it would also prevent typos in uninterpreted types.

As an aside, I happen to think dollar signs are ugly 😝

shonfeder · 2022-07-13T23:23:40Z

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala

+              val (alias, assignedType) = parseTypeAlias(decl.name, text)
+              if (!ConstT1.isAliasReference(alias)) {
+                val msg =
+                  s"Operator ${decl.name}: Deprecated syntax in type alias $alias. Use camlCase of Type System 1.2."


Why do we have to enforce anything about the case of the letters if we are requiring a $ to reference the alias? Shouldn't the case be irrelevant then?

In principle, yes, but we still have the all-caps syntax for old aliases and uninterpreted types. I just wanted some disambiguation here.

fwiw, I don't see the value in applying this unneeded constraint.

konnov · 2022-07-14T08:14:55Z

One question posed about the limit on cases.

I also have a proposal for an alternative solution: why not require users declare uninterpreted types up front with an annotation? It seems that this be a more robust solution, as it would also prevent typos in uninterpreted types.

As an aside, I happen to think dollar signs are ugly 😝

I agree and I also do not find dollar signs aesthetically pleasing. If we had better control over the language, we could make types better integrated into the syntax. If we start requiring type declarations for uninterpreted types, this will make life of specification writers even harder.

konnov · 2022-07-14T08:19:38Z

One question posed about the limit on cases.

@shonfeder, I do not see a question. Is it lost in the Github review process? :)

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala

Kukovec · 2022-07-14T08:23:58Z

tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/DefaultType1Parser.scala

+  // old ALIAS_SYNTAX, or newSyntaxInCamelCase
+  private def oldOrNewAlias: Parser[ConstT1] = {


It looks like we still match the old alias syntax and just show a deprecation message instead of failing. Shouldn't we just pick 1 syntax and go with that, instead of some pseudo backwards-compatibility? We're not even in alpha, we shouldn't be beholden to old syntax.

Yes, we will keep the old syntax for the same transition period, as we do for the old records. We should give the users a bit of time to switch to the new syntax.

Why though? They're going to have to change it eventually anyway. It'll be just as much of an issue for users then as it would be now, except we get the added downside of maintenance burden in the meantime.

Because we don't want angry users? 🤷‍♂️

Why would they be angry now, but not in, say, 1 month when this would become the new standard?

They still can get angry after 1 month, but we would give them the chance to transition without ruining their process all of a sudden.

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeAliasSubstitution.scala

Kukovec · 2022-07-14T08:38:00Z

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeAliasSubstitution.scala

+            // The behavior for an OLD_TYPE_ALIAS is to understand it as an uninterpreted type.
+            // Since in the old syntax, we cannot distinguish between uninterpreted types and type aliases,
+            // we cannot do much here.


I wrote the previous comment (#1977 (comment)), and up until this line it seemed to be the case, from reading the docs, that we support both syntaxes. In particular https://github.com/informalsystems/apalache/blob/ecd5b7188c211b8b7e3f6440f7ecefda4daa420d/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeAliasSubstitution.scala#L8
mentions ENTRY or $entryInCamlCase.

But these lines imply that we don't support old aliases anymore. This is a bit confusing and it should be much clearer whether we support old aliases or not (and in what way). Semantically, I don't think treating caps types as uninterpreted means that we support "old aliases" (and the Scala variable names should reflect this).

What I meant by "we cannot do much here" is that we cannot detect an error. I think I will fix the comment.

Kukovec · 2022-07-14T08:40:03Z

tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestTypeCheckerTool.scala

+    // (e.g., it failed in Intellij Idea). Now we are just reading it from $APALACHE_HOME/tla-types/src/test/resources.
+    // This is consistent with the behavior of SanyImporter when it is run in tests.
+    System.getenv("APALACHE_HOME") match {
+      // Warn if environment variable APALACHE_HOME is not set
+      case null =>
+        logger.error("Not running from fat JAR and APALACHE_HOME is not set.")
+        logger.error("Set APALACHE_HOME to a directory where Apalache has been checked out.")
+        throw new IllegalStateException("Missing APALACHE_HOME to run the tests")
+
+      case apalacheHome: String =>
+        Source.fromFile(s"$apalacheHome/tla-types/src/test/resources/$name.tla")
+    }


I get complaints about unrelated changes added into PRs, so I'm going to start complaining about unrelated changes added to other people's PRs. Consider creating a separate issue for this and factoring this into a separate PR.

It is related, as I had to run the tests, and they were not runnable in Idea, as we had two different solutions to dealing with resources.

Kukovec · 2022-07-14T08:41:40Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala

+/**
+ * A companion object for [[ConstT1]].
+ */
+object ConstT1 {


Not something I necessarily want now, but consider combining this class with ModelValueHandler (more accurately, moving methods from that class to here).
We don't want 2 unrelated classes handling utility for uninterpreted literals.

Fixing the regular expression. I will open an issue about ModelValueHandler.

Kukovec · 2022-07-14T08:43:19Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala

+   *   true iff the type name represents an uninterpreted type.
+   */
+  def isUninterpreted(name: String): Boolean = {
+    name.forall(c => c.isUpper || c.isDigit || c == '_')


Why don't you use regex here?

Also, this is incorrect, because you can start your value name with [0-9] and the forall test would pass.
The regex is [A-Z_][A-Z0-9_] (see ModelValueHandler.matchRegex)

I have opened a follow-up issue: #1992 (comment)

shonfeder · 2022-07-14T11:43:02Z

One question posed about the limit on cases.

@shonfeder, I do not see a question. Is it lost in the Github review process? :)

You answered my question already! Thanks :)

shonfeder

Outside of my general reservations and general agreement with Jure's suggestions, LGTM.

tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/DefaultType1Parser.scala

shonfeder · 2022-07-14T12:13:00Z

If we start requiring type declarations for uninterpreted types, this will make life of specification writers even harder.

I don't not see how requiring a single line delcaring an uninterpreted type makes the life of a specification writer than requiring them to prefix every instance of an alias with $. The latter seems more onerous.

Moreover, the slight inconvenience of adding a single line declaration seems more than compensated by helping spec writers ensure they don't introduce spurious errors with typos in their uninterpreted types.

Perhaps I am missing something?

konnov · 2022-07-15T09:14:10Z

I don't not see how requiring a single line delcaring an uninterpreted type makes the life of a specification writer than requiring them to prefix every instance of an alias with $. The latter seems more onerous.

The main problem is that annotations in comments are still fragile, so I am trying to minimize the number of annotations in general. The reason for having $ is that the type checker can now complain about a missing type alias. With the current implementation, the type checker silently assumes that the user meant an uninterpreted type. So yes, the user can make an error in a reference to a type alias, or completely forget to write $, but in this case they will get a type checker error. This is the most critical point for me here.

konnov · 2022-07-15T09:17:57Z

Moreover, the slight inconvenience of adding a single line declaration seems more than compensated by helping spec writers ensure they don't introduce spurious errors with typos in their uninterpreted types.

The way modules work in TLA+, this will introduce more confusion than it would help. You will have to be careful about explicitly declaring an uninterpreted type across different modules. We are already doing that with type aliases, so it is not impossible. However, I do not see any value of doing that for uninterpreted types. If you make a typo in the name of an uninterpreted type, you will get a type checking error.

konnov · 2022-07-15T09:27:19Z

Just to clarify the context here. We have four kinds of identifiers in the type grammar:

Uninterpreted types that are currently written in ALL_CAPS.
Variable names that match the regex a[0-9]+|[a-z].
Aliases, which currently coincide with uninterpreted types.
Type constructors such as Set and Seq.

So my proposal here is to disambiguate aliases by:

Enforcing caml case starting with a small letter in their names, so they do not conflict with uninterpreted types and type constructors.
Refer to type aliases via $, so this syntax does not conflict with type variables.

I also do not like the dollar syntax. However, this syntax is not really surprising. Type aliases are simply substituted in the type checker, they are not types of their own.

Co-authored-by: Shon Feder <[email protected]> Co-authored-by: Kukovec <[email protected]>

konnov · 2022-07-18T09:54:56Z

@Kukovec I think I took all of your comments into account. Would you like to approve it now?

thpani · 2022-07-18T09:55:25Z

tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeAliasSubstitution.scala

+ * meant to replace constant types, e.g., ENTRY or $entryInCamlCase, with a concrete type, whereas `Substitution`
+ * replaces variables. We use `ConstSubstitution` to rewrite type aliases.


Also need to rename the class here :)
(Unfortunately I can't mark the unchanged line above to make a suggestion)

* A substitution from constant names to types. It is very similar to [[Substitution]]. However, * [[TypeAliasSubstitution]] is meant to replace constant types, e.g., ENTRY or $entryInCamlCase, with a concrete type, * whereas [[Substitution]] replaces variables. We use [[TypeAliasSubstitution]]` to rewrite type aliases.

thpani · 2022-07-18T09:59:17Z

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala

+ * <p>An uninterpreted type constant such as PROC_NAME.</p>
+ *
+ * <p>Inside the type checker, this class may also represent references to type aliases. Do not use this feature outside
+ * of the type checker.</p>


I think Scaladoc infers the markup here

Suggested change

* <p>An uninterpreted type constant such as PROC_NAME.</p>

*

* <p>Inside the type checker, this class may also represent references to type aliases. Do not use this feature outside

* of the type checker.</p>

* An uninterpreted type constant such as PROC_NAME.

*

* Inside the type checker, this class may also represent references to type aliases. Do not use this feature outside

* of the type checker.

konnov · 2022-07-18T14:04:15Z

I think I have implemented all the comments. Thanks for the reviews! Will merge it now.

konnov added 6 commits July 12, 2022 21:53

extend the syntax for type aliases

dec803f

support all lower case in type aliases too

fe10983

update two tests to use the new alias syntax

962b3ec

instead of cwd, use APALACHE_HOME, as in SanyImporter

a8266ac

add tests for the old alias syntax and the new alias syntax

0d15232

implement new syntax for alias references

614a75c

konnov requested review from shonfeder and Kukovec as code owners July 13, 2022 17:27

add release notes

47f144c

konnov mentioned this pull request Jul 13, 2022

Document new syntax for type aliases #1978

Closed

update the type aliases in tests

9be9d2e

shonfeder reviewed Jul 13, 2022

View reviewed changes

konnov added 2 commits July 14, 2022 10:17

fix the type alias

79db8e6

Merge branch 'unstable' into ik/aliases1843

ecd5b71

Kukovec reviewed Jul 14, 2022

View reviewed changes

shonfeder approved these changes Jul 14, 2022

View reviewed changes

tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/DefaultType1Parser.scala Outdated Show resolved Hide resolved

konnov and others added 5 commits July 15, 2022 11:32

Merge branch 'unstable' into ik/aliases1843

1e7d0ba

Merge branch 'unstable' into ik/aliases1843

07b379c

Apply suggestions from code review

8b3e91f

Co-authored-by: Shon Feder <[email protected]> Co-authored-by: Kukovec <[email protected]>

fix the comments

84dd6b5

use a regex instead of a loop

89d6a36

konnov mentioned this pull request Jul 18, 2022

Refactor ModelValueHandler into ConstT1 #1992

Open

Merge branch 'unstable' into ik/aliases1843

504ef09

thpani approved these changes Jul 18, 2022

View reviewed changes

Kukovec approved these changes Jul 18, 2022

View reviewed changes

konnov added 4 commits July 18, 2022 13:12

fix a broken test case

d94082c

Merge branch 'ik/aliases1843'

b976245

fix the scaladoc a bit

d9ae6c4

Merge branch 'unstable' into ik/aliases1843

da58a6a

konnov enabled auto-merge July 18, 2022 14:04

fix a broken test

e8a96a1

konnov merged commit a86dcb7 into unstable Jul 18, 2022

shonfeder deleted the ik/aliases1843 branch July 21, 2022 21:27

This was referenced Jul 21, 2022

[release] 0.25.11 #2007

Closed

[release] 0.25.11 #2010

Closed

[release] 0.26.0 #2012

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce new syntax for type aliases #1977

Introduce new syntax for type aliases #1977

konnov commented Jul 13, 2022 •

edited

Loading

codecov-commenter commented Jul 13, 2022 •

edited

Loading

shonfeder left a comment

shonfeder Jul 13, 2022 •

edited

Loading

konnov Jul 14, 2022

shonfeder Jul 14, 2022

konnov commented Jul 14, 2022

konnov commented Jul 14, 2022

Kukovec Jul 14, 2022

konnov Jul 14, 2022

Kukovec Jul 14, 2022

konnov Jul 14, 2022

Kukovec Jul 14, 2022

konnov Jul 15, 2022

Kukovec Jul 14, 2022 •

edited

Loading

konnov Jul 18, 2022

Kukovec Jul 14, 2022

konnov Jul 14, 2022

Kukovec Jul 14, 2022

konnov Jul 18, 2022

Kukovec Jul 14, 2022

Kukovec Jul 14, 2022

konnov Jul 18, 2022

shonfeder commented Jul 14, 2022

shonfeder left a comment

shonfeder commented Jul 14, 2022

konnov commented Jul 15, 2022

konnov commented Jul 15, 2022

konnov commented Jul 15, 2022

konnov commented Jul 18, 2022

thpani Jul 18, 2022

thpani Jul 18, 2022

konnov commented Jul 18, 2022

		// old ALIAS_SYNTAX, or newSyntaxInCamelCase
		private def oldOrNewAlias: Parser[ConstT1] = {

		* meant to replace constant types, e.g., ENTRY or $entryInCamlCase, with a concrete type, whereas `Substitution`
		* replaces variables. We use `ConstSubstitution` to rewrite type aliases.

Introduce new syntax for type aliases #1977

Introduce new syntax for type aliases #1977

Conversation

konnov commented Jul 13, 2022 • edited Loading

codecov-commenter commented Jul 13, 2022 • edited Loading

Codecov Report

shonfeder left a comment

Choose a reason for hiding this comment

shonfeder Jul 13, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented Jul 14, 2022

konnov commented Jul 14, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Kukovec Jul 14, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder commented Jul 14, 2022

shonfeder left a comment

Choose a reason for hiding this comment

shonfeder commented Jul 14, 2022

konnov commented Jul 15, 2022

konnov commented Jul 15, 2022

konnov commented Jul 15, 2022

konnov commented Jul 18, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov commented Jul 18, 2022

konnov commented Jul 13, 2022 •

edited

Loading

codecov-commenter commented Jul 13, 2022 •

edited

Loading

shonfeder Jul 13, 2022 •

edited

Loading

Kukovec Jul 14, 2022 •

edited

Loading