A motivator for supporting ability sets where multiple abilities share the same head type constructor

h-o-exception-ability.md

This is a case that might help motivate support in Unison for ability sets where multiple abilities share the same head type constructor.

In a nutshell the point is that ability sets like {Exception Foo, Exception Bar} arise naturally when composing functions. So weak support for those ability sets bakes a barrier to compositionality into the language.

Let's suppose we're using the Exception ability.

ability Exception e where
  throw : e -> a

And suppose we have a higher order function that uses this ability.

mappy : (A ->{e} B) -> AA ->{e, Exception Foo} BB

Let's use it, together with another function - but one that uses the Exception Bar ability.

f : A ->{Exception Bar} B
f = (whatever)

eg1 : AA ->{Exception Bar, Exception Foo} BB
eg1 = mappy f

eg1 ends up with the kind of ability set we're talking about. OK maybe you might say people should work with Exception (Either Foo Bar) - but they're only going to be able to translate to that type after they've done mappy f.

I started off with the higher order example because I think it better illustrates the point that a natural code structure can lead to this case. You might write mappy without any prior suspicion that people will apply it to functions that also use Exception.

Here's another example - just straight composition this time.

p : A ->{Exception Foo} B
p = (whatever)

q : B ->{Exception Bar} C
p = (whatever)

eg2 : A ->{Exception Foo, Exception Bar} C
eg2 x = q (p x)

Trying to step back a bit (this paragraph is a bit speculative): I wonder whether a problem with the current limitation is that it allows internal structure of a type to leak out during typechecking, in a way other than through pattern matching on it. I can observe a difference between an Exception Foo and a Baz, by how they interact with Exception Bar when sharing an ability set. Seems a bit janky somehow, but I can't really say why. I guess it breaks my feeling that a type constructor like Exception allows me to form 'first class' types when I apply it to things.

---

-- full code for the above

ability Exception e where
  throw : e -> a

-- A higher order function that can throw.
mappy : (A ->{e} B) -> AA ->{e, Exception Foo} BB
mappy _ _ = hole ()

f : A ->{Exception Bar} B
f _ = hole ()

eg1 : AA ->{Exception Bar, Exception Foo} BB
eg1 = mappy f

p : A ->{Exception Foo} B
p _ = hole ()

q : B ->{Exception Bar} C
q _ = hole ()

-- (the following doesn't compile today)
--eg2 : A ->{Exception Foo, Exception Bar} C
--eg2 x = q (p x)

-- boring stuff follows

hole _ = hole ()

unique type Foo = Foo Nat
unique type Bar = Bar Text

unique type A = A
unique type B = B
unique type C = C
unique type AA = AA
unique type BB = BB