It's perfectly well typed in System F as "forall a. (a -> a) -> a".

Can you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a?

System F isn't consistent as a logic (pretty much precisely because it has general recursion). In languages with general recursion, you can do things like

(Haskell)

    anyType :: a
    anyType = anyType

or

(Rust)

    fn any_type<T>() -> T {
        any_type()
    }

System F doesn't have general recursion.

Extensions with a letrec-like construct are common, and are sometimes inaccurately called 'System F', but those languages do not have the properties of System F.

You're right. I must have been thinking of one of those extensions you're talking about (F# maybe?). I should have remembered that System F is part of the lambda cube, so it's at least as consistent as CoC

Could you write this in Java?

Here is Y-combinator in many languages:

https://rosettacode.org/wiki/Y_combinator

Not my code, but: https://gist.github.com/aruld/3965968

Does the github Java code make use of recursion?

As you can clearly see, it does not. It also doesn't use any forced typecasts to circumvent type checking.

Is FuncToFunc defined recursively in the excerpt below???

      private static interface FuncToTFunc<T> {
          Func<T> apply(FuncToTFunc<T> x);
      }

BTW, what is "x" in the above?

Also is Func defined mutually recursively with FuncToFunc in excerpt below?

      public static <T> Func<T> Y(final Func<Func<T>> r) {
        return ((FuncToTFunc<T>) f -> f.apply(f))
            .apply(
                f -> r.apply(
                    x -> f.apply(f).apply(x)));
      }

Joker_vD: Looks like you are incorrect because Func and

FuncToFunc are defined recursively.

No, they are not. Do you know what "interface" is in Java, and what is "class"? And what is "method"?

Interface Func doesn't refer to FuncToFunc in its declaration, and interface FuncToFunc doesn't refer to Func. The method Y does refer to those two interfaces, but it's declared later than those are, and they don't (and can't, acvtually) refer to it.

I think it is approximately `public <T> T y(Function <T, T> f)`.

Thanks!

Could you use your Java code to define Factorial?

Interestingly, mutable data is also sufficient to achieve general recursion in a typed language:

  let fact' = ref (fun x -> x) in
  let fact = fun n -> if n = 0 then 1 else n * !fact' (n-1) in
  fact' := fact; fact 3