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

[Matthew Johnson]

Very interesting reading, thanks Joe.  I have stumbled across Koka in the past when reading about effect systems and thought it looked like a really strong approach with many advantages.

I'm wondering how a couple of examples would behave under this approach.

If we have the following:
func foo( bar: ()->() throws T, U)
func baz() throws U, T
foo(baz)

Is the last statement valid?  It seems like the permutation would cause an unintuitive and problematic compiler error but maybe it is resolved somehow?

Also consider the following:

enum T: ErrorType { case A, case B }
enum U: ErrorType { case C }
func foo() throws T, U, T

do {
   Try foo()
} catch U.C {
} catch T.A {
} catch T.B {
}

Have we exhaustively handled all errors even though T appears twice in the type of foo and the catch clauses are not in the same order as T, U, T in the type of foo?  I don't think anyone would declare a foo like this, but maybe a function could end up with a type like this by rethrowing, etc.

Matthew

Sent from my iPad

> On Dec 12, 2015, at 1:36 PM, Joe Groff <jgroff at apple.com> wrote:
> 
> 
>>> On Dec 12, 2015, at 10:58 AM, Matthew Johnson <matthew at anandabits.com> wrote:
>>> 
>>> 
>>> 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.
>>> 
>> 
>> Did you mean "(T | U | V) and (U | T | V) would be distinct types, just like (T, U, V) and (U, T, V) are distinct product types."?
> 
> I meant that T | U | V, T | T | U | V, and U | T | V are all different.
> 
>> In the typed throws with multiple error types use case I think most developers would intuitively expect all permutations of error types to mean the same thing:
>> ()->() throws T, U, V
>> ()->() throws U, T, V
>> etc
>> 
>> I haven't given a lot of thought to other use cases but I my instinct is that the same intuition would apply.  I'm not sure that order provides a meaningful distinction for structural sum types.  I would like to learn about any use cases where the distinction would be meaningful if anyone knows of any.
>> 
>> If order doesn't provide a useful and meaningful distinction or if it contradicts intuition in the most prevalent and compelling use cases maybe syntactic permutations should be irrelevant.  A projection of syntax to a canonical order could be performed such that (U | T | V) is projected to (T | U | V) and the type system never encounters any of the other permutations.  
>> 
>> If we do this we probably don't want to expose cases of .0(T), etc as the canonical order be an implementation detail.  The constituent types of the union type would naturally be subtypes of the union type so dynamic cast could be used for projection instead. 
> 
> Order invariance is manageable. There are reasons *not* to coalesce equivalent effects, depending on the type system model. For reference, Koka doesn't attempt to coalesce equivalent effects, both because it would complicate the type system, and because it makes operations like 'catch' easier to type:
> 
> http://research.microsoft.com/pubs/210640/paper.pdf
> 
> Our effect rows differ in an important way from the usual approaches in that effect labels can be dupli- cated, i.e. ⟨exn, exn⟩ ̸≡ ⟨exn⟩ (1). This was first described by Leijen [17] where this was used to enable scoped labels in record types. Enabling duplicate labels fits our approach well: first of all, it enables principal unification without needing extra constraints, and secondly, it enables us to give precise types to effect elimination forms (like catching exceptions).
> 
> In particular, during unification we may end up with constraints of the form ⟨exn|μ⟩ ∼ ⟨exn⟩. With regular row-polymorphism which are sets of labels, such constraint can have multiple solutions, namely μ = ⟨⟩ or μ = ⟨exn⟩. This was first observed by Wand [43] in the context of records. Usually, this problem is fixed by either introducing lacks constraints [7] or polymorphic presence and absence flags on each label [32] (as used by Lindley and Cheney [23] for an effect system in the context of database queries). The problem with both approaches is that they complicate the type system quite a bit. With lacks contstraints we need a system of qualified types as in Haskell, while with presece and absence flags, we need a kind system that tracks for each type variable which labels cannot be present.
> 
> With rows allowing duplicate labels, we avoid any additional machinery and can use straight forward type inference techniques. In our case μ = ⟨⟩ is the only solution to the above constraint (due to (1)).
> 
> Moreover, duplicate labels make it easy to give types to effect elimination forms. For example, catching effects removes the exn effect:
> 
> catch : ∀αμ.(()→⟨exn|μ⟩α, exception→μ α)→μ α
> 
> Here we assume that catch takes two functions, the action and the exception handler that takes as an argument the thrown exception. The exn effect of the action is discarded in the final effect μ since all exceptions are caught by the handler. But of course, the handler can itself throw an exception and have an exn effect itself. In that case μ will unify with a type of the form ⟨exn|μ′⟩ giving action the effect ⟨exn|exn|μ′⟩ where exn occurs duplicated, which gives us exactly the right behavior. Note that withlacks constraints we would not be able to type this example because there would be a exn ̸∈ μ constraint. We can type this example using flags but the type would arguably be more complex with a polymorphic presence/absence flag φ on the exn label in the result effect, something like:
> 
> catch : ∀μαφ. (() → ⟨exn•| μ⟩ α, exception → ⟨exnφ | μ⟩ α) → ⟨exnφ | μ⟩ α
> 
> There is one situation where an approach with flags is more expressive though: with flags one can state specifically that a certain effect must be absent. This is used for example in the effect system by Lindley and Cheney [23] to enforce that database queries never have the wild effect (io). In our setting we can only enforce absence of an effect by explicitly listing a closed row of the allowed effects which is less modular. In our current experience this has not yet proven to be a problem in practice though but we may experiment with this in the future. 
> 
> 
> -Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20151212/67a833f9/attachment.html>