Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Surprising interaction between parenthesizing applications and default arguments #7832

Closed
vicuna opened this Issue Jul 24, 2018 · 3 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Jul 24, 2018

Original bug ID: 7832
Reporter: @jberdine
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2018-07-25T00:43:05Z)
Resolution: not a bug
Priority: low
Severity: minor
Version: 4.07.0
Category: typing
Monitored by: @jberdine

Bug description

A bug in ocamlformat found by hhugo uncovered some, to me, surprising sensitivity of the type checker to the presence of parentheses around applications. See the following toplevel interaction for example:

# let id x = x;; val id : 'a -> 'a = # let plus a ?(b=0) c = a + b + c;; val plus : int -> ?b:int -> int -> int = # id (plus 1);; - : ?b:int -> int -> int = # id (plus 1) 1;; - : int = 2 # (id (plus 1)) ~b:1;; - : int -> int = # id (plus 1) ~b:1;; Error: This expression has type ?b:int -> int -> int but an expression was expected of type b:'a -> 'b

Note the last two expressions are the same except for two nested 1-argument applications versus a single 2-argument application, but the first types and the second doesn't. Is this difference expected? Is there a description of when such distinctions are important? (Ideally ocamlformat would emit the parens where needed but not have to for all nested applications, so I'm looking for some syntactic criterion to use to distinguish which Parsetrees need the parens and which don't.)

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 25, 2018

Comment author: @garrigue

There is a specification of the dynamic semantics in "Labeled and optional arguments for Objective Caml" (http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html). Yhe problem you describe here is with the type checking, but the two are related.

For type checking, the rule is as follows:

  • match the labels of the arguments with those in the type of the function
  • after doing this matching, discard optional arguments in the type of the function if a non-labeled argument was passed that appears later in the type
  • for labels that do not appear in the type of the function, collect them in the order in which they appear in the application, and use them to generate an expected return type, to be unified with the return type of the function
  • then do all unifications

So the point is that when typing an application without parentheses, unifications are delayed to the end.
Here this means that the type inferred for id will be
(~b:'a -> 'b) -> ~b:'a -> 'b
which cannot be applied to (plus 1), which has type (?b:int -> int -> int).
By adding the parentheses, the unifications are forced first, so that (id (plus 1)) has exactly the type infered by the top-level.

So the answer is that you should be keeping the parentheses as they were in the original source code, since they may change both the static and dynamic behavior.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 25, 2018

Comment author: @garrigue

Nothing to fix, since this is the intended semantics.

@vicuna vicuna closed this Jul 25, 2018

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 25, 2018

Comment author: @jberdine

Thanks a lot Jacques, I see now.

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.