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