Binding Against Union Types

[DavePearce]

There are currently some problems related to the way that binding occurs against union types. The following illustrates:

function select<S,T>(S|T x, S y) -> (S|T r):
    if x == y:
        return y
    else:
        return x

public export method test():
    int|bool a1 = (int|bool) 1
    //
    assume select(a1,1) == 1

The essential problem is that we have three possible bindings and no clear winner:

• S=int T=bool --- this is the natural binding we expect
• S=(int|bool) T=bool --- this is also a valid binding though is perhaps not "natural" per se
• S=int T=(int|bool) --- another valid binding

The challenge here is that all three lead to essentially equivalent concrete lambda types and, hence, we have no clear way to distinguish them.

The above example contrasts with one such as this:

function join<S,T>(S s, T t) -> (S|T r):
    return s

public export method test():
    assume join(1,1) == 1

In this example, we want int|int to boil down to int.

[DavePearce]

UPDATE: I guess an interesting question is whether or not a type like S|T should ever be considered to make sense. The logic goes like this:

1. A type T is a universal type and hence can represent any possible type.
2. A type S|T is combining two universal types and, hence, many combinations clearly do not make sense. For example, should we allow int|int ?

[DavePearce]

UPDATE: The issue with select essentially boils down the following observation:

We know which function is being called, and we have multiple valid bindings. The only question is: which one to pick?

For example, one approach was to pick a binding which strictly subsumes all others. However, this is not enough for select(). But, other approaches could work (e.g. choose the smallest binding).