4
$\begingroup$

Is there a denotational (possibly, domain theoretic) semantics of intersection types? If yes, could you provide some references?

Let me try to give some context to my question. In the usual denotational semantics of (say) a functional language, the meaning of a data type is a domain. So, given types $\sigma$ and $\tau$, the meanings $[[\sigma]]$ and $[[\tau]]$ are domains. However, the intersection of two domains is not necessarily a domain. So, what is the (domain-theoretic) meaning of $\sigma \cap \tau$?

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ Did you bother to Google "denotational semantics of intersection types? For me the top result is a pretty good starting point. $\endgroup$
    – Andrej Bauer
    Commented Jan 30 at 23:03
  • $\begingroup$ My question was about the meaning of intersection types and not "the use of intersection types for reasoning in a finitary way about terms interpretations in various models of lambda-calculus" (as the paper you cite mentions in the abstract). $\endgroup$
    – LaR
    Commented Jan 31 at 8:28
  • 1
    $\begingroup$ I mean to be helpful here (but also to let people know that we're not a replacement for literature search). If you read past the abstract, you will see a bunch of references. You chase down the ones that seem most promising ([18] in particular), and you quickly realize that Simona Ronchi Della Rocca is the person to pay attention to. Then you're very close to finding out that intersection types are an Italian thing, north Italian to be more precise. But if you just ask an unmotivated and unexplained two-line question here, don't expect much of an answer. At least provide some context. $\endgroup$
    – Andrej Bauer
    Commented Jan 31 at 8:47
  • 1
    $\begingroup$ As the paper linked by Andrej says, intersection types are denotational semantics. You see a glimpse of this in the fact that intersection types enjoy both subject reduction and expansion, so the collection of types of a term is invariant under reduction. I haven't read the paper but it probably will explain at some point how so-called filter models, which are particular types of Scott-domain-based models, may be described with intersection types. $\endgroup$
    – Damiano Mazza
    Commented Jan 31 at 9:20
  • 1
    $\begingroup$ If I understand correctly your question, you are looking for an interpretation of intersection types into domains, so you want to associate a domain with a type. In light of what I said above, this would amount to associating a domain to a point of a domain. Is this what you want to do? In any case, as it is, I don't think the question makes much sense. $\endgroup$
    – Damiano Mazza
    Commented Jan 31 at 9:26

2 Answers 2

Reset to default
3
$\begingroup$

Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type $\mathsf{read}\;\alpha$ of readable variables storing values of type $\alpha$ and a type $\mathsf{write}\;\alpha$ of writable variables sotring values of type $\alpha$, we have:

  • $\mathsf{read}\;\mathsf{int}$ - a read-only integer variable
  • $\mathsf{write}\;\mathsf{int}$ - a write-only integer variable
  • $\mathsf{read}\;\mathsf{int} \land \mathsf{write}\;\mathsf{int}$ (an intersection type) – a read-write integer variable
  • $\mathsf{write}\;(\mathsf{int} \land \mathsf{bool})$ – a variable into which we can write both an integer and a boolean

One such example is John Reynold's language Forsythe. The paper linked to also gives denotational semantics of intersection types as pullbacks. For further material see Chapter 16.3 of his book Theories of Programming Languages.

Improve this answer
$\endgroup$
4
  • $\begingroup$ The paper of Reynolds states in page 8: "At the outset, a caution must be sounded that this use of the word "intersection" can be misleading. If one thinks of types as standing for sets, then the intersection of two types need not stand for the intersection of the two corresponding sets". It seems that there is another paper that gives a set-theoretic semantics for intersection types based on ideals. See: David B. MacQueen, Gordon D. Plotkin, Ravi Sethi: An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71(1/2): 95-130 (1986). $\endgroup$
    – LaR
    Commented Feb 4 at 19:27
  • $\begingroup$ What's your point? $\endgroup$
    – Andrej Bauer
    Commented Feb 4 at 22:35
  • $\begingroup$ That, if I understand it correctly, in the MacQueen-Plotkin-Sethi paper, the intersection of two types stands for the intersection of the two corresponding sets. Therefore, this latter paper may be closer to what one expects when hearing the words "intersection types". I will update when I finish the papers. $\endgroup$
    – LaR
    Commented Feb 5 at 6:40
  • $\begingroup$ In PL you should expect the unexpected. $\endgroup$
    – Andrej Bauer
    Commented Feb 5 at 7:17
3
$\begingroup$

Later edit: When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped $\lambda$-calculus. It is now clear that this is not the right context for the question. As suggested by others, I'm keeping the answer for the sake of completeness.

As I said in the comments, this is not how people usually think of intersection types. The word "type" in this case is used by analogy, but intersection types are are not intended to be assigned a denotation. Instead, intersection types are elements of the denotation of an untyped $\lambda$-term.

The idea is that there are general constructions taking an intersection type system together with a preorder $\leq$ on the types (satisfying certain conditions) and building a reflexive domain $D$ (in the sense that $D$ is a reflexive object in the category of domains of some kind, so a model of the untyped $\lambda$-calculus) such that the elements of $D$ are sets of intersection types ordered by the order induced by $\leq$. Intersection is just infimum in this order.

This is all described in the paper by Simona Ronchi pointed out by Andrej in the comments.

Improve this answer
$\endgroup$
9
  • $\begingroup$ Does anyone use PER models on a reflexive domain, takes types to be PERs (probably closed under suprema of chains and containing bottom) and interprets intersection of types as intersection of PERs? $\endgroup$
    – Andrej Bauer
    Commented Feb 2 at 8:28
  • $\begingroup$ So, intersection types are mainly of theoretical interest? What I mean is: if I added intersection types to (say) Haskell, I would not be able to understand them in the naive way, ie., as denoting the intersection of the sets of values of two types? $\endgroup$
    – LaR
    Commented Feb 2 at 8:57
  • 1
    $\begingroup$ Indeed, here John's paper on Forsythe, he introduces intersection types on page 8. And there is denotational semantics, just what @LaR asked for. I warmly recommend reading John's papers to anyone who is interested in programming language design. $\endgroup$
    – Andrej Bauer
    Commented Feb 2 at 11:44
  • 2
    $\begingroup$ I agree that Andrej Bauer should turn his last comment into an answer. But I believe it is useful for the answer of @DamianoMazza and his comments to remain. They are useful for anyone who would like to get a broader picture of the topic. $\endgroup$
    – LaR
    Commented Feb 3 at 7:09
  • 1
    $\begingroup$ @DamianoMazza: Don't delete the answer, but consider prefacing it with a disclaimer. $\endgroup$
    – Andrej Bauer
    Commented Feb 3 at 8:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.