High Order Function with Type Parameter

[shelby3]

@shelby3

Agreed. The reason the example of this thread won't compile is not due to a lack of higher-kinded nor higher-ranked types, but rather because afaik the way Rust implements ad hoc polymorphism is it creates a separate instance of each function for each caller that uses a different set of input types, i.e. Rust's implementation is not a dynamic dispatch of passing in a hidden input argument for the dictionary for the trait implementation of the caller and is instead hard-coding the dictionary in each instance of the function, e.g. is not subclassing nor dynamic inversion-of-control ad hoc polymorphism (where the caller inputs the dictionary). Thus the function f has no way to control the types of Read instance of G it wants unless it specifies them. If f knows all the specific instance of Read it will use, then it can specify them as the lower bound on A instead of Read, except there is the problem that Rust (nor Haskell, nor Scala, nor Kotlin, etc) does not support first-class disjunctions (aka unions) thus we can't write:

fn f<A: File \/ Cursor, G: Fn(A) -> ()>(g: G, pred: bool) {

Note Rust does support dynamic dispatch via trait objects, so an alternative solution is (which does compile):

use std::io::Read;
use std::fs::File;
use std::io:: Cursor;

fn f<G: Fn(Box<Read>) -> ()>(g: G, pred: bool) {
  if pred {
    g(Box::new(File::open("foo").unwrap()));
  } else {
    g(Box::new(Cursor::new(b"foo")));
  }
}

fn main() {}

---

@shelby3

I understand we can emulate rank-2 (higher ranked) types in a language which doesn't explicitly support them via forall, by employing a trait with a method for generic parameter A, as explained in an example for Scala.

Rewriting that example in Rust:

fn apply<A,B>(f: A -> List<A>, b: B, s: String) -> (List<B>, List<String>) {
  (f(b), f(s));
}

It’s a type error because, B and String are not A. That is, the type A is fixed on the right of the quantifier <A,B>. We really want the polymorphism of the argument to be maintained so we can apply it polymorphically in the body of our function.

Thus the reason we'd need higher-ranked types (HRT) in this example translated from Scala to Rust, is because we desire for the type of A to be inferred by the compiler. Instead if Rust had first-class unions, we could annotate the type bounds of A so no higher-ranked inference would be required:

fn apply<A: B \/ String,B>(f: A -> List<A>, b: B, s: String) -> (List<B>, List<String>) {
  (f(b), f(s));
}

---

@keean

I think what is wanted is a intersection type like this:

fn f(g : Fn(&File) -> () /\ Fn(&Cursor) -> ())

You've restricted (changed) the intended semantics. The programmer intended that the input function would only need Read semantics (which is yet another example of how universal inference could be dangerous, see below).

If we want the input function to not use dynamic dispatch (i.e. not use trait objects), then must input a function whose polymorphism is not resolved at the scope of the signature of fn f, e.g. by employing the trait Foo as shown in the solution upthread.

With first-class unions, one could imagine perhaps we could eliminate the boilerplate (and lack of degrees-of-freedom) imposed by the trait Foo, by writing or the compiler inferring HRT:

fn f<A: (File \/ Cursor) /\ Read, G: Fn(A) -> ()>(g: G, pred: bool) {

Which could mean to resolve (caller provide) g with two non-dispatched variants of Read, one for File and the other for Cursor.

@keean

The reason to prefer function intersections can be seen by considering the difference between the following:

fn f(g : Fn(File) -> File /\ Fn(Cursor) -> Cursor)
fn f(g : Fn(File \/ Cursor) -> Fn(File \/ Cursor))

@keean and I have been discussing this, and I have pointed out (after @keean showed an example type derivation of divergence) that implicit inference of intersections can combine two different things in ways that the programmer never intended. Imagine a function which calls the add and convolve methods on a generic parameter A. With inferred intersections, the compiler could infer any combination of trait bounds for A which satisfy those two methods, giving weird semantics that were not intended (and also making the inferred types potentially gargantuan). This an example of why universal inference is dangerous.

Also, I have pointed out to @keean that (as explained by the Lambda Cube) function application is a higher-order function operator. First-class intersections (and unions) are higher-order type (construction) operators. When higher-order abstractions are allowed to interact, then the universal inference (i.e. principle typings) of type system diverges to infinite recursion (i.e. is undecidable), analogous to two mirrors facing each other. A concise example of this recursion divergence can be seen by the interaction between Scala's type (construction) operators and first-class subtyping where subtyping is a higher-order subsumption operator. Afaics Scala's problem in that linked example is not confined to universal inference, but to resolving the annotated type, thus illustrating the danger of making the type system unsound when higher-order abstractions are allowed to interact.

Thus I am arguing to @keean that if a language has both higher-order first-class abstractions:

1. Function application operators
2. Intersection type construction operators

Then only one of them should interact with the other so as to remove one of the analogous mirrors and prevent unsound divergence into infinite recursion. Thus I argue that intersections can contain higher-order functions, but function application should be illegal for intersections (of functions).

As for @keean's point about fn f(g : Fn(File \/ Cursor) -> Fn(File \/ Cursor)), I wrote to him:

This does not occur very often because it means you can give it an A or a B and you get back an A or a B, but with no relation to the type you gave it.
...
Basically (A \/ B) -> (A \/ B) throws away too much type information.

Well the type signature doesn't necessarily mean that it throws away information. The type signature does not say that if you give it an A, that has any impact on whether you might get an A or a B. The runtime computation is elided from our typing consideration. There could be valid computation with that type which has nothing to do with throwing away information.

That was all clear to me before you wrote it. I was not arguing that function is common. Rather I am stating that the following is not a function in a language without some form of I presume dependent typing:

(A -> A) /\ (B -> B)

Because the call-site will be selecting a result type based on the input type at compile-time.

Which lead to follow on discussion:

Yes, thats what static typing usually does, and this is what we usually want. Consider the identity function:
fn id<A>(x : A) -> A {

Afaics, you are conflating nominal types and anonymous types.

When we call id, we pass any input type and get back that type for one function id.

When we call (A -> A) /\ (B -> B), we are calling potentially two separate functions anonymously. There is no nominal contract (constraint) which says they have to have the same semantics. Semantics are controlled through naming scope.

Thus that is not a function type. It can only be verified to be correct in some dependent typing.

Whereas the union case at least guarantees us we get a subsumption to one function.

Ditto we should not infer intersections of types, for the same reason. The programmer must write the trait bounds when there is an intersection otherwise we can get unintended semantic combinations.

To which @keean replied:

(A -> A) /\ (B -> B)

You need to not get confused between what the type means and how we might implement it.

The intersection of two functions is still a function. It must be. Think of it like this:

The type A -> A is the set of all functions that take a single argument of type A and return a value of the same type. The functions are the values that inhabit the type.

The type B -> B is the set of all functions that take a single argument of type B and return a value of the same type.

So (A -> A) /\ (B -> B) is the set of all objects that are in BOTH the sets A -> A and B -> B, so the object is a function and can be applied.

And so we continue to discuss this in private.