<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><div>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.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">I'm wondering how a couple of examples would behave under this approach.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">If we have the following:</div><div id="AppleMailSignature">func foo( bar: ()->() throws T, U)</div><div id="AppleMailSignature">func baz() throws U, T</div><div id="AppleMailSignature"><span style="background-color: rgba(255, 255, 255, 0);">foo(baz)</span></div><div id="AppleMailSignature"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></div><div id="AppleMailSignature">Is the last statement valid? It seems like the permutation would cause an unintuitive and problematic compiler error but maybe it is resolved somehow?</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Also consider the following:</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">enum T: ErrorType { case A, case B }</div><div id="AppleMailSignature">enum U: ErrorType { case C }</div><div id="AppleMailSignature">func foo() throws T, U, T</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">do {</div><div id="AppleMailSignature"> Try foo()</div><div id="AppleMailSignature">} catch U.C {</div><div id="AppleMailSignature"><div id="AppleMailSignature"><span style="background-color: rgba(255, 255, 255, 0);">} catch T.A {</span></div><div id="AppleMailSignature"><span style="background-color: rgba(255, 255, 255, 0);">} catch T.B {</span></div></div><div id="AppleMailSignature">}</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">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.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Matthew</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Sent from my iPad</div><div><br>On Dec 12, 2015, at 1:36 PM, Joe Groff <<a href="mailto:jgroff@apple.com">jgroff@apple.com</a>> wrote:<br><br></div><blockquote type="cite"><div><meta http-equiv="Content-Type" content="text/html charset=utf-8"><br class=""><div><blockquote type="cite" class=""><div class="">On Dec 12, 2015, at 10:58 AM, Matthew Johnson <<a href="mailto:matthew@anandabits.com" class="">matthew@anandabits.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class=""><br class=""><blockquote type="cite" class="">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.<br class=""><br class=""></blockquote><br class="">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."?<br class=""></div></div></blockquote><div><br class=""></div>I meant that T | U | V, T | T | U | V, and U | T | V are all different.<br class=""><div><br class=""></div><blockquote type="cite" class=""><div class=""><div class="">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:<br class="">()->() throws T, U, V<br class="">()->() throws U, T, V<br class="">etc<br class=""><br class="">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.<br class=""><br class="">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. <br class=""><br class="">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. <br class=""></div></div></blockquote></div><br class=""><div class="">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:</div><div class=""><br class=""></div><div class=""><a href="http://research.microsoft.com/pubs/210640/paper.pdf" class="">http://research.microsoft.com/pubs/210640/paper.pdf</a></div><div class=""><br class=""></div><div class="">
<div class="page" title="Page 5">
<div class="layoutArea">
<div class="column"><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">Our effect rows differ in an important way from the usual approaches in that effect labels can be dupli-
cated, i.e. </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMMI10'" class="">, </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ ̸≡ ⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11pt; font-family: NimbusRomNo9L;" class="">(1)</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">. This was first described by Leijen [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">17</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] 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).
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">In particular, during unification we may end up with constraints of the form </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">|</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ ∼ ⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">. With
regular row-polymorphism which are sets of labels, such constraint can have multiple solutions, namely
</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">= </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨⟩ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">or </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">= </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">. This was first observed by Wand [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">43</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] in the context of records. Usually, this
problem is fixed by either introducing </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">lacks </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">constraints [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">7</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] or polymorphic presence and absence flags
on each label [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">32</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] (as used by Lindley and Cheney [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">23</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] 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
</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">lacks </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">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.
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">With rows allowing duplicate labels, we avoid any additional machinery and can use straight forward
type inference techniques. In our case </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">= </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨⟩ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">is the only solution to the above constraint (due to (1)).
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">Moreover, duplicate labels make it easy to give types to effect elimination forms. For example,
catching effects removes the </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">effect:
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">catch </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">: </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">∀</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">αμ</span><span style="font-size: 11.000000pt; font-family: 'CMMI10'" class="">.</span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">(()</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">|</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">α</span><span style="font-size: 11.000000pt; font-family: 'CMMI10'" class="">, </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exception</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ α</span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">)</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ α
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">Here we assume that </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">catch </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">takes two functions, the action and the exception handler that takes as an
argument the thrown </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exception</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">. The </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">effect of the action is discarded in the final effect </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">since all
exceptions are caught by the handler. But of course, the handler can itself throw an exception and have
an </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">effect itself. In that case </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">will unify with a type of the form </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">|</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 8.000000pt; font-family: 'CMSY10'; vertical-align: 4.000000pt" class="">′</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">giving action the effect
</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">|</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">|</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 8.000000pt; font-family: 'CMSY10'; vertical-align: 4.000000pt" class="">′</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">where </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">occurs duplicated, which gives us exactly the right behavior. Note that with</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">lacks
</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">constraints we would not be able to type this example because there would be a </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class=""≯∈ </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">constraint. We
can type this example using flags but the type would arguably be more complex with a polymorphic
presence/absence flag </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">φ </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">on the </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">label in the result effect, something like:
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">catch </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">: </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">∀</span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μαφ</span><span style="font-size: 11.000000pt; font-family: 'CMMI10'" class="">. </span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">(() </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→ ⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 8.000000pt; font-family: 'CMSY10'; vertical-align: -2.000000pt" class="">•</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">| </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">α</span><span style="font-size: 11.000000pt; font-family: 'CMMI10'" class="">, </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exception </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→ ⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 8.000000pt; font-family: 'StandardSymL'; vertical-align: -2.000000pt" class="">φ </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">| </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">α</span><span style="font-size: 11.000000pt; font-family: 'CMR10'" class="">) </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">→ ⟨</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">exn</span><span style="font-size: 8.000000pt; font-family: 'StandardSymL'; vertical-align: -2.000000pt" class="">φ </span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">| </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">μ</span><span style="font-size: 11.000000pt; font-family: 'CMSY10'" class="">⟩ </span><span style="font-size: 11.000000pt; font-family: 'StandardSymL'" class="">α
</span></p><p class=""><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">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 [</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; color: rgb(0.000000%, 0.000000%, 50.195000%)" class="">23</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">] to enforce that database queries never have the </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">wild </span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">effect (</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'; font-style: italic" class="">io</span><span style="font-size: 11.000000pt; font-family: 'NimbusRomNo9L'" class="">). 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. </span></p><div class=""><br class=""></div><div class="">-Joe</div>
</div>
</div>
</div></div></div></blockquote></body></html>