2021-08-31 00:25:30 +03:00
|
|
|
|
Tests for a loop that was previously occurring in the type checker.
|
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
|
``` unison
|
2021-08-31 00:25:30 +03:00
|
|
|
|
structural ability A t g where
|
|
|
|
|
fork : '{g, A t g} a -> t a
|
|
|
|
|
await : t a -> a
|
|
|
|
|
empty! : t a
|
|
|
|
|
put : a -> t a -> ()
|
|
|
|
|
|
|
|
|
|
example : '{A t {}} Nat
|
|
|
|
|
example = 'let
|
|
|
|
|
r = A.empty!
|
|
|
|
|
go u =
|
|
|
|
|
t = A.fork '(go (u + 1))
|
|
|
|
|
A.await t
|
|
|
|
|
|
|
|
|
|
go 0
|
|
|
|
|
t2 = A.fork '(A.put 10 r)
|
|
|
|
|
A.await r
|
|
|
|
|
```
|
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
|
``` ucm
|
2021-08-31 00:25:30 +03:00
|
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
|
2021-08-31 00:25:30 +03:00
|
|
|
|
I tried to infer a cyclic ability.
|
|
|
|
|
|
|
|
|
|
The expression in red was inferred to require the ability:
|
|
|
|
|
|
2024-06-25 22:54:10 +03:00
|
|
|
|
{A t25 {𝕖36, 𝕖18}}
|
2021-08-31 00:25:30 +03:00
|
|
|
|
|
|
|
|
|
where `𝕖18` is its overall abilities.
|
|
|
|
|
|
2021-08-31 18:17:11 +03:00
|
|
|
|
I need a type signature to help figure this out.
|
2021-08-31 00:25:30 +03:00
|
|
|
|
|
|
|
|
|
10 | go u =
|
|
|
|
|
11 | t = A.fork '(go (u + 1))
|
|
|
|
|
12 | A.await t
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
```
|