3
$\begingroup$

By reading literature on (denotational) semantics of types, I see that people tried to give several models of types. Reynolds showed that types in general cannot be given a set semantics in classical set theory. However, it was shown later that constructive sets could be used. Now, I also stumbled upon papers where types are seen as complete partial orders and Scott domains. Further, Cardelli presents types as ideals, but acknowledges that retracts should be used to handle parametric types.

I understand that one can give different models depending on the type system, but is there a known model of types that handles parametric types, universal parametric polymorphism, existential polymorphism, recursive types, and subtyping? For instance, where would I start if I want to give a denotational model for OCaml types (but without the side-effect features)?

Also, how does Reynolds' relational model relate (no pun intended) to the existing models?

|cite|improve this question
$\endgroup$
  • $\begingroup$ It is not clear what you are asking. Which kind of type system do you have in mind? The semantic models you mention are quite different and so it's hard to guess what sort of structure you want to model. If you're going to throw together a bunch of features you need to be far more specific: what sort of polymorphism? Whuch recursive types are allowed (in the presence of polymorphisms and subtyping)? What are the subtyping rules? It's easy to come up with something inconcsistent. $\endgroup$ – Andrej Bauer Sep 21 '16 at 20:47
  • $\begingroup$ Fair point. I updated the answer to make it a bit more concrete. But, the vagueness of my question comes from the fact that I don't completely understand even why are there so many models and how do they relate. That is why I asked is there a single model (covering multiple features). My primary goal is to really understand what types denotationally mean. $\endgroup$ – bellpeace Sep 21 '16 at 21:00
  • $\begingroup$ Are you considering operational semantics as well, or just denotational? I'm not too familiar with denotational semantics, but operational semantics can give a clear definition of all these concepts. $\endgroup$ – gardenhead Sep 22 '16 at 0:34
  • 1
    $\begingroup$ There are many models because type theory is not a single thing. There are many type theories, used for various purposes, and they are not all compatible with each other. There is no all-encompassing system and there is no single kind of model that would cover all other models. $\endgroup$ – Andrej Bauer Sep 22 '16 at 7:10
  • 1
    $\begingroup$ Sure, I should have said constrainted or suggested instead of induced in "semantic models are induced by the typing rules". $\endgroup$ – Andrej Bauer Sep 22 '16 at 15:06

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.