Is there a generally accepted name for creating types that select a subset of other types?

Question

Tl;Dr;

Given:

type A = { int: foo, int: bar }
type B = select foo from A

• What is the name of the typing relationship between A and B?
• What is the name of the operation of deriving type B from type A?

---

Long Version

When we talk of subtyping in programming we typically think of it in terms of whether a new subtype B of a type A is able to substitute for A. However, when you think of it in terms of implementation what you are actually saying is that B can do everything that A can. Typically B does more. It might implement the interface and add new fields and methods of its own. So despite 'sub' sounding like 'subset' the relationship is more like the subtype enriching the supertype. We derive the subtype from the supertype. I'm curious about deriving a new type by selecting a subset instead.

Consider two structures:

A = { int: foo, int: bar }
B = { int: foo }

The fields of B are a subset of the fields of A.

Is there a proper name for this relationship? I would say A includes B.

You could implement A by embedding an instance of B. As in:

C = { B, int: bar }

In a language like Go, C is the same as A. In other languages you need to reference B to get to foo. i.e. C.B.foo rather than C.foo

Another kind of subset relation is subranging. For instance limiting a integer to a range of 0-10.

Q = int
P = int[0..10]

P is a subset of Q as before. You can still say Q includes P. subranges are a special case of refinement types.

The main language I can think of where creating subsets is central is SQL. We could define B as:

B = select foo from A 

So selection is probably a better term to use than "sub-setting"? B is not a subtype of A is it cannot be used as a substitute for A. A is a subtype of B because it can be. So B is a supertype of A. I think this misses the essential distinction that we are deriving B from A rather than the other way around. i.e. the process has a direction:

B = f(A) , where f = selection and B is a supertype of A

vs

subtype = g(supertype), where g is derivation/inheritance.

We also have intersection types which combine two types by producing the subset they have in common. SQL does this with joins. Unification in prolog has a similar effect. Selection is via intersection with a second type. You could view selecting the fields as constructing a set of selectors and which is then intersected with the original set. I'm not sure this is the correct way to look at it though. selection and intersection are not the same. An intersection ignores fields that are not common a selection operation should treat that as an error.

There is also destructuring (assignment) as in:

let x = { 10, 1 }
{y, z} = x

But this has to do with values more than types and the isomorphism between a structure and a generic tuple.

My question is:

• Is there a generally accepted name for this kind of 'selection'?
• What would you call a type system supporting this kind of relationship?

Bonus discussion questions:

• Why is 'selection' not more common in general purpose programming languages as opposed to query languages? Surely they complement each other well?

• Are there any interesting languages supporting this? How successful is the feature? (linq is very successful in C# for example)

Answer 1

First, the field-subset model of subtyping, while uncommon in OO languages, is common in PL theory for modelling subtyping. It's often called row subtyping.

I'm not sure if there's a general name for all the other things you've described, but I think the closest fit is refinement types, which come in many flavours.

• Liquid types refine types by a boolean predicate, i.e. you can make a type which contains all values from another type satisfying a certain predicate. For example, you could have $\{ i : Int \mid 0 < i < 10 \}$ as a refinement of $Int$.
• Datasort Refinements are similar to liquid types, but they constrain a type by the shape of its values. So, you can refine $(List\ Int)$ to $ T = Cons(Int, Cons(Int, List))$, and $T$ is then the type of all $Int$-containing lists of length 2 or more.

More generally, Set-theoretic types describe a system where can form types using intersection, union, and negation operations on existing types. Here, there is a close correspondence between subtyping and the subset-relationship between values in a type.

A general comment is that I think you need to be careful distinguishing terms from types. While you're describing sensible operations on types, the SQL example and the Prolog unification example are both operations on terms, and not on types, so they're really something different from what you're describing.

I don't think destructuring assingment has anything to do with the other things, it's just a shorthand for pattern-matching, either where there's only one case, or where we throw an error in all but one case.

Bonus Discussion

Why is this not common? Type-checking is performed often, and adding too many features makes it undecidable. The refinement-types I listed above depend on SMT-solvers for typechecking, since they require solving logical constraints.

Are there langauges that support these? The main ones I can think of are Liquid Haskell and Dependent ML. I'm not sure how often they show up in an object-oriented context, because these are areas under active research, and functional languages are generally faster to incorporate bleeding-edge ideas from PL research.