mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-21 07:17:25 +03:00
a5b978daab
- Previously the results could depend on the order that wanted abilities were tested against provided abilities. The new approach runs until a fixed point is reached, allowing some unifications on concrete abilities to better inform the overall process.
1.3 KiB
1.3 KiB
Tests for an ability failure that was caused by order dependence of checking wanted vs. provided abilities. It was necessary to re-check rows until a fixed point is reached.
unique ability C c where
new : c a
receive : c a -> a
send : a -> c a -> ()
unique ability A t g where
fork : '{A t g, g, Exception} a -> t a
await : t a -> a
unique ability Ex where raise : () -> x
Ex.catch : '{Ex, g} a ->{g} Either () a
Ex.catch _ = todo "Exception.catch"
C.pure.run : (forall c . '{C c, g} r) ->{Ex, g} r
C.pure.run _ = todo "C.pure.run"
A.pure.run : (forall t . '{A t g, g} a) ->{Ex,g} a
A.pure.run _ = todo "A.pure.run"
ex : '{C c, A t {C c}} Nat
ex _ =
c = C.new
x = A.fork 'let
a = receive c
a + 10
y = A.fork 'let
send 0 c
()
A.await x
x : '{} (Either () Nat)
x _ = Ex.catch '(C.pure.run '(A.pure.run ex))
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
unique ability A t g
unique ability C c
unique ability Ex
A.pure.run : (∀ t. '{g, A t g} a) ->{g, Ex} a
C.pure.run : (∀ c. '{g, C c} r) ->{g, Ex} r
Ex.catch : '{g, Ex} a ->{g} Either () a
ex : '{C c, A t {C c}} Nat
x : 'Either () Nat