<p>Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type <span class="math-container">$\mathsf{read}\;\alpha$</span> of readable variables storing values of type <span class="math-container">$\alpha$</span> and a type <span class="math-container">$\mathsf{write}\;\alpha$</span> of writable variables sotring values of type <span class="math-container">$\alpha$</span>, we have:</p>
<ul>
<li><span class="math-container">$\mathsf{read}\;\mathsf{int}$</span> - a read-only integer variable</li>
<li><span class="math-container">$\mathsf{write}\;\mathsf{int}$</span> - a write-only integer variable</li>
<li><span class="math-container">$\mathsf{read}\;\mathsf{int} \land \mathsf{write}\;\mathsf{int}$</span> (an intersection type) – a read-write integer variable</li>
<li><span class="math-container">$\mathsf{write}\;(\mathsf{int} \land \mathsf{bool})$</span> – a variable into which we can write both an integer and a boolean</li>
</ul>
<p>One such example is John Reynold's language <a href="https://apps.dtic.mil/sti/pdfs/ADA311094.pdf" rel="nofollow noreferrer">Forsythe</a>. The paper linked to also gives denotational semantics of intersection types as pullbacks. For further material see Chapter 16.3 of his book <a href="https://doi.org/10.1017/CBO9780511626364" rel="nofollow noreferrer">Theories of Programming Languages</a>.</p>

CC BY-SA 4.0
2024-02-04T19:27:11.987Z
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).
LaR
CC BY-SA 4.0
2024-02-04T22:35:34.173Z
What's your point?
Andrej Bauer
CC BY-SA 4.0
2024-02-05T06:40:18.810Z
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.
LaR
CC BY-SA 4.0
2024-02-05T07:17:56.057Z
In PL you should expect the unexpected.
Andrej Bauer
CC BY-SA 4.0
2024-02-03T08:25:31.730Z
2024-02-03T08:25:31.730Z
Andrej Bauer
<p><strong>Later edit:</strong> When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped <span class="math-container">$\lambda$</span>-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.</p>
<hr />
<p>As I said in the comments, this is not how people usually think of intersection types.  The word &quot;type&quot; in this case is used by analogy, but intersection types are are not intended to be assigned a denotation.  Instead, intersection types are <em>elements</em> of the denotation of an untyped <span class="math-container">$\lambda$</span>-term.</p>
<p>The idea is that there are general constructions taking an intersection type system together with a preorder <span class="math-container">$\leq$</span> on the types (satisfying certain conditions) and building a reflexive domain <span class="math-container">$D$</span> (in the sense that <span class="math-container">$D$</span> is a reflexive object in the category of domains of some kind, so a model of the untyped <span class="math-container">$\lambda$</span>-calculus) such that the elements of <span class="math-container">$D$</span> are sets of intersection types ordered by the order induced by <span class="math-container">$\leq$</span>.  Intersection is just infimum in this order.</p>
<p>This is all described in the paper by Simona Ronchi pointed out by Andrej in the comments.</p>

CC BY-SA 4.0
2024-02-02T08:28:10.103Z
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?
Andrej Bauer
CC BY-SA 4.0
2024-02-02T08:57:49.657Z
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?
LaR
CC BY-SA 4.0
2024-02-02T10:11:54.933Z
@AndrejBauer Yes! That is one of the ways I think about them.
Neel Krishnaswami
CC BY-SA 4.0
2024-02-02T11:39:41.593Z
@LaR: "theoretical interest" is such an ugly phrase. But if you are interested in programming languages that implement intersection types, why didn't you ask about that? Didn't John Reynolfds have? Forsythe or some such.
Andrej Bauer
CC BY-SA 4.0
2024-02-02T11:44:06.730Z
Indeed, here John's paper on [Forsythe](https://apps.dtic.mil/sti/pdfs/ADA311094.pdf), 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.
Andrej Bauer
CC BY-SA 4.0
2024-02-02T12:53:26.563Z
Great, thanks a lot!
LaR
CC BY-SA 4.0
2024-02-03T06:27:08.160Z
@AndrejBauer I suggest you turn your last comment into an answer.  I had in mind intersection types as they are used in the untyped $\lambda$-calculus, but at this point it's clear that the OP had in mind intersection types in (typed) programming languages, so my answer doesn't really answer his question (in fact, I'm thinking of deleting it, as well as my comments, if you add a more pertinent answer!).
Damiano Mazza
CC BY-SA 4.0
2024-02-03T07:09:44.830Z
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.
LaR
CC BY-SA 4.0
2024-02-03T08:13:10.403Z
@DamianoMazza: Don't delete the answer, but consider prefacing it with a disclaimer.
Andrej Bauer
CC BY-SA 4.0
2024-02-02T07:44:22.640Z
2024-02-04T12:18:28.470Z
2024-02-04T12:18:28.470Z
Damiano Mazza
<p>Is there a denotational (possibly, domain theoretic) semantics of intersection types? If yes, could you provide some references?</p>
<p>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 <span class="math-container">$\sigma$</span> and <span class="math-container">$\tau$</span>, the meanings <span class="math-container">$[[\sigma]]$</span> and <span class="math-container">$[[\tau]]$</span> are domains. However, the intersection of two domains is not necessarily a domain. So, what is the (domain-theoretic) meaning of <span class="math-container">$\sigma \cap \tau$</span>?</p>

CC BY-SA 4.0
2024-01-30T23:03:35.960Z
Did you bother to [Google "denotational semantics of intersection types](https://www.google.com/search?hl=en&q=denotational%20semantics%20of%20intersection%20types)? For me the [top result](https://drops.dagstuhl.de/storage/00lipics/lipics-vol097-types2016/LIPIcs.TYPES.2016.2/LIPIcs.TYPES.2016.2.pdf) is a pretty good starting point.
Andrej Bauer
CC BY-SA 4.0
2024-01-31T08:28:02.017Z
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).
LaR
CC BY-SA 4.0
2024-01-31T08:47:20.240Z
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.
Andrej Bauer
CC BY-SA 4.0
2024-01-31T09:20:56.657Z
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.
Damiano Mazza
CC BY-SA 4.0
2024-01-31T09:26:16.660Z
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.
Damiano Mazza
CC BY-SA 4.0
2024-01-31T09:39:09.393Z
Thank you for your responses and I apologize for my, possibly naive, question. I am a complete newcomer to type theory (as you may have already realized :-)). I have edited my initial question to add some context.
LaR
<type-theory><denotational-semantics><domain-theory>
Denotational semantics of intersection types
LaR
# Denotational semantics of intersection types

(Asked by: username_0 on 2024-01-30)

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$?

**Tags:** type-theory, denotational-semantics, domain-theory
> **Comments:**
> **username_1**: Did you bother to [Google "denotational semantics of intersection types](https://www.google.com/search?hl=en&q=denotational%20semantics%20of%20intersection%20types)? For me the [top result](https://drops.dagstuhl.de/storage/00lipics/lipics-vol097-types2016/LIPIcs.TYPES.2016.2/LIPIcs.TYPES.2016.2.pdf) is a pretty good starting point.  
> **username_0**: 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).  
> **username_1**: 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.  
> **username_2**: 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.  
> **username_2**: 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.  
> **username_0**: Thank you for your responses and I apologize for my, possibly naive, question. I am a complete newcomer to type theory (as you may have already realized :-)). I have edited my initial question to add some context.  

---

## 2 answers

### Answer by username_1 on 2024-02-03. Score: 3 | Accepted answer

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](https://apps.dtic.mil/sti/pdfs/ADA311094.pdf). 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](https://doi.org/10.1017/CBO9780511626364).

> **Comments:**
> **username_0**: 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).  
> **username_1**: What's your point?  
> **username_0**: 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.  
> **username_1**: In PL you should expect the unexpected.  

---

### Answer by username_2 on 2024-02-02. Score: 3

**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.

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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?  
> **username_3**: @AndrejBauer Yes! That is one of the ways I think about them.  
> **username_1**: @LaR: "theoretical interest" is such an ugly phrase. But if you are interested in programming languages that implement intersection types, why didn't you ask about that? Didn't John Reynolfds have? Forsythe or some such.  
> **username_1**: Indeed, here John's paper on [Forsythe](https://apps.dtic.mil/sti/pdfs/ADA311094.pdf), 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.  
> **username_0**: Great, thanks a lot!  
> **username_2**: @AndrejBauer I suggest you turn your last comment into an answer.  I had in mind intersection types as they are used in the untyped $\lambda$-calculus, but at this point it's clear that the OP had in mind intersection types in (typed) programming languages, so my answer doesn't really answer his question (in fact, I'm thinking of deleting it, as well as my comments, if you add a more pertinent answer!).  
> **username_0**: 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.  
> **username_1**: @DamianoMazza: Don't delete the answer, but consider prefacing it with a disclaimer.  

---

