<p>I have a structurally-typed object-oriented language, and I'd like to allow for types with some mutually-exclusive properties/attributes/slots/methods. That is, an object having <em>more than one</em> of these properties, or none of them, does not belong to the type. There could also be other ordinary properties within the types, which would be required as normal.</p>
<p>Clearly these wouldn't be accessible on the type itself, but you'd know that if you found one of them then the others weren't there, so that for example typecase pattern-matching on them all would be exhaustive and order-independent.</p>
<p>Ideally I'd like for this to be sound, but it does break ordinary subsumption so it may be necessary to accept some level of breakage, dynamic enforcement, or both, and I'd like to know what that is. In some respects this is related to <a href="https://languagedesign.stackexchange.com/q/952/133">this question</a> about optional properties, but this is concerned with the interplay between multiple properties within the same type.</p>

<types><static-typing><structural-types><soundness>
How can I have mutually-exclusive properties in a structural type system?
CC BY-SA 4.0
2023-05-25T08:52:45.977Z
I have to ask though: how would you use such a type? Knowing that `a` is present means you can access it. Knowing that `a` is absent means you don't need to implement it. But what can you do with an object where you know that exactly one of `a` and `b` is present, that doesn't require discriminating between the two cases (in which case you'd just take a discriminating union of the a and b versions)?
Gilles 'SO- stop being evil'
CC BY-SA 4.0
2023-05-25T09:09:19.807Z
I am imagining a typecase or multimethod scenario that does eventually discriminate, but intermediately only the shared properties are in use. A tagged union is how I might express this disjunction in another environment, but those are further outside of a structural type that a suitable value can flow into ad-hoc. In a partially-typed system it can be possible for an "extra" property to be accessible somewhere, so I want ruling it out in the types to actually rule out belonging to two classes. I'm also alive to multiple sets in the same type, but I don't want to complicate this more now (yet)
Michael Homer
CC BY-SA 4.0
2023-05-25T10:08:51.947Z
I suspect the answer involves [row polymorphism](https://en.wikipedia.org/wiki/Row_polymorphism), which allows representing types like `{x: number, empty}` and `{x: number, ρ}` where `ρ` is a row parameter. In the notation from Wikipedia, mutually exclusive properties might be written as a union type like `{x: number, absent(y), ρ} | {y: string, absent(x), ρ}`. I'm not really knowledgeable enough to write more on the subject, but if this is useful enough then I can convert it from a comment to an answer.
kaya3
CC BY-SA 4.0
2023-05-25T10:31:26.237Z
@kaya3 Row polymorphism treats each property independently. You'd need an extension to describe interactions between properties. A non-discriminated union works, but then you need to have non-discriminated unions in your type system and that's hard in a static type system.
Gilles 'SO- stop being evil'
CC BY-SA 4.0
2023-05-25T10:38:22.770Z
@Gilles'SO-stopbeingevil' Indeed, this approach would require more than just row polymorphism; I'm thinking about the question from the perspective of Typescript, which has one of the most expressive static structural type systems but lacks soundness particularly for this kind of type. Since Typescript already has undiscriminated union types, row polymorphism would be the necessary additional feature.
kaya3
CC BY-SA 4.0
2023-05-25T11:50:31.803Z
I might misunderstand the question, but it seems to me that you want to have a discriminated-variant field (like Rust's `enum`, or C++'s `std::variant`). Then that field could be exactly one of the alternatives in any given object
abel1502
CC BY-SA 4.0
2023-05-25T19:43:17.913Z
@abel1502 I'm not sure that would help - even for a field, a variant type would allow the concrete value to change dynamically between different variants at run time, so you couldn't rely on a previous check still holding. For methods it probably wouldn't work at all (although in a JavaScript-style model these are conflated, so maybe).
Michael Homer
CC BY-SA 4.0
2023-05-25T21:19:22.987Z
@MichaelHomer I don't understand your last comment. A discriminated union (aka variant) trivialises the problem (using row polymorphism, which is the basic tool to describe which properties an object has) — the type is just something like `Has_a_not_b {a: int; b: absent; 'rest} | B {a: absent; b: float; 'rest}`. You can do that with a non-discriminated union, but that opens the can of worms of non-discriminated unions.
Gilles 'SO- stop being evil'
CC BY-SA 4.0
2023-05-25T21:44:26.400Z
@Gilles'SO-stopbeingevil' The last comment was replying to a suggestion of using a single variant-typed field (as I read it, anyway), which I don't think helps, at least directly. You could nest the properties one layer deep in the values, I suppose.
Michael Homer
CC BY-SA 4.0
2023-05-25T21:44:58.827Z
Row polymorphism is likely to be part of an answer, yes, and I'm asking about how far-reaching the effects of these types would have to be.
Michael Homer
<h2>Enforcing exclusion</h2>
<p>Some inspiration for a system that works this way can be found in <a href="https://doi.org/10.1184/R1/6605507.v1" rel="nofollow noreferrer">Extensible Records Without Subsumption</a> (<a href="https://scholar.archive.org/work/jg7m6qdnpraynhid6rwvuj2n3i/access/wayback/https://s3-eu-west-1.amazonaws.com/pstorage-cmu-348901238291901/12095981/file.pdf" rel="nofollow noreferrer">pdf</a>) by Bob Harper and Benjamin Pierce. They present extensible records via row polymorphism, which your comments on your question indicate you are already familiar with, but the paper also includes the notion of a <em>lacks</em> constraint. From the introduction:</p>
<blockquote>
<p>For example, Cardelli and Mitchell’s record extension operator is only defined on records where the field being added is not already present; to prevent run time type errors, the typing rule for the extension operator must check that this is the case. We found it simpler to express this constraint directly as “<span class="math-container">$r$</span> lacks <span class="math-container">$l$</span>” instead of encoding it as “<span class="math-container">$r$</span> is less than some type lacking <span class="math-container">$l$</span>.”</p>
</blockquote>
<p>Their system allows quantified type variables to be constrained by both these negative <em>lacks</em> constraints as well as positive <em>has</em> constraints. Lacks constraints provide some of the basic material necessary to implement the mutual exclusion property you’re looking for, and in fact, they’re already sufficient to guarantee it is maintained. To see how, let’s consider a “label declaration” that binds a name that can be used as a label in a record:
<span class="math-container">$$
\mathbf{label}\ \mathsf{x} : \mathsf{T}
$$</span>
This declares <span class="math-container">$\mathsf{x}$</span> as a record label for a value of type <span class="math-container">$\mathsf{T}$</span>. We can imagine extending this declaration with support for constraints:
<span class="math-container">$$\begin{array}{l}
\mathbf{label}\ (\mathsf{x} : \mathsf{T}) ∈ \rho \\
\quad \mathbf{where}\ \mathsf{y} ∉ \rho
\end{array}$$</span>
This can be read as “<span class="math-container">$\mathsf{x}$</span> is a label for a value of type <span class="math-container">$\mathsf{T}$</span> in some row type <span class="math-container">$\rho$</span> such that <span class="math-container">$\rho$</span> lacks label <span class="math-container">$\mathsf{y}$</span>.” When a record is constructed using this label, the <span class="math-container">$\mathsf{y} \notin \rho$</span> constraint would be generated, and a constraint solver would need to be able to somehow solve it in order for the program to be accepted.</p>
<h2>Exposing exclusion</h2>
<p>This is enough to <em>enforce</em> the property, but it is not quite enough to truly leverage it. In your question, you state</p>
<blockquote>
<p>You'd know that if you found one of them then the others weren't there, so that for example typecase pattern-matching on them all would be exhaustive and order-independent.</p>
</blockquote>
<p>which requires that we <em>gain</em> information by pattern matching. This requires something a bit stronger: <em>local assumptions</em>, which are most commonly associated with generalized algebraic data types (GADTs). GADTs offer precisely the sort of property we’re looking for, namely that matching on a constructor can introduce local constraints (i.e. assumptions) only available within the pattern match’s right hand side. For example, we might write the Haskell datatype
<span class="math-container">$$\begin{array}{l}
\mathbf{data}\;\mathsf{SomeShowable}\ a\;\mathbf{where} \\
\quad \mathsf{MkSomeShowable} :: \mathsf{Show}\ a \Rightarrow a \rightarrow \mathsf{SomeShowable}\ a
\end{array}$$</span>
which “contains” a <span class="math-container">$\mathsf{Show}$</span> constraint, so pattern matching on the <span class="math-container">$\mathsf{MkSomeShowable}$</span> constructor brings that constraint into scope.</p>
<p>Although these constrained labels aren’t quite GADTs, they can be typechecked using the same principles. Since the constraint must be satisfied for each record they’re added to, a record containing the label serves as a proof that all the constraints must hold, and a local constraint can be brought into scope. Implementing a typechecker that supports local assumptions can be quite tricky, but <a href="https://doi.org/10.1017/S0956796811000098" rel="nofollow noreferrer">Modular type inference with local assumptions</a> (<a href="https://scholar.archive.org/work/bdcqy3psnbedjikkygrncvwhqa/access/wayback/http://research.microsoft.com:80/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf" rel="nofollow noreferrer">pdf</a>) provides an detailed overview.</p>
<h2>Challenges, alternatives, and loose ends</h2>
<p>While the above description provides a decent sketch of the idea, it is somewhat simplified in that it associates the lacks constraint with a particular label when in fact the exclusion must be mutual. That is, it does not suffice to check that <span class="math-container">$\rho$</span> lacks <span class="math-container">$\mathsf{y}$</span> when <span class="math-container">$\mathsf{x}$</span> is added to a record, but it is also necessary to check that <span class="math-container">$\rho$</span> lacks <span class="math-container">$\mathsf{x}$</span> when <span class="math-container">$\mathsf{y}$</span> is. If records are <em>not</em> extensible (that is, labels cannot be added to an existing record unless all of its labels are statically known), this is not a problem, as checking exclusion in one direction is sufficient. But if polymorphic extension is permitted, you would need to take care to infer the appropriate constraints on excluded labels.</p>
<p>However, this introduces a new quandary: if a label to be considered mutually exclusive may be defined in a yet-to-be-defined module (that is, we take an “open world” assumption), it is impossible to know at any given record construction site which lacks constraints we must enforce! Therefore, <em>some</em> restriction on where/how this mutual exclusiveness may be defined is probably necessary. An easy approach would be to require that both labels be declared in the same module.</p>
<p>Finally, a different approach altogether would be to associate the constraints with a given row type rather than with the labels. In that case, you might allow constrained types like
<span class="math-container">$$
(\mathsf{x} ⊕ \mathsf{y} ∈ \rho) \Rightarrow \mathsf{Record}\ \rho
$$</span>
where <span class="math-container">$⊕$</span> is read as “XOR”. In this case, your constraint solver would need to have inference rules like the following:
<span class="math-container">$$\begin{array}{l}
\begin{array}{l}
⊢ \ell_1 ∈ \rho \\
⊢ \ell_2 ∉ \rho \\
\hline
⊢ \ell_1 ⊕ \ell_2 ∈ \rho
\end{array}
\begin{array}{l}\\ [\textsf{XOR-intro}]\end{array}\\
%
\begin{array}{l}
⊢ \ell_1 ⊕ \ell_2 ∈ \rho \\
⊢ \ell_1 ∈ \rho \\
\hline
⊢ \ell_2 ∉ \rho
\end{array} \begin{array}{l}\\ [\textsf{XOR-elim}]\end{array}\\
\end{array}$$</span>
When constructing the record, the <span class="math-container">$\textsf{XOR-intro}$</span> rule would be used to satisfy the constraint. When pattern matching on a record, a match would supply the necessary <em>has</em> constraint as a local assumption, so the <span class="math-container">$\textsf{XOR-elim}$</span> rule could derive the corresponding lacks constraint, permitting bidirectional flow of information.</p>
<p>But be cautious! This approach also runs into some trouble if you allow adding labels after the record has already been constructed, since the constraint may have already been discharged. So you’d need to do some extra work to ensure the property holds globally, which could quickly make the system difficult to use. Such is the pain of proving a negative.</p>

CC BY-SA 4.0
2023-06-30T06:04:49.850Z
2023-08-11T17:23:53.620Z
2023-08-11T17:23:53.620Z
Alexis King
# How can I have mutually-exclusive properties in a structural type system?
Posted by: username_0 on 2023-05-25
I have a structurally-typed object-oriented language, and I'd like to allow for types with some mutually-exclusive properties/attributes/slots/methods. That is, an object having *more than one* of these properties, or none of them, does not belong to the type. There could also be other ordinary properties within the types, which would be required as normal.

Clearly these wouldn't be accessible on the type itself, but you'd know that if you found one of them then the others weren't there, so that for example typecase pattern-matching on them all would be exhaustive and order-independent.

Ideally I'd like for this to be sound, but it does break ordinary subsumption so it may be necessary to accept some level of breakage, dynamic enforcement, or both, and I'd like to know what that is. In some respects this is related to [this question](https://languagedesign.stackexchange.com/q/952/133) about optional properties, but this is concerned with the interplay between multiple properties within the same type.
**Tags:** types static-typing structural-types soundness
> **Comments:**
> **username_1**: I have to ask though: how would you use such a type? Knowing that `a` is present means you can access it. Knowing that `a` is absent means you don't need to implement it. But what can you do with an object where you know that exactly one of `a` and `b` is present, that doesn't require discriminating between the two cases (in which case you'd just take a discriminating union of the a and b versions)?  
> **username_0**: I am imagining a typecase or multimethod scenario that does eventually discriminate, but intermediately only the shared properties are in use. A tagged union is how I might express this disjunction in another environment, but those are further outside of a structural type that a suitable value can flow into ad-hoc. In a partially-typed system it can be possible for an "extra" property to be accessible somewhere, so I want ruling it out in the types to actually rule out belonging to two classes. I'm also alive to multiple sets in the same type, but I don't want to complicate this more now (yet)  
> **username_2**: I suspect the answer involves [row polymorphism](https://en.wikipedia.org/wiki/Row_polymorphism), which allows representing types like `{x: number, empty}` and `{x: number, ρ}` where `ρ` is a row parameter. In the notation from Wikipedia, mutually exclusive properties might be written as a union type like `{x: number, absent(y), ρ} | {y: string, absent(x), ρ}`. I'm not really knowledgeable enough to write more on the subject, but if this is useful enough then I can convert it from a comment to an answer.  
> **username_1**: @kaya3 Row polymorphism treats each property independently. You'd need an extension to describe interactions between properties. A non-discriminated union works, but then you need to have non-discriminated unions in your type system and that's hard in a static type system.  
> **username_2**: @Gilles'SO-stopbeingevil' Indeed, this approach would require more than just row polymorphism; I'm thinking about the question from the perspective of Typescript, which has one of the most expressive static structural type systems but lacks soundness particularly for this kind of type. Since Typescript already has undiscriminated union types, row polymorphism would be the necessary additional feature.  
> **username_3**: I might misunderstand the question, but it seems to me that you want to have a discriminated-variant field (like Rust's `enum`, or C++'s `std::variant`). Then that field could be exactly one of the alternatives in any given object  
> **username_0**: @abel1502 I'm not sure that would help - even for a field, a variant type would allow the concrete value to change dynamically between different variants at run time, so you couldn't rely on a previous check still holding. For methods it probably wouldn't work at all (although in a JavaScript-style model these are conflated, so maybe).  
> **username_1**: @MichaelHomer I don't understand your last comment. A discriminated union (aka variant) trivialises the problem (using row polymorphism, which is the basic tool to describe which properties an object has) — the type is just something like `Has_a_not_b {a: int; b: absent; 'rest} | B {a: absent; b: float; 'rest}`. You can do that with a non-discriminated union, but that opens the can of worms of non-discriminated unions.  
> **username_0**: @Gilles'SO-stopbeingevil' The last comment was replying to a suggestion of using a single variant-typed field (as I read it, anyway), which I don't think helps, at least directly. You could nest the properties one layer deep in the values, I suppose.  
> **username_0**: Row polymorphism is likely to be part of an answer, yes, and I'm asking about how far-reaching the effects of these types would have to be.  
---
## 1 answers
### Answer by username_4 on 2023-06-30. Score: 9 | Accepted answer
## Enforcing exclusion

Some inspiration for a system that works this way can be found in [Extensible Records Without Subsumption](https://doi.org/10.1184/R1/6605507.v1) ([pdf](https://scholar.archive.org/work/jg7m6qdnpraynhid6rwvuj2n3i/access/wayback/https://s3-eu-west-1.amazonaws.com/pstorage-cmu-348901238291901/12095981/file.pdf)) by Bob Harper and Benjamin Pierce. They present extensible records via row polymorphism, which your comments on your question indicate you are already familiar with, but the paper also includes the notion of a *lacks* constraint. From the introduction:

> For example, Cardelli and Mitchell’s record extension operator is only defined on records where the field being added is not already present; to prevent run time type errors, the typing rule for the extension operator must check that this is the case. We found it simpler to express this constraint directly as “$r$ lacks $l$” instead of encoding it as “$r$ is less than some type lacking $l$.”

Their system allows quantified type variables to be constrained by both these negative *lacks* constraints as well as positive *has* constraints. Lacks constraints provide some of the basic material necessary to implement the mutual exclusion property you’re looking for, and in fact, they’re already sufficient to guarantee it is maintained. To see how, let’s consider a “label declaration” that binds a name that can be used as a label in a record:
$$
\mathbf{label}\ \mathsf{x} : \mathsf{T}
$$
This declares $\mathsf{x}$ as a record label for a value of type $\mathsf{T}$. We can imagine extending this declaration with support for constraints:
$$\begin{array}{l}
\mathbf{label}\ (\mathsf{x} : \mathsf{T}) ∈ \rho \\
\quad \mathbf{where}\ \mathsf{y} ∉ \rho
\end{array}$$
This can be read as “$\mathsf{x}$ is a label for a value of type $\mathsf{T}$ in some row type $\rho$ such that $\rho$ lacks label $\mathsf{y}$.” When a record is constructed using this label, the $\mathsf{y} \notin \rho$ constraint would be generated, and a constraint solver would need to be able to somehow solve it in order for the program to be accepted.

## Exposing exclusion

This is enough to *enforce* the property, but it is not quite enough to truly leverage it. In your question, you state

> You'd know that if you found one of them then the others weren't there, so that for example typecase pattern-matching on them all would be exhaustive and order-independent.

which requires that we *gain* information by pattern matching. This requires something a bit stronger: *local assumptions*, which are most commonly associated with generalized algebraic data types (GADTs). GADTs offer precisely the sort of property we’re looking for, namely that matching on a constructor can introduce local constraints (i.e. assumptions) only available within the pattern match’s right hand side. For example, we might write the Haskell datatype
$$\begin{array}{l}
\mathbf{data}\;\mathsf{SomeShowable}\ a\;\mathbf{where} \\
\quad \mathsf{MkSomeShowable} :: \mathsf{Show}\ a \Rightarrow a \rightarrow \mathsf{SomeShowable}\ a
\end{array}$$
which “contains” a $\mathsf{Show}$ constraint, so pattern matching on the $\mathsf{MkSomeShowable}$ constructor brings that constraint into scope.

Although these constrained labels aren’t quite GADTs, they can be typechecked using the same principles. Since the constraint must be satisfied for each record they’re added to, a record containing the label serves as a proof that all the constraints must hold, and a local constraint can be brought into scope. Implementing a typechecker that supports local assumptions can be quite tricky, but [Modular type inference with local assumptions](https://doi.org/10.1017/S0956796811000098) ([pdf](https://scholar.archive.org/work/bdcqy3psnbedjikkygrncvwhqa/access/wayback/http://research.microsoft.com:80/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf)) provides an detailed overview.

## Challenges, alternatives, and loose ends

While the above description provides a decent sketch of the idea, it is somewhat simplified in that it associates the lacks constraint with a particular label when in fact the exclusion must be mutual. That is, it does not suffice to check that $\rho$ lacks $\mathsf{y}$ when $\mathsf{x}$ is added to a record, but it is also necessary to check that $\rho$ lacks $\mathsf{x}$ when $\mathsf{y}$ is. If records are *not* extensible (that is, labels cannot be added to an existing record unless all of its labels are statically known), this is not a problem, as checking exclusion in one direction is sufficient. But if polymorphic extension is permitted, you would need to take care to infer the appropriate constraints on excluded labels.

However, this introduces a new quandary: if a label to be considered mutually exclusive may be defined in a yet-to-be-defined module (that is, we take an “open world” assumption), it is impossible to know at any given record construction site which lacks constraints we must enforce! Therefore, *some* restriction on where/how this mutual exclusiveness may be defined is probably necessary. An easy approach would be to require that both labels be declared in the same module.

Finally, a different approach altogether would be to associate the constraints with a given row type rather than with the labels. In that case, you might allow constrained types like
$$
(\mathsf{x} ⊕ \mathsf{y} ∈ \rho) \Rightarrow \mathsf{Record}\ \rho
$$
where $⊕$ is read as “XOR”. In this case, your constraint solver would need to have inference rules like the following:
$$\begin{array}{l}
\begin{array}{l}
⊢ \ell\_1 ∈ \rho \\
⊢ \ell\_2 ∉ \rho \\
\hline
⊢ \ell\_1 ⊕ \ell\_2 ∈ \rho
\end{array}
\begin{array}{l}\\ [\textsf{XOR-intro}]\end{array}\\
%
\begin{array}{l}
⊢ \ell\_1 ⊕ \ell\_2 ∈ \rho \\
⊢ \ell\_1 ∈ \rho \\
\hline
⊢ \ell\_2 ∉ \rho
\end{array} \begin{array}{l}\\ [\textsf{XOR-elim}]\end{array}\\
\end{array}$$
When constructing the record, the $\textsf{XOR-intro}$ rule would be used to satisfy the constraint. When pattern matching on a record, a match would supply the necessary *has* constraint as a local assumption, so the $\textsf{XOR-elim}$ rule could derive the corresponding lacks constraint, permitting bidirectional flow of information.

But be cautious! This approach also runs into some trouble if you allow adding labels after the record has already been constructed, since the constraint may have already been discharged. So you’d need to do some extra work to ensure the property holds globally, which could quickly make the system difficult to use. Such is the pain of proving a negative.
---
