4 ms·
The type system appears to be System Fω[1], the “higher-order polymorphic lambda calculus”. I’m not really familiar with what class of programs it accepts, othe
by evincarofautumn 9y ago
The type system appears to be System Fω[1], the “higher-order polymorphic lambda calculus”. I’m not really familiar with what class of programs it accepts, other than “more than simply typed lambda calculus”, but typechecking is decidable and evaluation is strongly normalising (i.e. both always terminate).
[1]: https://en.wikipedia.org/wiki/System_F#System_F.CF.89 https://en.wikipedia.org/wiki/System_F#System_F.CF.89
- chombier 9y agoCan 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!