[TYPES] Fwd: Denotational semantics of Fω with type- & term-recursion

[Yufei Cai]

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