Refactor `Typecore.type_application` by voodoos · Pull Request #13612 · ocaml/ocaml

voodoos · 2024-11-14T15:35:03Z

This PR proposes a refactor of Typecore.type_application.
This work was originally done by @lpw25 in Jane Street's fork of the compiler with extensions. Jane Street has asked for help from Tarides to upstream these changes.

This PR introduces a more descriptive type for arguments of a function application:

type expression_desc =
  | ...
  | Texp_apply of expression * (arg_label * apply_arg) list

and apply_arg = (expression, unit) arg_or_omitted

and ('a, 'b) arg_or_omitted =
  | Arg of 'a
  | Omitted of 'b

These were formerly represented with the type expression option.

The typing of applications is now clearly split in two phases: first collect_apply_args maps over the arguments, classify them and collect additional information. Then type_apply_arg and type_omitted_parameters perform the actual typing.

The classification was previously done by imperatively filling lists such as eliminated_optional_arguments and omitted_parameters. Now it uses the type parameters of arg_or_omitted to store additional information and specific type constructors are introduced for these cases:

type untyped_apply_arg =
  | Known_arg of
      { sarg : Parsetree.expression;
        ty_arg : type_expr;
        ty_arg0 : type_expr;
        mode_arg : Alloc_mode.t;
        wrapped_in_some : bool; }
  | Unknown_arg of
      { sarg : Parsetree.expression;
        ty_arg : type_expr;
        mode_arg : Alloc_mode.t; }
  | Eliminated_optional_arg of
      { mode_fun: Alloc_mode.t;
        ty_arg : type_expr;
        mode_arg : Alloc_mode.t;
        level: int;}

type untyped_omitted_param =
  { mode_fun: Alloc_mode.t;
    ty_arg : type_expr;
    mode_arg : Alloc_mode.t;
    level: int; }

(untyped_apply_arg, untyped_omitted_param) arg_or_omitted

Thus, the flow for typing an application can now be summarized with these three functions:

collect_apply_args :
  ... (arg_label * expression) list ->
  ... * (untyped_apply_arg, untyped_omitted_param) arg_or_omitted list

type_apply_arg :
  ... (untyped_apply_arg, untyped_omitted_param) arg_or_omitted ->
  ... * (Typedtree.expression, untyped_omitted_param) arg_or_omitted

type_omitted_parameters :
  ... (Typedtree.expression, untyped_omitted_param) arg_or_omitted list ->
  ... * (Typedtree.expression, unit) arg_or_omitted list

I was not familiar with the typing process of function application before doing this work but my impression is that these changes do make the code clearer and more robust.

cc @OlivierNicole @goldfirere

The typing of applications is now decomposed in two phases: collecting the arguments and typing them. Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

goldfirere · 2024-11-15T13:17:52Z

Thanks, @voodoos, for posting this!

Suggested-by: Antonin Décimo <antonin@tarides.com>

gasche

(A very shallow first review on the small part of the change that is not within typecore.ml, which the github UI hides by default.)

gasche

I tried to have a look at the diff as a neophyte, and started by trying to piece out a map from the new code (which comes first in the github diff) to the old code. If I wanted to review this, I guess that I would try to check that the newly-located code is indeed equivalent to the previous code, and separately try to read the new body of the type_application function and compare with the previous one.

gasche · 2024-11-20T14:43:30Z

+    level: int;
+  }
+
+let remaining_function_type ty_ret rev_args =


For reviewers: this corresponds to result_type at the beginning of type_application in the trunk implementation, except that it takes the full (rev)list of apply_arg, not just omitted and eliminated arguments.

I find this function particularly confusing, as it mixes two steps.
The original result_type was just rebuilding a type, given labels and levels.
It was called in two distinct places:

in the default case of type_unknown_arg, in order to generate an error message. In that case we need to pretend that omitted arguments are still there, since the error may be that we misspelled a label so that it ended up being omitted.

in type_unknown_args, in order to generate the final type of the function application. In that case omitted arguments are of course omitted.

But this version is actually specialized for the first occurrence, which explains why it handles omitted arguments as kept.
At least it should be renamed to remaining_function_type_for_error.

Looking at code, I also wonder if your choice of types is ideal.
Would it not be better to reserve Arg for actual arguments, and put erased arguments on the Omitted side.

type untyped_omitted_param = { eliminated : bool ; (* true for eliminated optional arguments, false otherwise *) ty_arg : type_expr; level: int; }

Since this type is internal to type_application, there is no external impact, and it could clarify the code.

Would it not be better to reserve Arg for actual arguments, and put erased arguments on the Omitted side.

It is much more important to distinguish omitted parameters -- which cause a closure to be created rather than a function to be called -- from ordinary arguments. Whist untyped_omitted_param is local to type_application the use of the arg_or_omitted is not: the distinction between actual arguments and omitted parameters is preserved all the way through to translcore. Getting this distinction clear and correct was a key motivation for this patch (it matters a lot for our work on modes like local).

Indeed, arg_or_omitted is kept. But untyped_apply_arg is not.
And I am still under the impression that, until they get typed, the code would be simpler with eliminated optional arguments on the Omitted side. In particular, in this function the distinction between omitted arguments that are eliminated and those that are kept does not matter yet. Of course, you need to move them to the Arg side eventually, when you create the concrete argument. This can be done either in type_apply_arg or type_omitted_parameters. I would actually prefer the latter, and it would even give you a justification for the name.

Having the meaning of Omitted be inconsistent between different parts of the code just makes it much harder to understand for no obvious benefit. Eliminated optional parameters are fundamentally not omitted arguments and it is confusing to label them as such.

But they are omitted. Seeing them otherwise makes this function hard to understand.
Anyway, I don't want to make this a requirement (this is why I approved).
This function still must be renamed: if you see eliminated optional parameters as not omitted, they clearly cannot be part of the remaining function type.

My point of view is that type_application is converting some omitted arguments into defaults, the point at which it is done in the function being a question of design choice. The benefit of doing it at the end is that the intermediate representation becomes closer to the source syntax, which for instance makes reasoning about errors easier.

gasche · 2024-11-20T14:58:10Z

+  in
+  loop ty_fun ty_fun0 [] sargs
+
+let type_omitted_parameters ty_ret args =


Still trying to map the new code to the old code: it is unclear to me where this function comes from, it appears to be new. There seems to be some redudancy with the function remaining_function_type above, I am not sure why this is.

Part of the code for this function actually comes from the result_type auxiliary function defined at the beginning of trunk's type_application function and which is called over the list of !omitted_parameters.

But result_type was already moved into remaining_function_type above. Why have the same Tarrow-building logic in two different places?

For me the difference is that :

remaining_function_type of (f : ?x:int -> y:bool -> float -> t) 3. is ?x:int -> y:bool -> t because ?x will go in the Arg (Eliminated_optional_arg _) case.

type_omitted_parameters of (f : ?x:int -> y:bool -> float -> t) 3. is y:bool -> t
The first case is used for error messages when the second is the resulting type after eta-expanding ommited labelled arguments.
It might be nice to put both function together with a comment to explain why they are different.

We could merge the two function by adding an ?reinject_eliminated_optional_arg arguments to type_omitted_parameters and discarding the argument part in the error path that was using remaining_function_type.

I also think that it could be nice the rename the function to return_function_type or return_type_with_omitted_parameters to better convey the idea that there is no typing going on in the function type_omitted_parameters.

The reason it is called type_omitted_parameters is that it maps over the omitted parameters turning them from their untyped form -- untyped_omitted_param -- into their typed form. Unfortunately, in this patch the typed form is just unit so it looks a bit weird. Our work on both modes and kinds requires us to put more information into the typed form, so that we have a type omitted_param in Typedtree and that is what is produced for the omitted parameters here.

I do think this is still to right way to think about this function however, so I'd prefer if this view could be preserved in the name.

It is true than this function is really a fold_map rather than a map -- it also computes the result_type as it goes -- and this isn't reflected in the current name. It probably would be better if the name included that detail. How about something like type_omitted_parameters_and_build_result_type?

Here I really think that this PR should use a name that corresponds to what is done, not what will be done in the future. You can easily change this name when the meaning changes: this function is used only once.

My understanding is that it's not just about a change in the future, it about reducing the diff between upstream and Jane Street's existing fork of the type-checker codebase. I think that it's worth accommodating this need if we can at reasonable cost, to make such upstreaming easier (and worthy) in the future. Maybe we could find a name that would be acceptable in both versions, for example handle_omittted_parameters_and_build_result_type?

My point was actually slightly stronger than just about keeping the diff small. I was also arguing that semantically this is the place where we "type" the omitted arguments: taking them from their representation in the parsetree to their representation in the typedtree. Just because the representation in the typedtree is () doesn't mean it is the wrong way to picture this function.

Still, I would settle for handle_omitted_parameters_... if people object to using the word type_ for this.

If you want to call it that way, that's fine.
For a preciser picture, we would need to see the real code.

gasche · 2024-11-21T08:51:02Z

(Note: the fact that the change comes in one big commit makes it harder to review than if it was split in a sequence of smaller changes.)

samsa1 · 2024-11-26T14:28:00Z

+        let may_warn loc w =
+          if not !warned && !Clflags.principal && lv <> generic_level
+          then begin
+            warned := true;
+            Location.prerr_warning loc w
+          end
+        in


If we add lv as a parameter of this function we can move it outside of the loop function. Thus closed to the definition of warned that could even become local to this function definition.

But it might be better to minimize the diff and leave such rewriting for another time

I am not sure it would be correct. This function iterates on the spine of the function type, and the level changes along it.

goldfirere · 2024-11-27T20:06:24Z

I offered to help out with review here. What's the current status of review? How can I be of service?

gasche · 2024-12-04T17:21:27Z

@voodoos, @sama1, @Octachron and myself reviewed this commit together. We pushed a string of changes as we went along. We are now collectively convinced that the new behavior is the same as the previous one.

(@samsa1 said he would look at the location we use in error messages for eliminated optional arguments)

gasche

Approved in principle.

@samsa1 is wondering about error message locations, and @voodoos should do a pass on the review comments and see if minor changes need to be applied. (I need to rebase to remove the fixup! commit.)

gasche · 2024-12-04T17:22:23Z

  (Mark Shinwell, review by Vincent Laviron)

+- #13612: Refactor `type_application`
+  (Ulysse Gérard, Leo White, review by Antonin Décimo, ...)


(This needs an update.)

samsa1 · 2024-12-05T06:27:22Z

I managed to convince myself that there was no problem with location.
I approve of the changes on this PR.

For the record :

ocaml/typing/typecore.ml

Line 5479 in 061adb7

(sargs, Some (eliminate_optional_arg (), Some sarg.pexp_loc))

and

ocaml/typing/typecore.ml

Line 5499 in 061adb7

Some (eliminate_optional_arg (), None)

Where incoherent between classic and non-classic mode. This could lead to an difference in error messages. This PR chooses the approach of not storing the location (which is understandable because there are no corresponding arguments). However this could have impacted locations in error messages.

However I found only one usage of the location stored in that list :

ocaml/typing/typecore.ml

Lines 5355 to 5382 in 061adb7

    
                     let ty_fun = match td with Tarrow _ -> newty td | _ -> ty_fun in 
        
                     let ty_res = 
        
                       result_type (!omitted_parameters @ !eliminated_optional_arguments) 
        
                         ty_fun 
        
                     in 
        
                     match get_desc ty_res with 
        
                     | Tarrow _ -> 
        
                         if !Clflags.classic || not (has_label lbl ty_fun) then 
        
                           raise (Error(sarg.pexp_loc, env, 
        
                                        Apply_wrong_label(lbl, ty_res, false))) 
        
                         else 
        
                           raise (Error(funct.exp_loc, env, Incoherent_label_order)) 
        
                     | _ -> 
        
                         let previous_arg_loc = 
        
                           (* [typed_args] is the arguments typed until now, in reverse 
        
                              order of appearance. Not all arguments have a location 
        
                              attached (eg. an optional argument that is not passed). *) 
        
                           typed_args 
        
                           |> List.find_map 
        
                               (function (_, Some (_, loc)) -> loc | _ -> None) 
        
                           |> Option.value ~default:funct.exp_loc 
        
                         in 
        
                         raise(Error(funct.exp_loc, env, Apply_non_function { 
        
                             funct; 
        
                             func_ty = expand_head env funct.exp_type; 
        
                             res_ty = expand_head env ty_res; 
        
                             previous_arg_loc; 
        
                             extra_arg_loc = sarg.pexp_loc; }))

However because of the match on the result_type we can never go into the second case of the match if we had ommited an optionnal argument before.
Thus the question of which location is stored for the eliminated optional argument is irrelevant because it is never used.

Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

…message Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

… version (This might make a difference when reconstructed omitted parameters that were deconstructed from a generic type.) Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

gasche · 2024-12-05T07:46:15Z

( @goldfirere sorry for the lack of responsiveness here; last week was my "avoid looking at github/ocaml notifications" week and I missed your question. I think that we can move to merge this quickly, and maybe spend the coordination effort on the review of polymorphic arguments. )

garrigue

I did not check all the details, but the approach seems fine.
Being more functional is always good, but the main goal seems here to be the separation between argument selection and typing.
I am a bit curious of how all that interacts with Merlin (I suppose that you already checked).
My comments are mostly stylistic, but I think it matters here.
Particularly, the two functions that replace result_type should be at least renamed and their roles explained.

garrigue · 2024-12-13T06:10:01Z

+    level: int;
+  }
+
+let remaining_function_type ty_ret rev_args =


I find this function particularly confusing, as it mixes two steps.
The original result_type was just rebuilding a type, given labels and levels.
It was called in two distinct places:

in the default case of type_unknown_arg, in order to generate an error message. In that case we need to pretend that omitted arguments are still there, since the error may be that we misspelled a label so that it ended up being omitted.

in type_unknown_args, in order to generate the final type of the function application. In that case omitted arguments are of course omitted.

But this version is actually specialized for the first occurrence, which explains why it handles omitted arguments as kept.
At least it should be renamed to remaining_function_type_for_error.

Looking at code, I also wonder if your choice of types is ideal.
Would it not be better to reserve Arg for actual arguments, and put erased arguments on the Omitted side.

type untyped_omitted_param = { eliminated : bool ; (* true for eliminated optional arguments, false otherwise *) ty_arg : type_expr; level: int; }

Since this type is internal to type_application, there is no external impact, and it could clarify the code.

garrigue · 2024-12-13T06:22:52Z

+  in
+  loop ty_fun ty_fun0 [] sargs
+
+let type_omitted_parameters ty_ret args =


Indeed, this is the second usage of result_type in the original code (see my comment above).
It also builds the list of desugared arguments, so clearly the name is wrong.
Maybe build_result_type_and_arguments.

garrigue · 2024-12-13T06:24:14Z

+        let may_warn loc w =
+          if not !warned && !Clflags.principal && lv <> generic_level
+          then begin
+            warned := true;
+            Location.prerr_warning loc w
+          end
+        in


I am not sure it would be correct. This function iterates on the spine of the function type, and the level changes along it.

garrigue

I am happy with the code, just need to clarify function names.

garrigue · 2024-12-16T06:29:01Z

+    level: int;
+  }
+
+let remaining_function_type ty_ret rev_args =


Indeed, arg_or_omitted is kept. But untyped_apply_arg is not.
And I am still under the impression that, until they get typed, the code would be simpler with eliminated optional arguments on the Omitted side. In particular, in this function the distinction between omitted arguments that are eliminated and those that are kept does not matter yet. Of course, you need to move them to the Arg side eventually, when you create the concrete argument. This can be done either in type_apply_arg or type_omitted_parameters. I would actually prefer the latter, and it would even give you a justification for the name.

garrigue · 2024-12-16T06:33:34Z

+  in
+  loop ty_fun ty_fun0 [] sargs
+
+let type_omitted_parameters ty_ret args =


Here I really think that this PR should use a name that corresponds to what is done, not what will be done in the future. You can easily change this name when the meaning changes: this function is used only once.

voodoos · 2024-12-19T14:02:02Z

I made the requested changes. I chose to rename type_omitted_parameters to type_omitted_parameters_and_build_result_type (following the argument saying that "this is the place where we "type" the omitted arguments: taking them from their representation in the parsetree to their representation in the typedtree")

I can switch it promptly if you prefer handle_omitted_parameters_and_build_result_type !

gasche · 2024-12-19T14:08:40Z

I am happy with the resulting PR, and would be in favor of merging as-is because it's good enough.

(The history is slightly messy now, with several small review commits, but I also propose to leave it as-is because flemme.)

Suggested-by: Gabriel Scherer <gabriel.scherer@gmail.com>

gasche · 2024-12-19T16:29:28Z

Merged! Thanks everyone for your time.

garrigue · 2025-01-08T02:13:39Z

It seems that this was merged without renaming remaining_function_type, which is clearly wrong.
Will have to fix it.

voodoos · 2025-01-08T09:37:14Z

I must have missed it when re-reading the comments. I just made the change you suggested in #13715

Refactor Typecore.type_application

e267d7b

The typing of applications is now decomposed in two phases: collecting the arguments and typing them. Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

MisterDA reviewed Nov 14, 2024

View reviewed changes

Comment thread ocamldoc/odoc_ast.ml Outdated

voodoos added 2 commits November 20, 2024 14:46

Refactor: use std function to filter a list in odoc_ast

183948c

Suggested-by: Antonin Décimo <antonin@tarides.com>

Add changelog entry for ocaml#13612

f91ec48

gasche reviewed Nov 20, 2024

View reviewed changes

Comment thread lambda/translcore.ml Outdated

Comment thread lambda/translcore.ml

gasche reviewed Nov 20, 2024

View reviewed changes

samsa1 reviewed Nov 26, 2024

View reviewed changes

Comment thread typing/typecore.ml Outdated

dra27 assigned gasche and goldfirere Nov 27, 2024

gasche mentioned this pull request Dec 4, 2024

non-termination in type_application #13658

Closed

gasche approved these changes Dec 4, 2024

View reviewed changes

gasche and others added 8 commits December 5, 2024 08:43

typecore.ml: documentation comments for untyped_apply_arg

7f0c3f4

Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

typecore.ml: documentation comments for type_application

0a100d8

Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

type_args: move [expand_head] to match trunk evaluation order

015b82e

fix a comment

e0c1db7

typecore.ml: small location improvement in an type_application error …

21604ef

…message Co-authored-by: Samuel Vivien <samuel.vivien@inria.fr> Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr> Co-authored-by: Ulysse Gérard <thevoodoos@gmail.com>

minor renaming for consistency

21338b9

typecore.ml: minor tweak

5bf48cb

gasche force-pushed the js-upstream-type-application-refactor branch from 53b2ab7 to 5bf48cb Compare December 5, 2024 07:44

garrigue requested changes Dec 13, 2024

View reviewed changes

garrigue approved these changes Dec 16, 2024

View reviewed changes

voodoos force-pushed the js-upstream-type-application-refactor branch from b29f136 to dd0b9ad Compare December 19, 2024 13:51

voodoos force-pushed the js-upstream-type-application-refactor branch from dd0b9ad to 2a41550 Compare December 19, 2024 13:53

gasche reviewed Dec 19, 2024

View reviewed changes

Comment thread lambda/translcore.ml

gasche added the merge-me label Dec 19, 2024

voodoos added 5 commits December 19, 2024 15:24

Introduce Typedtree.map_apply_arg

d2b884f

Suggested-by: Gabriel Scherer <gabriel.scherer@gmail.com>

Make matching exhaustive

f4c8d14

Reword some comments.

3c94f26

Rename type_omitted_parameters

32c98b6

Update reviewers list in changelog

fceca9e

voodoos force-pushed the js-upstream-type-application-refactor branch from dde8951 to fceca9e Compare December 19, 2024 14:24

gasche merged commit e74da11 into ocaml:trunk Dec 19, 2024

ccasin mentioned this pull request Apr 21, 2026

Reconciliation of typing/ merges oxcaml/oxcaml#5781

Closed

Uh oh!

Conversation

voodoos commented Nov 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

goldfirere commented Nov 15, 2024

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

garrigue Dec 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

garrigue Dec 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

garrigue Dec 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

voodoos Nov 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

gasche commented Nov 21, 2024

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!

Uh oh!

goldfirere commented Nov 27, 2024

Uh oh!

gasche commented Dec 4, 2024

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

samsa1 commented Dec 5, 2024

voodoos commented Nov 14, 2024 •

edited

Loading

garrigue Dec 13, 2024 •

edited

Loading

garrigue Dec 16, 2024 •

edited

Loading

garrigue Dec 16, 2024 •

edited

Loading

voodoos Nov 20, 2024 •

edited

Loading

garrigue Dec 13, 2024 •

edited

Loading

garrigue Dec 16, 2024 •

edited

Loading