Merge pull request #1386 from informalsystems/1298/typechecking-polymorphic-types-redux

Add support for polymorphic type declarations

Author: Shon Feder

CHANGELOG.md

@@ -8,10 +8,23 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- Added polymorphic type declarations, allowing abstracting commonly used data
+  types like `Option[a]` and `Result[err, ok]`. Note that this is not yet
+  supported by `verify`. (#1298)
+
 ### Changed
+
+- The latest supported node version is now bounded at <= 20, which covers the
+  latest LTS. (#1380)
+
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Removed a dependency causing deprecation errors messages to be emitted.
+  (#1380)
+
 ### Security
 
 ## v0.18.3 -- 2024-02-08

doc/lang.md

@@ -147,31 +147,34 @@ This is the same type system as in Apalache:
 
 A type is one of the following:
 
- - Basic type: `bool`, `int`, `str`.
+- Basic type: `bool`, `int`, `str`.
 
- - Uninterpreted type or type name: `IDENTIFIER_IN_CAPS`.
+- Uninterpreted type or type name: `IDENTIFIER_IN_CAPS`.
 
- - Type variable (parameter): `a`, ..., `z`.
+- Type variable (parameter): `a`, ..., `z`.
 
- - Set: `Set[T]` for a type `T`.
+- Set: `Set[T]` for a type `T`.
 
- - List: `List[T]` for a type `T`.
+- List: `List[T]` for a type `T`.
 
- - Tuple: `(T_1, T_2, ..., T_n)` for `n >= 2` types `T_1`, ..., `T_n`.
+- Tuple: `(T_1, T_2, ..., T_n)` for `n >= 2` types `T_1`, ..., `T_n`.
 
- - Record: `{ name_1: T_1, name_2: T_2, ..., name_n: T_n }`
-    for `n >= 1` types `T_1`, ..., `T_n`.
+- Record: `{ name_1: T_1, name_2: T_2, ..., name_n: T_n }`
+  for `n >= 1` types `T_1`, ..., `T_n`.
 
- - Function: `T1 -> T2` for types `T1` and `T2`.
+- Function: `T1 -> T2` for types `T1` and `T2`.
 
- - Operator: `(T_1, ..., T_n) => R` for `n >= 0` argument types `T_1, ..., T_n`
-   and result type `R`.
+- Operator: `(T_1, ..., T_n) => R` for `n >= 0` argument types `T_1, ..., T_n`
+  and result type `R`.
 
- - Sum Types: `type T = L_1(T_1) | ... | L_n(T_n) ` for `n >= 1`, argument types
-   `T_1`, ..., `T_n`, and a type alais `T`.
+- Sum Types: `type T = L_1(T_1) | ... | L_n(T_n) ` for `n >= 1`, argument types
+  `T_1`, ..., `T_n`, and a type alais `T`.
 
- - Type in parentheses: `(T)` for a type `T`.
+- Type in parentheses: `(T)` for a type `T`.
 
+- An instance of a defined polymorphic type `T[T_1, ..., T_n]` for a defined type
+  constructor with type parameters `T[p_1, ..., p_n]` and types `T_1, ...,
+  T_n`.
 
 It is often convenient to declare a type alias. You can use `type` to define
 an alias inside a module definition. For instance:
@@ -180,6 +183,18 @@ an alias inside a module definition. For instance:
 type Temperature = int
 ```
 
+A type alias specified with type parameters defines a polymorphic type
+constructor for instances of the defined type. For instance, given
+
+```bluespec
+type Option[a] =
+  | Some(a)
+  | None
+```
+
+You can then construct concrete types such as `Option[int]` or
+`Option[List[int]]`.
+
 A type identifier can also introduce an uninterpreted type by defining a type without any constructors for values of that type:
 
 ```bluespec

examples/.scripts/run-example.sh

@@ -60,6 +60,8 @@ result () {
         printf "<sup>https://github.com/informalsystems/quint/issues/1284</sup>"
       elif [[ "$file" == "classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt" && "$cmd" =~ (test|verify) ]] ; then
         printf "<sup>https://github.com/informalsystems/quint/issues/1299</sup>"
+      elif [[ "$file" == "language-features/option.qnt" && "$cmd" == "verify" ]] ; then
+        printf "<sup>https://github.com/informalsystems/quint/issues/1391</sup>"
       fi
     fi
 }

examples/README.md

@@ -86,7 +86,7 @@ listed without any additional command line arguments.
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1391</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

examples/language-features/option.qnt

@@ -1,12 +1,26 @@
 module option {
   // A demonstration of sum types, specifying an option type.
 
-  // An option type for int values.
-  type VoteOption =
+  // A polymorphic option type
+  type Option[a] =
+    | Some(a)
     | None
-    | Some(int)
 
-  var votes: List[VoteOption]
+  // `o.optionMap(f)` is `Some(f(v))` if `o = Some(v)` or `None` of `o = None`
+  def optionMap(o: Option[a], f: a => b): Option[b] =
+    match o {
+    | Some(x) => Some(f(x))
+    | None    => None
+    }
+
+  // `o.getOr(v)` is `x` or `Some(x) = o` or `v` if `o = None`
+  def getOr(o: Option[a], default: a): a =
+    match o {
+    | Some(x) => x
+    | None    => default
+    }
+
+  var votes: List[Option[int]]
   var outcome: int
 
   action init = all {
@@ -18,22 +32,31 @@ module option {
     votes' = votes.append(Some(v))
   }
 
+  action incrVote(i, n) = {
+    val vote0 = votes[i]
+    val vote1 = vote0.optionMap(x => x + n)
+    votes' = votes.replaceAt(i, vote1)
+  }
+
   action unvote(i) = all {
-    votes[i] != None,
     votes' = votes.replaceAt(i, None),
   }
 
   val sumVotes =
-    votes.foldl(0, (sum, v) => match v {
-        | Some(n) => sum + n
-        | None    => sum
-      }
-    )
+    votes.foldl(0, (sum, v) => v.getOr(0) + sum)
 
   action step = all {
     any {
-      nondet v = oneOf(Int); vote(v),
-      nondet i = oneOf(votes.indices()); unvote(i),
+      nondet v = oneOf(0.to(5)); vote(v),
+      all {
+          votes.length() > 0,
+          nondet i = oneOf(votes.indices()); unvote(i),
+      },
+      all {
+          votes.length() > 0,
+          nondet i = oneOf(votes.indices()); nondet v = oneOf(0.to(5)) incrVote(i, v),
+      }
+
     },
     outcome' = sumVotes
   }

quint/src/FreshVarGenerator.ts

@@ -16,7 +16,7 @@ export class FreshVarGenerator {
   private freshVarCounters: Map<string, number> = new Map<string, number>()
 
   freshVar(prefix: string): string {
-    const counter = this.freshVarCounters.get(prefix)! ?? 0
+    const counter = this.freshVarCounters.get(prefix) ?? 0
     this.freshVarCounters.set(prefix, counter + 1)
 
     return `${prefix}${counter}`

quint/src/types/constraintGenerator.ts

@@ -82,6 +82,8 @@ function validateArity(
 }
 
 // A visitor that collects types and constraints for a module's expressions
+//
+// NOTE: Assumes all type applications have been resolved by typeApplicationResolution first
 export class ConstraintGeneratorVisitor implements IRVisitor {
   // Inject dependency to allow manipulation in unit tests
   constructor(solvingFunction: SolvingFunctionType, table: LookupTable, types?: Map<bigint, TypeScheme>) {
@@ -95,13 +97,12 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
 
   protected types: Map<bigint, TypeScheme> = new Map<bigint, TypeScheme>()
   protected errors: Map<bigint, ErrorTree> = new Map<bigint, ErrorTree>()
+  protected freshVarGenerator: FreshVarGenerator
+  protected table: LookupTable
 
-  private solvingFunction: SolvingFunctionType
   private constraints: Constraint[] = []
-
+  private solvingFunction: SolvingFunctionType
   private builtinSignatures: Map<string, Signature> = getSignatures()
-  private table: LookupTable
-  private freshVarGenerator: FreshVarGenerator
 
   // Track location descriptions for error tree traces
   private location: string = ''
@@ -356,13 +357,11 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
         // Apply substitution to environment
         // FIXME: We have to figure out the scope of the constraints/substitutions
         // https://github.com/informalsystems/quint/issues/690
-        this.types = new Map<bigint, TypeScheme>(
-          [...this.types.entries()].map(([id, te]) => {
-            const newType = applySubstitution(this.table, subs, te.type)
-            const scheme: TypeScheme = this.quantify(newType)
-            return [id, scheme]
-          })
-        )
+        this.types.forEach((oldScheme, id) => {
+          const newType = applySubstitution(this.table, subs, oldScheme.type)
+          const newScheme: TypeScheme = this.quantify(newType)
+          this.addToResults(id, right(newScheme))
+        })
 
         return subs
       })

quint/src/types/inferrer.ts

@@ -21,12 +21,16 @@ import { TypeScheme } from './base'
 import { ConstraintGeneratorVisitor } from './constraintGenerator'
 import { solveConstraint } from './constraintSolver'
 import { simplify } from './simplification'
+import { TypeApplicationResolver } from './typeApplicationResolution'
+import { transformDeclaration, transformLookupDefinition } from '../ir/IRTransformer'
 
 export type TypeInferenceResult = [Map<bigint, ErrorTree>, Map<bigint, TypeScheme>]
 
 export class TypeInferrer extends ConstraintGeneratorVisitor {
+  private resolver: TypeApplicationResolver
   constructor(table: LookupTable, types?: Map<bigint, TypeScheme>) {
     super(solveConstraint, table, types)
+    this.resolver = new TypeApplicationResolver(this.table, this.freshVarGenerator)
   }
 
   /**
@@ -38,8 +42,18 @@ export class TypeInferrer extends ConstraintGeneratorVisitor {
    *          ids to the corresponding error for any problematic expressions.
    */
   inferTypes(declarations: QuintDeclaration[]): TypeInferenceResult {
+    // Resolve all type applications used in expressions in the lookup table
+    this.table.forEach((def, id) => {
+      // Don't resolve type definitions, since those should keep their original type variable names
+      // They are our source of truth for all resolutions
+      if (def.kind !== 'typedef') {
+        const resolvedLookupDef = transformLookupDefinition(this.resolver, def)
+        this.table.set(id, resolvedLookupDef)
+      }
+    })
     declarations.forEach(decl => {
-      walkDeclaration(this, decl)
+      const resolvedDecl = transformDeclaration(this.resolver, decl)
+      walkDeclaration(this, resolvedDecl)
     })
     const simplifiedTypes = new Map([...this.types.entries()].map(([id, t]) => [id, simplify(t)]))
     return [this.errors, simplifiedTypes]