Skip to content

[asl] maintain a type annotation for every typechecked expression#1870

Open
Roman-Manevich wants to merge 2 commits into
masterfrom
asl-910-maintain-types
Open

[asl] maintain a type annotation for every typechecked expression#1870
Roman-Manevich wants to merge 2 commits into
masterfrom
asl-910-maintain-types

Conversation

@Roman-Manevich

Copy link
Copy Markdown
Collaborator

This PR enables maintaining the type inferred for each expression during typechecking as an annotation attached to the expression. The intention is to make this available for tools built on top of aslref.

Comment thread asllib/AST.mli Outdated
Comment thread asllib/ASTUtils.ml Outdated
Comment thread asllib/ASTUtils.ml Outdated
Comment thread asllib/ASTUtils.ml Outdated
Comment thread asllib/Typing.ml Outdated
Comment thread asllib/Typing.ml Outdated
@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from a8097cc to 124b7b9 Compare June 18, 2026 12:56
@Roman-Manevich Roman-Manevich requested a review from hrutvik June 18, 2026 12:57

@HadrienRenaud HadrienRenaud left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this needs to be more carefully documented. For example one of the important thing that is not said is that none of those type informations are used for type-checking.

Another important choice made here is not to use dependent types for some constructed expressions. This needs to be justified. I can see other options:

  1. Do not put any type annotations for those.
  2. Put only integer, as is done here
  3. Use recursive values to provide full precision types for literal values (this seems dangerous to me).

Maybe this should be hidden behind a command line flag not to impact the reference interpreter.
In the long term, we should probably write a typed AST which would incorporate those informations, and document what precision is given by those.

Comment thread asllib/AST.mli Outdated
Comment thread asllib/ASTUtils.ml Outdated
Comment thread asllib/Native.ml Outdated
Comment thread asllib/Typing.ml
Comment thread asllib/ASTUtils.mli Outdated
Comment thread asllib/ASTUtils.mli Outdated
Comment thread asllib/Typing.ml Outdated
@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from 124b7b9 to df82466 Compare June 18, 2026 13:01

@hrutvik hrutvik left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we need to reduce the scope of this PR. I think it should contain only:

  • Mechanism for storing type annotations - whether the existing version or Hadrien's proposal.
  • Storing type annotations as calculated during type-checking already (i.e. wrap annotate_{expr,lexpr}, base_value)

I.e. the additional type annotations not provided by the type system, the exhaustivity checks should be removed. In future we can discuss whether we consider "missing" type annotations as truly missing (and if so whether they should be inserted post-hoc or the type system should be changed to calculate them appropriately), and how this could all be encoded into a truly typed AST.

Please let me know if you disagree.

@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from df82466 to 52ba579 Compare July 13, 2026 11:31
@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from 52ba579 to a8157e8 Compare July 13, 2026 12:24
@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from 55e915d to c1688c4 Compare July 13, 2026 14:03
@Roman-Manevich Roman-Manevich marked this pull request as ready for review July 13, 2026 14:04

@HadrienRenaud HadrienRenaud left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me, thanks @Roman-Manevich, I've just got a few improvements.

Comment thread asllib/AST.mli Outdated
Comment thread asllib/ASTUtils.ml Outdated
Comment thread asllib/AST.mli Outdated
Comment thread asllib/desugar.mli
Co-authored-by: Hadrien Renaud <hadrien.renaud2@arm.com>
@Roman-Manevich Roman-Manevich force-pushed the asl-910-maintain-types branch from c1688c4 to 37f89ee Compare July 13, 2026 18:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants