mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 10:35:57 +03:00
45 lines
913 B
Markdown
45 lines
913 B
Markdown
|
|
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.
|
|
|
|
```ucm:hide
|
|
scratch/main> builtins.merge
|
|
```
|
|
|
|
```unison
|
|
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))
|
|
```
|