Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion?

I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]. It has a term-level fixed point combinator $$\mathit{fix} : \forall X:*.~(X\rightarrow X)\rightarrow X$$ and type-level fixed point combinators $$\mu_\kappa : (\kappa\rightarrow\kappa)\rightarrow\kappa.$$ Neither the ideal model the the interval model seems to fit.

In the ideal model [1], the convertibility rule $$\mu_\kappa T\leftrightarrow T(\mu_\kappa 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 $$\mu_*(\lambda X.~X)\rightarrow\mu_*(\lambda 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.

  • $\begingroup$ I have not thought about this problem much, but I expect that the denotational model in Genericity and the Pi-Calculus should be extendable to F$\omega$. $\endgroup$ – Martin Berger Jul 3 '16 at 19:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.