Hacker News new | past | comments | ask | show | jobs | submit login

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!




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: