24 ms·
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
by chombier 9y ago
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?
- Gabriel439 9y agoSystem 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)
- evincarofautumn 9y agoSystem 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.
- chombier 9y agoI 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?
- evincarofautumn 9y agoSorry, 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.
- chombier 9y agoI see, thanks for the precision!