[aslspec] type parameter refactoring and type inference by Roman-Manevich · Pull Request #1927 · herd/herdtools7

Roman-Manevich · 2026-07-22T18:31:23Z

This PR is the first in a sequence of changes to support grammar definitions in aslspec (and also to model generic helper relations). Grammar definitions need parameterized relations to define reusable rules that build the ASL AST. A follow-up PR will unify operators and relations; this PR prepares for that by making type-parameter inference reusable and completing support for parameterized types.

Parameterized types are currently not instantiated during type inference. For example:

typedef Pair[[T]] =
  | PairValue(left: T, right: T)
;

When type checking PairValue(x, y), we need to infer a concrete type for T from the types of x and y, then instantiate the variant PairValue before comparing it with the expression.

For example, if both x and y have type Int, PairValue(x, y) is inferred as Pair[[Int]], so accessing left from a Pair[[Int]] produces an Int. If x has type Int but y has type Bool, the two inferred types for T cannot be unified and aslspec reports an error.

This PR:

Represents operator type parameters explicitly in the AST.
Factors out type-parameter inference and substitution so parameterized types, and later parameterized relations, can use them.
Instantiates parameterized variants during type checking.
Detects duplicate operator type parameters.
Adds documentation and end-to-end tests.

Resolve operator type-parameter references to explicit Parameter nodes, matching parameterized typedefs. This removes the need to inject synthetic parameter types into per-operator symbol tables.

Separate type-parameter inference and substitution from operator instantiation, and describe diagnostics in terms of a generic owner. This prepares the machinery for reuse by parameterized typedefs without changing accepted specifications.

Instantiate parameterized variants while checking constructors, field access and updates, list indexing, and function application. Add successful end-to-end coverage and a diagnostic for inconsistent parameter bindings.

HadrienRenaud

In general, this looks good to me.

I struggle a bit to see the big picture, so consider maintaining a big picture explanation of what is happening.

Detects duplicate operator type parameters.

I think having a small example in the PR description would make it clearer what this is about

I think it is worth considering implementing a map_terms function on your types so that you can implement term rewriting more easily.

HadrienRenaud · 2026-07-23T08:25:29Z

+
+typing relation make_leaf(x: Int) -> (Tree[[Int]])
+{
+  prose_transition = ""


Can we make prose_transition optional?

HadrienRenaud · 2026-07-23T08:28:54Z

+      in
+      ()


Consider using |> ignore instead of let _ = ... in () to decrease indentation and simplify code.

HadrienRenaud · 2026-07-23T08:32:54Z

+            if StringSet.mem parameter seen then
+              Error.duplicate_type_parameter loc ~owner:("operator " ^ name)
+                parameter
+            else StringSet.add parameter seen)


optionally: avoid doing 2 accesses by checking physical equality:

let seen' = StringSet.add parameter seen in if seen' == seen then Error.duplicate_type_parameter loc ~owner:("operator " ^ name) parameter; seen'

HadrienRenaud · 2026-07-23T08:34:28Z

      check_well_instantiated spec term

-    let check ({ ast; id_to_defining_node } as spec) =
+    let check ({ ast; _ } as spec) =


At this point, do not deconstruct it here and use spec.ast at line 1772:

Suggested change

let check ({ ast; _ } as spec) =

let check spec =

HadrienRenaud · 2026-07-23T08:42:53Z

+(** Low-level, error-free transformations of explicit type parameters in type
+    terms. Parameter binding inference, which depends on type unification, is
+    implemented by [TypeInference.TypeParameterInference]. *)


If you could put a small example here that would help readability a lot

HadrienRenaud · 2026-07-23T09:07:19Z

        (function Some count -> Some (count + 1) | None -> Some 1)
        expanded_types

    (** [subsumed id_to_defining_node expansion_limit expanded_types sub super]


this is outdated btw

HadrienRenaud · 2026-07-23T09:09:23Z

+                increment_expansion_count typename expanded_types
+              in
+              let variants = TypeParameterOps.variants spec typename argument in
+              (not (Utils.list_is_empty variants))


why this line? can there be an empty list of variants? Why wouldn't they be subsumed then? the empty type could be understood as a subtype of anything (because it can't get any value anyway)

HadrienRenaud · 2026-07-23T09:10:36Z

            String.equal sub_typename super_typename
            && subsumed_rec spec expansion_limit expanded_types sub_term
                 super_term
+        | _, ParamType { typename; term = _, argument } ->


Can we add a negative test that is recursive and uses parameters?

HadrienRenaud · 2026-07-23T09:22:12Z

+        containing [variant]. Labelled variants are found through their label;
+        record variants are found through one of their globally unique fields.
+    *)
+    let containing_type_for_variant spec { TypeVariant.term; _ } =


If I'm reading this correctly, the only usage of containing_type_for_variant has an assert false if containing_type_for_variant return None.
Consider moving this assert false up the chain, making containing_type_for_variant return a 'a instead of a 'a option.
Benefits are simplifying the code , make it more succinct, and simplify debugging (multiple assert false give you more information when one of them is hit).

HadrienRenaud · 2026-07-23T09:27:32Z

+      match term with
+      | Term.Record { fields = { Term.name; _ } :: _; _ } ->
+          StringMap.find_opt name spec.field_to_containing_record
+          |> Option.map (fun { containing_type; _ } -> containing_type)
+      | Term.Label { label } | Term.Tuple { label_opt = Some label; _ } -> (
+          match StringMap.find_opt label spec.variant_id_to_containing_type with
+          | Some type_name -> (
+              match StringMap.find_opt type_name spec.id_to_defining_node with
+              | Some (Node_Type type_def) -> Some type_def
+              | _ -> None)
+          | None -> None)
+      | Term.Parameter _ | Term.TypeOperator _ | Term.ParamType _
+      | Term.Tuple { label_opt = None; _ }
+      | Term.Record { fields = []; _ }
+      | Term.ConstantsSet _ | Term.Function _ ->
+          None


Suggestion above:

Suggested change

match term with

| Term.Record { fields = { Term.name; _ } :: _; _ } ->

StringMap.find_opt name spec.field_to_containing_record

|> Option.map (fun { containing_type; _ } -> containing_type)

| Term.Label { label } | Term.Tuple { label_opt = Some label; _ } -> (

match StringMap.find_opt label spec.variant_id_to_containing_type with

| Some type_name -> (

match StringMap.find_opt type_name spec.id_to_defining_node with

| Some (Node_Type type_def) -> Some type_def

| _ -> None)

| None -> None)

| Term.Parameter _ | Term.TypeOperator _ | Term.ParamType _

| Term.Tuple { label_opt = None; _ }

| Term.Record { fields = []; _ }

| Term.ConstantsSet _ | Term.Function _ ->

None

match term with

| Term.Record { fields = { Term.name; _ } :: _; _ } ->

let { containing_type; _ } =

StringMap.find name spec.field_to_containing

in

containing_type

| Term.Label { label } | Term.Tuple { label_opt = Some label; _ } -> (

let type_name =

StringMap.find label spec.variant_id_to_containing_type

in

match StringMap.find type_name spec.id_to_defining_node with

| Node_Type type_def -> type_def

| _ -> assert false)

| Term.Parameter _ | Term.TypeOperator _ | Term.ParamType _

| Term.Tuple { label_opt = None; _ }

| Term.Record { fields = []; _ }

| Term.ConstantsSet _ | Term.Function _ ->

assert false

Roman-Manevich added 3 commits July 22, 2026 18:01

[aslspec] Represent operator type parameters explicitly

3be8124

Resolve operator type-parameter references to explicit Parameter nodes, matching parameterized typedefs. This removes the need to inject synthetic parameter types into per-operator symbol tables.

[aslspec] Generalize type parameter inference

04124b3

Separate type-parameter inference and substitution from operator instantiation, and describe diagnostics in terms of a generic owner. This prepares the machinery for reuse by parameterized typedefs without changing accepted specifications.

[aslspec] Infer parameterized type instantiations

336b76e

Instantiate parameterized variants while checking constructors, field access and updates, list indexing, and function application. Add successful end-to-end coverage and a diagnostic for inconsistent parameter bindings.

Roman-Manevich marked this pull request as ready for review July 22, 2026 18:41

Roman-Manevich requested review from HadrienRenaud and hrutvik July 22, 2026 18:41

HadrienRenaud reviewed Jul 23, 2026

View reviewed changes

Navigation Menu

Uh oh!

[aslspec] type parameter refactoring and type inference - #1927

[aslspec] type parameter refactoring and type inference#1927
Roman-Manevich wants to merge 3 commits into
masterfrom
aslspec-type-parameter-inference

Roman-Manevich commented Jul 22, 2026 •

edited

Loading

Uh oh!

HadrienRenaud left a comment

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

HadrienRenaud Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

Roman-Manevich commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

HadrienRenaud left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Roman-Manevich commented Jul 22, 2026 •

edited

Loading