11
$\begingroup$

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 about optional properties, but this is concerned with the interplay between multiple properties within the same type.

$\endgroup$
10
  • 1
    $\begingroup$ 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)? $\endgroup$ May 25, 2023 at 8:52
  • 1
    $\begingroup$ 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) $\endgroup$
    – Michael Homer
    May 25, 2023 at 9:09
  • $\begingroup$ I suspect the answer involves 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. $\endgroup$
    – kaya3
    May 25, 2023 at 10:08
  • 2
    $\begingroup$ @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. $\endgroup$ May 25, 2023 at 10:31
  • $\begingroup$ @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. $\endgroup$
    – kaya3
    May 25, 2023 at 10:38

1 Answer 1

9
$\begingroup$

Enforcing exclusion

Some inspiration for a system that works this way can be found in Extensible Records Without Subsumption (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 (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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .