Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007832OCamltypingpublic2018-07-25 01:232018-07-25 12:06
Reporterjjb 
Assigned Togarrigue 
PrioritylowSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.07.0 
Target VersionFixed in Version 
Summary0007832: Surprising interaction between parenthesizing applications and default arguments
DescriptionA 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:

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

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.)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019272)
garrigue (manager)
2018-07-25 02:41

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.
(0019273)
garrigue (manager)
2018-07-25 02:43

Nothing to fix, since this is the intended semantics.
(0019275)
jjb (reporter)
2018-07-25 12:06

Thanks a lot Jacques, I see now.

- Issue History
Date Modified Username Field Change
2018-07-25 01:23 jjb New Issue
2018-07-25 02:41 garrigue Note Added: 0019272
2018-07-25 02:43 garrigue Note Added: 0019273
2018-07-25 02:43 garrigue Status new => resolved
2018-07-25 02:43 garrigue Resolution open => no change required
2018-07-25 02:43 garrigue Assigned To => garrigue
2018-07-25 12:06 jjb Note Added: 0019275


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker