Skip to content

[refactor] typing/predef: introduce a variant of predefined type constructors - #13460

Merged
gasche merged 3 commits into
ocaml:trunkfrom
gasche:refactor-Predef-types
Oct 4, 2024
Merged

gasche merged 3 commits into
ocaml:trunkfrom
gasche:refactor-Predef-types

Conversation

@gasche

@gasche gasche commented Sep 20, 2024

Copy link
Copy Markdown
Member

predef.ml contains the definition of all "predefined" type constructors, that are defined in the compiler rather than the standard library. Some type analyses need special cases for those predefined types, whose property often cannot be defined from their definition.

Currently the check for these special cases is done with an or-cascade of boolean checks, for example Typeopt.classify (for compilation of lazy thunks):

ocaml/typing/typeopt.ml

Lines 92 to 101 in d753ea1

| Tconstr (p, _args, _abbrev) ->
if Path.same p Predef.path_float then Float
else if Path.same p Predef.path_lazy_t then Lazy
else if Path.same p Predef.path_string
|| Path.same p Predef.path_bytes
|| Path.same p Predef.path_array
|| Path.same p Predef.path_nativeint
|| Path.same p Predef.path_int32
|| Path.same p Predef.path_int64 then Addr
else begin

This is not very robust, because no one remembers to update those analyses when new predefined types are introduced. And of course, the code I quoted above does not contain the logic one could expect for the predefined types floatarray, eff and continuation.

To make this code more robust, we add in typing/Predef a variant type of all predefined type constructors (it is split in two classes, the "abstract" type constructors and the "data" type constructors that have a datatype definition, because analyses typically only need to special-case the abstract ones). They are used just enough in the module to force people to add a new variant each time they add a predefined type.

The PR also includes a find_type_constr function to decide whether am arbitrary type constructor is predefined, and uses it to update the definition in Typeopt.classify -- which revealed the missing cases.

@gasche
gasche force-pushed the refactor-Predef-types branch from c0bfc3b to 3a01464 Compare September 20, 2024 21:01
@gasche

gasche commented Sep 26, 2024

Copy link
Copy Markdown
Member Author

I wonder who would be interested in reviewing this. It should be relatively easy to review as there are no expected behavior changes (except a slightly better analysis in Typeopt). It's about the predefined typing environment, but it's not related to type inference (so less tricky, but also doesn't teach you about that). Maybe @voodoos, @MisterDA, @Elarnon or @lthls would be interested.

@voodoos voodoos left a comment •

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

The refactoring looks sound to me and is a clear improvement. Are there other places that would benefit from using find_type_constr ?

I found a few typo / copy-pasting errors that need to be fixed.

Comment thread typing/predef.ml
Comment on lines +142 to +143
let path_of_type_constr typ =
Pident (ident_of_type_constr typ)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Since there is only one usage of this helper function (in find_type_constr) I suggest moving it closer to its call site.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

My idea is that we keep the ident_* names for compatibility, and then the generic mechanism ident_of_type_constr which logically comes right after. Similarly, we keep path_* names, and then the generic path_of_type_constr function. So the place makes sense to me. But then that would suggest making those functions public -- exposing them in the .mli, which I haven't done yet, I'm not sure why. I guess I need to decide whether I consider this a useful function to expose, and then actually expose it (same with ident_of_type_constr), or we don't care about this function, and it could be inlined away as you point out. Do you have an opinion?

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I don't have a strong opinion, and agree with the reasoning behind the current placement of the find_type_constr.

Comment thread typing/predef.ml Outdated
Comment thread typing/predef.ml
Comment thread typing/predef.ml Outdated
@gasche
gasche force-pushed the refactor-Predef-types branch from 3a01464 to 4181d5f Compare September 30, 2024 15:34
@gasche

gasche commented Sep 30, 2024

Copy link
Copy Markdown
Member Author

Thanks @voodoos, very helpful -- I made two silly mistakes and I'm glad to have gotten a careful review.

Comment thread typing/typeopt.ml
Comment thread typing/typeopt.ml
Comment thread typing/predef.ml Outdated
Type_variant (constrs, Variant_regular) in
function
| `Int -> decl0 ~immediate:Always ident_int
| `Char -> decl0 ~immediate:Always ident_char

@Octachron Octachron Oct 3, 2024 •

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

If the code factored the computation of the associated ident, it would reduce the number of location whete this association is defining while allowing to group together predefined types with similar shape:

fun type_constr ->
  let name = ident_of_type_constr in
  match type_constr with
  | `Int | `Char -> decl0 ~immediate:Always name
  | `String | `Byte | `Float -> decl0 name

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

I pushed a modified version along those lines. Let me know what you think. I keep it as a separate commit because I think it is easier to review the first version first, which kept the same structure as the previous code, and then this refactoring separately.

@gasche
gasche force-pushed the refactor-Predef-types branch from 4181d5f to 981dc38 Compare October 3, 2024 14:20
gasche added 3 commits October 3, 2024 16:21
It is useful for some type-directed analyses to special case
predefined type constructors -- see for example
{!Typeopt.classify}. Currently the only way to do it is to list all
special cases by hand, with an explicit path check. If we add more
predefined types, we typically forget to update those lists of cases,
and the new types are not properly taken into account by the analyses.

In this PR we introduce a variant type of all predefined types, so that
analyses can be defined by pattern-matching on this variant type, and will
get an exhaustivity warning if a new case is added.

(We make sure to also use the variant type internally -- in the module
itself -- so that people don't forget to extend it when they add a new
predefined type.)
Suggested-by: Florian Angeletti <florian.angeletti@inria.fr>
@gasche
gasche force-pushed the refactor-Predef-types branch from 981dc38 to 08cf5d8 Compare October 3, 2024 14:21

@Octachron Octachron left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

The refactoring is correct, I am not fully convinced that it is very useful:

  • it adds two more locations to the bureaucracy needed to add a new primitive type
  • it reduces the boilerplate coupling in one location in Predef
  • it makes possible to check if a path constructor is a known primitive type, which is is used once in this PR.

Nevertheless, the refactoring can be at least also be used in Genprintval (see 62726f0) , and being able to check for exhaustive coverage of primitive types is useful to avoid future regressions.

Thus I am approving.

@gasche

gasche commented Oct 4, 2024

Copy link
Copy Markdown
Member Author

I see with your comment that I haven't submitted upstream my in-branch commits to refactor genprintval, which would have made your change much easier. Let me send a PR for this right away.

@gasche

gasche commented Oct 4, 2024

Copy link
Copy Markdown
Member Author

Thanks for the review, merging!

@voodoos I notice now that I forgot to answer your question about which other places would benefit from this check. As @Octachron remarked, genprintval.ml is one. Otherwise git grep Predef.path suggests some places that are close call, but sometimes only handle a specific subset of predefined types. For example lambda/translprim.ml has special handling of "numeric" predefined types (when specializing comparison), debugger/eval.ml has special handling of array-like predefined types (arguably bytes were forgotten and it's a minor mistake), typing/parmatch.ml has special handling of predefined sum types, and typing/typedecl.ml has special handling of unboxable predefined types. Maybe I should consider refining my polymorphic variant to represent these cases, but for now I am happy to keep things less invasive.

My main use-case is a new type analysis in the style of typeopt, in my in-progress rebase of unboxed constructors.

@gasche
gasche merged commit 9bb7929 into ocaml:trunk Oct 4, 2024
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.

4 participants