2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability X t where
|
2020-11-26 05:12:09 +03:00
|
|
|
x : t -> a -> a
|
|
|
|
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability Abort where
|
2020-11-26 05:12:09 +03:00
|
|
|
abort : a
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2020-11-26 05:12:09 +03:00
|
|
|
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`:
|
|
|
|
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability Abort
|
|
|
|
structural ability X t
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability Abort
|
|
|
|
structural ability X t
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
This code should not type check. The match on X.x ought to introduce a
|
|
|
|
skolem variable `a` such that `c : a` and the continuation has type
|
|
|
|
`a ->{X} b`. Thus, `handle c with h : Optional a`, which is not the
|
|
|
|
correct result type.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2020-11-26 05:12:09 +03:00
|
|
|
h0 : Request {X t} b -> Optional b
|
|
|
|
h0 req = match req with
|
|
|
|
{ X.x _ c -> _ } -> handle c with h0
|
|
|
|
{ d } -> Some d
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2024-03-08 23:18:35 +03:00
|
|
|
Each case of a match / with expression need to have the same
|
|
|
|
type.
|
|
|
|
|
|
|
|
Here, one is: Optional b
|
|
|
|
and another is: Optional a
|
|
|
|
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2022-12-03 01:08:40 +03:00
|
|
|
3 | { X.x _ c -> _ } -> handle c with h0
|
|
|
|
|
2024-03-08 23:18:35 +03:00
|
|
|
from these spots, respectively:
|
2022-12-03 01:08:40 +03:00
|
|
|
|
|
|
|
1 | h0 : Request {X t} b -> Optional b
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
This code should not check because `t` does not match `b`.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2020-11-26 05:12:09 +03:00
|
|
|
h1 : Request {X t} b -> Optional b
|
|
|
|
h1 req = match req with
|
|
|
|
{ X.x t _ -> _ } -> handle t with h1
|
|
|
|
{ d } -> Some d
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2020-11-26 05:12:09 +03:00
|
|
|
Each case of a match / with expression need to have the same
|
2021-04-08 08:24:00 +03:00
|
|
|
type.
|
|
|
|
|
2024-03-08 23:18:35 +03:00
|
|
|
Here, one is: Optional b
|
|
|
|
and another is: Optional t
|
2021-04-08 08:24:00 +03:00
|
|
|
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
3 | { X.x t _ -> _ } -> handle t with h1
|
|
|
|
|
2024-03-08 23:18:35 +03:00
|
|
|
from these spots, respectively:
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
1 | h1 : Request {X t} b -> Optional b
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
This code should not check for reasons similar to the first example,
|
|
|
|
but with the continuation rather than a parameter.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2020-11-26 05:12:09 +03:00
|
|
|
h2 : Request {Abort} r -> r
|
|
|
|
h2 req = match req with
|
|
|
|
{ Abort.abort -> k } -> handle k 5 with h2
|
|
|
|
{ r } -> r
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2021-04-08 08:24:00 +03:00
|
|
|
The 1st argument to `k`
|
2021-04-01 04:44:01 +03:00
|
|
|
|
2021-04-08 08:24:00 +03:00
|
|
|
has type: Nat
|
|
|
|
but I expected: a
|
2020-11-26 05:12:09 +03:00
|
|
|
|
|
|
|
3 | { Abort.abort -> k } -> handle k 5 with h2
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
This should work fine.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2020-11-26 05:12:09 +03:00
|
|
|
h3 : Request {X b, Abort} b -> Optional b
|
|
|
|
h3 = cases
|
|
|
|
{ r } -> Some r
|
|
|
|
{ Abort.abort -> _ } -> None
|
|
|
|
{ X.x b _ -> _ } -> Some b
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2020-11-26 05:12:09 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2020-11-26 05:12:09 +03:00
|
|
|
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`:
|
|
|
|
|
|
|
|
h3 : Request {X b, Abort} b -> Optional b
|
|
|
|
|
|
|
|
```
|