[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Is there a denotational semantics for System Fω in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System Fω [4]. It has a term-level fixed point combinator fix : ∀X. (X → X) → X and type-level fixed point combinators μ_κ : (κ → κ) → κ. Neither the ideal model the the interval model seems to fit. In the ideal model [1], the convertibility rule μ T ≡ T (μ T) is not sound, because not all ideal functions have fixed points. In the interval model [2], it is not clear how to make the term-abstraction and term-application rules sound. Martini's interval model for F [3] restricts types to maximal intervals, but such a restriction would leave the inhabited type μ (λX. X) → μ (λX. X) without any meaning. [1] MacQueen, Plotkin, Sethi. An ideal model for recursive polymorphic types. [2] Cartwright. Types as intervals. [3] Martini. An interval model for second order lambda calculus. [4] Hinze. Polytypic values possess polykinded types. Yufei Cai Reposting cstheory.stackexchange.com/q/36072
