[swift-evolution] Proposal: An Either Type in the STL

[John McCall]

> On Dec 12, 2015, at 10:01 AM, Joe Groff <jgroff at apple.com> wrote:
>> On Dec 10, 2015, at 6:14 PM, John McCall <rjmccall at apple.com> wrote:
>> 
>>> On Dec 10, 2015, at 6:05 PM, Joe Groff <jgroff at apple.com> wrote:
>>>> On Dec 10, 2015, at 5:59 PM, Matthew Johnson <matthew at anandabits.com> wrote:
>>>> 
>>>> 
>>>>> Structural sum types containing dependent types.
>>>> 
>>>> Dependent in what sense?  Swift doesn't support anything like dependent types in the usual sense of being dependent on a value (modulo the pretty limited ability to abuse the type system).
>>> 
>>> I think John means 'dependent' in the more prosaic C++ sense of 'dependent on generic type parameters', e.g. 'Array<T>' inside a function generic on <T>, not dependent types in the Coq/Agda/Idris sense.
>> 
>> Right, sorry; I’ve gotten too used to the C++ sense.  I mean types which contain free uses of the generic parameters of the context, which therefore appear to be opaque there.  It’s a problem for union typing because the intersection of any opaque types with the other concrete types in a union is not necessarily empty.  It’s not an unsolvable problem, of course.
> 
> A structural sum type that was a disjoint sum and strictly ordered seems reasonably easy to support, if not perfectly ergonomic, and would handy if we ever get variadic generics, and better than the Either towers Haskellers construct for abstract anonymous sums. You could say that (T | U | V) behaves like an enum with cases .0(T), .1(U), .2(V); maybe you get implicit conversion in cases where the type-to-tag association is unambiguous. (T | T | U | V) and (U | T | V) would be distinct types, just like (T, U, V) and (U, T, V) are distinct product types.

That is easy to support, but it is completely different from what Ceylon supports, which is true structural union-typing, including implicit injection and union-lookup.  Although they seem to structurally demand disjointness for some reason that escapes me; avoidance of programmer confusion, perhaps?

Ceylon is, of course, a JVM language, which means it is just providing additional type accuracy over java.lang.Object.  To support their model reasonably, we would have to use a representation closer to Any.

Anyway, proposals to add new kinds of structural types will require a lot more motivation than I’m seeing here.

John.