Are lower-arity functions subtypes of higher-arity ones?

I've found that there isn't a concept similar to "arity-based subtyping" in many languages that I've programmed in, where higher-order functions could consume functions of lower arity than their argument type, differing in a consistent way: say, preserving leftmost arguments in order, or requiring name-type pairs to match. For example, `(A) -> C <: (A, B) -> C` such that `((A, B) -> C) -> D` admits `(A) -> C`. Would such a feature be equivalent to ad hoc polymorphism, and if so, why isn't it offered or used much/at all?

A special case that I'm particularly interested in is substituting values for functions of the same return type without wrapping in an identity function, i.e. `((A) -> B) -> C` admitting `B`. If this exists and is better known under a different name, that would also certainly answer my question.

• How would your question relate to partial function application and currying? – Robert Harvey Dec 19 '16 at 23:15
• @RobertHarvey We could sort of say the concrete lower-arity function is the partial of an intermediate, higher-order function constructed during the cast, but I think that would be sort of backwards. There isn't "fixing" per se because the fixed arguments intentionally don't matter. How do you see them being relevant? – concat Dec 20 '16 at 0:14

2 Answers

I am not aware of any subtyping system for which `A -> C` is a subtype of `(A, B) -> C`. That being said, there is no reason after all, `(a -> c) => (a & b -> c)` is a theorem of basically all logics so you could consistently design a type system with that subtyping rule. Nevertheless, I think there are several reasons that this is never done:

1. Subtyping rules generally comes with costs: they make type inference more difficult/more limited and they can complicate language implementation. You generally want to avoid them if you can't come up with a great reason to have them.
2. It would be inconsistent with arity overloading which is a feature in many languages (Erlang, C#, Java, ...).
3. It is not clear why you would want `(A -> C) <: ((A, B) -> C)` rather than, say `(B, A) -> C` or `B -> A -> C`. That is the subtyping relation is not as natural as typical ones and would be arbitrarily picked among related ones.

All that being said, a structural subtyping system is very similar to what you want. Suppose I have `F = { a : A } -> C` and `G = { a : A, b : B } -> C`. Because `{ a : A, b : B } <: { a : A }`, by the rule `(A <: B) => (B -> C <: A -> C)`, we have `F <: G`. This is basically what you want and exists in several programming languages already such as Elm and Typescript.

• Good points. The logic of preserving leftmost arguments comes from optional and variadic arguments being on the right, so that priority of arguments could be preserved. Is `A->C <: B->A->C` traditionally? That's unexpected. – concat Dec 20 '16 at 2:26
• Not traditionally, but `(A, B) -> C`, `(B, A) -> C`, `A -> B -> C` and `B -> A -> C` are all intraconvertible. Type theory and functional programming languages would tend to prefer the last of these as it makes adding arguments and taking them away simpler. My main point is that it is a matter of fairly arbitrary choice which convention you pick. – walpen Dec 20 '16 at 2:39

So it's not quite right to say that lower arity functions are subtypes of higher ones. You're not talking only about functions after all.

But if you have a delegate (function pointer, function variable, etc) that has a signature of a higher arity, it should be able to take a function that only satisfies part of the parameters. That is typesafe, though I'm not sure it has a proper name.

There are some gotchas there though. The function pointer will still want to pass in all of the arguments. Your implementation will need to be smart enough with the call stack to ignore those arguments, find the ones I need, and also clean everything up when done. Or you'll need to automatically wrap the function when assigning it to the variable expecting a higher arity (which then adds complexity when you're not directly assigning the function, and the same performance overhead as wrapping it yourself).

• I'm guessing it'll boil down to semantics, but I don't quite follow "You're not talking only about functions after all." Could you elaborate? – concat Dec 20 '16 at 2:30
• Apologies also, I didn't realize that the rules I was evaluating were so vague, so I edited the question to suggest leftmost arguments be preserved as an example. In that case, I don't see the function needing to do any work finding the arguments. Cleaning up though is a solid issue. – concat Dec 20 '16 at 2:40
• @concat - the only place where function subtyping makes sense off hand is if you can pass a function into a variable or as an argument to a higher order function. In both these cases, one of the types you're comparing isn't a function - it's a variable or parameter type. – Telastyn Dec 20 '16 at 2:49