Hacker News Reader

Can somebody comment on what is missing for System F(ω) to be Turing complete?

I recall that it can typecheck self-application, so is it not possible to define and use the fixed-point combinator?

System Fw cannot type-check self application

The type system is what prevents System Fw from being Turing complete. Specifically, the key bit is that you cannot unify the type "a -> b" with "a" (which is what prevents self application)

System F can check self-application with an explicit type annotation, something like λx:(∀a. a → a). x [∀a. a → a] x, but Fω can’t.

I thought Fω was an extension of System F with type operators, so I figured if System F can check self-application, System Fω can too.

Am I missing something else?

Sorry, that comment was worded badly. Both System F and System Fω can express self-application at a particular type, but they can’t give a general type for self-application, e.g., Ω = ω ω where ω = λx.xx.

I see, thanks for the precision!

Reply on news.ycombinator.com