This PR implements syntactic function arity as described in this RFC.

This is a big PR! To help everyone understand what's going on, I've written this (longish) introductory post. It starts by summarizing the related RFC, offers some changes to design that came up during implementation, includes details to help a reviewer understand the changes, and ends with a few warts in the current implementation that seem unnecessary to solve now. Readers interested in language design but not implementation details can read just through the design details. The rest of this post is relevant only to someone providing a detailed review and may make the most sense read in parallel with the review.

The motivation is twofold:

• Semantics: in the relatively rare cases where it makes a difference, the implemented semantics is both clearer and closer to programmer expectations than the current semantics.
• Implementation: the implemented semantics allow us to simplify some tricky and fragile parts of the compiler.

The RFC has more detail, but I’ll summarize briefly. A function has a notion of “arity”, which is how many arguments it will accept before running effects for optional argument defaults and pattern matching. (Pattern matching can have effects, e.g. lazy patterns.) Currently the parser treats all functions as unary and the arity is only determined later based on the typedtree. Effectful patterns interrupt arity, so let f (lazy x) y = x + y is treated as a unary function returning a unary function. However, this changes with this PR.

After this PR, arity is a syntactic notion, so let f (lazy x) y = x + y is a 2-ary function. f (lazy (assert false)) won’t raise, but f (lazy (assert false)) 3 will.

There is a related, but subtly different, notion of “runtime arity” of a function. If a function application is fully saturated (i.e. the function has runtime arity n and is applied to n arguments), there is an optimization to make application fast in native code. This PR makes syntactic arity almost always the same notion as runtime arity. The one exception is when the syntactic arity is greater than the max allowed runtime arity (127), in which case the application optimization stops being useful.

Design Decisions and Clarifications to RFC

There are a few details implicit in or missing from the RFC that are worth spelling out here.

Optional argument defaults

The RFC describes how pattern matching works with syntactic arity, but doesn’t give a precise spec for optional argument defaults. The intuition is the same. Pattern matches and optional argument defaults are evaluated from left-to-right, with the relative order preserved from the parameter order.

The more general characterization is as follows:

Any active function parameter in the list of parameters between fun and -> (or between let function_name and =) is evaluated in left-to-right order before entering the body of a function (or before performing the match that is part of a function body). An active function parameter is any of the following:

• Lazy pattern
• A record pattern matching a mutable field
• Partial pattern matches
• Optional parameters with default values
• Float array patterns, like [| 1.0, x |]. Matching against such a pattern can involve allocation, because x must refer to a boxed float but the array is flat. Allocation can run the GC. Running the GC can run finalizers, which runs arbitrary code.

Coercions and constraints

The parsetree spec given in the RFC mentions constraints, but not coercions. This should be a 2-ary function:

type a = [ `A ]
type ab = [ a | `B ]
type abc = [ ab | `C ]
let f () : ab -> ab :> a -> abc = function x -> x;;

stedolan tells me this was an unintentional omission. Coercions should be treated just like normal type constraints, not interrupting the arity of the declared function.

Class functions

Class functions still aren’t n-ary:

# class c ?(arg1 = print_endline "arg1") () ?(arg2 = print_endline "arg2") () = object(_) end;;
# let c' = new c ();;
arg1
# let c'' = c' ();;
arg2

I wanted to get input on this design before doing the same thing for class functions.

Avoiding unsoundness

This definition would be unsound:

# type (_, _) eq = Eq : ('a, 'a) eq
# let bad : type a. ?opt:(a, int -> int) eq -> unit -> a =
    fun ?opt:(Eq = assert false) () x -> x + 1

(* hypothetically, this would be given this type. but we don't actually do this. *)
val bad : ?opt:('a, int -> int) eq -> unit -> 'a
# let x : 'a. 'a = bad ()

In the current world, unsoundness is avoided by not pushing the evaluation of assert false past any GADT patterns. (So bad () would raise.) But this “pushing the evaluation” is the whole point of syntactic arity. So the approach I take is to stipulate that an n-ary function definition must unify with an n-ary arrow type:

# let bad : type a. ?opt:(a, int -> int) eq -> unit -> a =
      fun ?opt:(Eq = assert false) () x -> x + 1;;
Error: This expression has type ?opt:(a, int -> int) eq -> unit -> 'a -> 'b
       but an expression was expected of type
         ?opt:(a, int -> int) eq -> unit -> a
       Type 'a -> 'b is not compatible with type a

This approach has two warts. One, it rules out some previously-accepted (if weird) definitions:

# let spurious : type a. (a, int -> int) eq -> a = fun Eq x -> x + 1;;
Error: This expression has type (a, int -> int) eq -> 'a -> 'b
       but an expression was expected of type (a, int -> int) eq -> a
       Type 'a -> 'b is not compatible with type a

Two, it interacts with locally abstract types in a non-obvious way. The unification happens after unification variables have been substituted for any locally abstract type. So a definition might typecheck, but with 'a -> 'b substituted for what was written as a locally-abstract type:

# let odd (type a) ?opt:((Eq : (a, int -> int) eq) = assert false) () : a = function x -> x + 1;;
val odd : ?opt:('a -> 'b, int -> int) eq -> unit -> 'a -> 'b = <fun>

(This definition is ok because it will assert false if opt is omitted and it is applied up to the 'a argument.)

This type-checking behavior is consistent with how locally-abstract types behave in other situations, like recursion and the value restriction, and so is perhaps acceptable.

# let rec f (type a) (x : a) = f 3;;
val f : int -> 'a = <fun>
# let r (type a) = ref ([] : a list);;
val r : '_a list ref = {contents = []}

If this is a sticking point, I’m happy to discuss alternatives.

Question

This is a substantial change to a widely-used AST construct. How does the OCaml community deal with such changes that warrant (e.g.) updating all PPXes?

A guide to review

It’s likely best to review directory-by-directory. Here’s a quick summary of the per-directory changes:

• parsing: Add the new function construct, replacing the two old constructs. The new construct includes multiple function parameters, newtype parameters, coercions/constraints on the function body, and the function body itself (whether that’s function cases or a standard expression body).
• typing: Though the diff is large, this is semantically a refactor of existing functionality. The new function construct involves several language features (newtypes, coercions, constraints, function cases), and so this patch factors out pieces of type-checking code for those language features to be reused in the typing of the new construct.
• lambda: Some tricky code is deleted. I get rid of push_defaults and the currying transformation, instead preserving the syntactic arity from type-checking. I add the translation of optional default arguments – this used to be done in type-checking, but this interacts poorly with syntactic arity.
• utils: I add a helper function, List.chunks_of, that I found useful in enforcing the max runtime arity of a function.
• tools: Changes to ocamlprof implied by the change in parsetree.
• ocamldoc: Changes to ocamldoc implied by the change in typedtree.

There is more detail below.

The parsetree/typedtree changes imply some changes outside of the parsing/typing directories. The first few commits split up the parsing and typechecking changes, if you’re interested in narrowing in on the changes implied by one or the other.

Parsing

This is mostly a straightforward implementation of the RFC, with a few things to note:

• fun (type a b c) -> e is still interpreted as nested Pexp_newtype’s, and not as a zero-argument Pexp_function.
• I maintain a function parameter as arg_label * expression option * pattern to keep the diff smaller. This is instead of adopting the Arg_simple of pattern | Arg_labelled of string * pattern | Arg_optional of string * pattern * expression option distinction described in the RFC. This could easily be changed later.
• I introduce a Pconstraint/Pcoerce variant instead of representing coercions/constraints as a pair of optional types. I found this type to be advantageous in type-checking, as it allows us to keep the code that handles coercions/constraints separate from the code that handles the absence of a coercion/constraint. It’s parallel to Pexp_constraint/Pexp_coerce, which is a nice bonus.
• In fun x y -> function p1 -> e1 | p2 -> e2, the function should be parsed as a Tfunction_cases and not as a Tfunction_body $expr in order to get the arity right. The PR attempts to avoid shift-reduce conflicts here by creating a new class of expression, fun_expr, which can appear on the RHS of a lambda/function definition, and which excludes function constructs. To force the interpretation of the RHS as Tfunction_body $expr, the programmer can wrap the function in parentheses.

Typing

Typing code for three constructs is significantly refactored, in increasing order of invasiveness:

• Newtypes, like (type a) …
• Coercions/constraints
• Cases (already used in typing matches and fun/function constructs)
• Functions

A source of complexity common to all of these is the fact that typing the “argument” is no longer uniform. I address this by parameterizing the typing of these constructs over a function that takes care of typing the argument.

Let me make that clearer with an example. Take constraints. Previously the only constraint-like construct was Pexp_constraint (e, t), which represents things like (e : t). Constructs like let f x : t = function <cases> were desugared as let f x = (function <cases> : t). This desugaring is no longer possible, as the function body is parsed as Pfunction_cases, i.e. not an expression. So, I took the code that handled Pexp_constraint, bubbled it up to a top-level function, and parameterized it over the argument to the constraint; that allows the argument to be an expression (as in (e : t)) or “function cases” (as in let f x : t = function <cases>).

It is relatively straightforward to see how this technique was applied with Pexp_newtype and Pexp_constraint/Pexp_coerce. It is somewhat more difficult to see how this worked with type_cases, so I have a dedicated section on that below.

map_half_typed_cases and type_cases

This section describes the refactoring I did in the typing of function cases. It’s ultimately a no-op refactor, but the approach is more complex than the other pieces of this PR.

There used to be a single function, type_cases, which handled the typing for fun parameters, match cases, function cases, letop cases, and try cases. In this PR, I pull out a large amount of that code into map_half_typed_cases – the typing of fun parameters now calls that instead of type_cases. The “half” in “half typed cases” refers to the fact that the pattern, but not the body, is type-checked. (This terminology is used already in typecore.)

Take an example like fun x y -> function <cases>. You can think of map_half_typed_cases as the code in common to the typing of x, y, and <cases>. It’s the common prelude and postlude that we always want to run when typing a parameter, including (say) the typing of the pattern. But it’s now parameterized over what it means to type the body of the parameter. For x and y, that’s a recursive call to type_function to check the rest of the parameters and the body; for <cases>, that’s checking the expression bodies of each of the cases.

GitHub’s diff is actually very helpful here. It shows how type_cases was refactored into map_half_typed_cases. The big deleted hunk of code was just moved into the new type_cases. type_cases is now only called on things that are syntactically cases, so it does some extra things:

• Type when-guards
• Do the ambiguous binding check in the presence of when-guards
• Check case expression bodies

Typing a function

This is now structured as a fold over the parameters. type_function does much of the same work as the old type_function, except now it also calls the parameterized versions of typing constraints, newtypes, and cases.

A guide to review: better diffs

Refactoring newtypes/coercions involved moving a fair amount of code. This bash function helps you see that, with color:

function my_diff () {
  # git diff doesn't work with process subsitution
  tmp1=$(mktemp)
  tmp2=$(mktemp)
  merge_base=$(git merge-base trunk syntactic-function-arity)
  git show "$merge_base":typing/typecore.ml | sed -n "$1" > "$tmp1"
  git show syntactic-function-arity:typing/typecore.ml | sed -n "$2" > "$tmp2"
  git diff --patience --no-index -w -- "$tmp1" "$tmp2"
}

Warts in the implementation

Methods

There is a small ugly function in translation to give methods the right arity.

Take the method m of this class as an example:

class c = object(self)
  method m x y = x + y
end

This method is parsed roughly as: Pexp_function ([ “self” ], Pexp_poly (Pexp_function ([ “x”, “y” ], … (* x + y *)))). But we’d like for m to have an arity of 3 (not because this can change the semantics of the program, but so that we get a runtime arity of 3 and can benefit from the native code optimization). The approach I take is to recover the arity in translation to lambda, by fusing together function bodies when the inner one is a Texp_poly. This is possible because methods are the only places that Pexp_poly is introduced.

It seems more principled to have an AST node that encodes this more directly. (Perhaps Pexp_poly should take an extra argument, self?) But, I didn’t do this as part of this PR to avoid yet another invasive change.

Attributes

Some attributes continue to be dropped. E.g.:

fun x y -> function[@inline] z -> expr

Here, the inline attribute is dropped in translation as it’s attached to the Pfunction_cases piece of an n-ary function, and not a proper expression. (This function can’t be inlined!) This doesn’t change anything. Previously this attribute was silently dropped in the currying translation.

Attributes relevant to type-checking continue to be respected, e.g. this is OK:

fun x y -> function[@ocaml.warning "-8"] true -> expr