3 ms·
Y Combinator does not work for strongly-typed programs because the definition is not strongly typed. Instead recursion must be added as an additional primitiv
by ProfHewitt 5y ago
Y Combinator does not work for strongly-typed programs
because the definition is not strongly typed.
Instead recursion must be added as an additional primitive to
the lambda calculus.
See https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
- Joker_vD 5y agoIt's perfectly well typed in System F as "forall a. (a -> a) -> a".
- ProfHewitt 5y agoCould you write this in Java?
- bidirectional 5y agoI think it is approximately `public <T> T y(Function <T, T> f)`.
- ProfHewitt 5y agoThanks! Could you use your Java code to define Factorial?
- Joker_vD 5y agoNot my code, but: https://gist.github.com/aruld/3965968 https://gist.github.com/aruld/3965968
- ProfHewitt 5y agoDoes the github Java code make use of recursion?
- Joker_vD 5y agoAs you can clearly see, it does not. It also doesn't use any forced typecasts to circumvent type checking.
- ProfHewitt 5y agoIs 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))); }
- ProfHewitt 5y agoJoker_vD: Looks like you are incorrect because Func and FuncToFunc are defined recursively.
- Joker_vD 5y agoNo, 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.
- jhallenworld 5y agoHere is Y-combinator in many languages: https://rosettacode.org/wiki/Y_combinator https://rosettacode.org/wiki/Y_combinator
- bidirectional 5y agoCan you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a?
- scapp 5y agoSystem 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() }
- gsg 5y agoSystem 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.
- scapp 5y agoYou'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
- cheese_it 5y agoInterestingly, 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