2024-10-08 23:23:34 +03:00
|
|
|
``` ucm :hide
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> builtins.merge
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
|
|
|
# Basics
|
2023-07-19 20:45:05 +03:00
|
|
|
## non-exhaustive patterns
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : T -> ()
|
|
|
|
test = cases
|
2023-02-28 00:12:10 +03:00
|
|
|
A -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
test : (T, Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
(A, Some _) -> ()
|
|
|
|
(A, None) -> ()
|
|
|
|
(B, Some A) -> ()
|
|
|
|
(B, None) -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
## redundant patterns
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : T -> ()
|
|
|
|
test = cases
|
2023-02-28 00:12:10 +03:00
|
|
|
A -> ()
|
|
|
|
B -> ()
|
|
|
|
C -> ()
|
|
|
|
_ -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
test : (T, Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
(A, Some _) -> ()
|
|
|
|
(A, None) -> ()
|
|
|
|
(B, Some _) -> ()
|
|
|
|
(B, None) -> ()
|
|
|
|
(A, Some A) -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
# Uninhabited patterns
|
|
|
|
|
|
|
|
match is complete without covering uninhabited patterns
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type V =
|
|
|
|
|
|
|
|
test : Optional (Optional V) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
uninhabited patterns are reported as redundant
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type V =
|
|
|
|
|
2023-03-08 20:24:21 +03:00
|
|
|
test0 : V -> ()
|
|
|
|
test0 = cases
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-08 20:24:21 +03:00
|
|
|
unique type V =
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Optional (Optional V) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
Some _ -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
# Guards
|
|
|
|
|
|
|
|
## Incomplete patterns due to guards should be reported
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : () -> ()
|
|
|
|
test = cases
|
|
|
|
() | false -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Optional Nat -> Nat
|
|
|
|
test = cases
|
|
|
|
None -> 0
|
|
|
|
Some x
|
|
|
|
| isEven x -> x
|
|
|
|
```
|
|
|
|
|
|
|
|
## Complete patterns with guards should be accepted
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Optional Nat -> Nat
|
|
|
|
test = cases
|
|
|
|
None -> 0
|
|
|
|
Some x
|
|
|
|
| isEven x -> x
|
|
|
|
| otherwise -> 0
|
|
|
|
```
|
|
|
|
|
|
|
|
# Pattern instantiation depth
|
|
|
|
|
|
|
|
Uncovered patterns are only instantiated as deeply as necessary to
|
|
|
|
distinguish them from existing patterns.
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : Optional (Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : Optional (Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
Some (Some A) -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
# Literals
|
2023-03-02 18:04:36 +03:00
|
|
|
|
|
|
|
## Non-exhaustive
|
|
|
|
|
|
|
|
Nat
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Nat -> ()
|
|
|
|
test = cases
|
|
|
|
0 -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
## Exhaustive
|
|
|
|
|
|
|
|
Nat
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Nat -> ()
|
|
|
|
test = cases
|
|
|
|
0 -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
2023-03-02 18:04:36 +03:00
|
|
|
false -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
# Redundant
|
|
|
|
|
|
|
|
Nat
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Nat -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
test = cases
|
2023-03-02 18:04:36 +03:00
|
|
|
0 -> ()
|
|
|
|
0 -> ()
|
|
|
|
_ -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
|
|
|
false -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
# Sequences
|
2023-03-02 18:04:36 +03:00
|
|
|
|
|
|
|
## Exhaustive
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
x +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
## Non-exhaustive
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
x +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
xs :+ x -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
x0 +: (x1 +: xs) -> ()
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
x0 +: [] -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
## Uninhabited
|
|
|
|
|
|
|
|
`Cons` is not expected since `V` is uninhabited
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type V =
|
|
|
|
|
|
|
|
test : [V] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
|
|
|
## Length restrictions can equate cons and nil patterns
|
|
|
|
|
|
|
|
Here the first pattern matches lists of length two or greater, the
|
|
|
|
second pattern matches lists of length 0. The third case matches when the
|
|
|
|
final element is `false`, while the fourth pattern matches when the
|
|
|
|
first element is `true`. However, the only possible list length at
|
|
|
|
the third or fourth clause is 1, so the first and final element must
|
|
|
|
be equal. Thus, the pattern match is exhaustive.
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b] ++ xs -> ()
|
|
|
|
[] -> ()
|
|
|
|
xs :+ false -> ()
|
|
|
|
true +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
This is the same idea as above but shows that fourth match is redundant.
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b] ++ xs -> ()
|
|
|
|
[] -> ()
|
|
|
|
xs :+ true -> ()
|
|
|
|
true +: xs -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
This is another similar example. The first pattern matches lists of
|
|
|
|
length 5 or greater. The second matches lists of length 4 or greater where the
|
|
|
|
first and third element are true. The third matches lists of length 4
|
2023-07-19 20:45:05 +03:00
|
|
|
or greater where the final 4 elements are `true, false, true, false`.
|
2023-03-02 18:04:36 +03:00
|
|
|
The list must be exactly of length 4 to arrive at the second or third
|
|
|
|
clause, so the third pattern is redundant.
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b, c, d, f] ++ xs -> ()
|
|
|
|
[true, _, true, _] ++ _ -> ()
|
|
|
|
_ ++ [true, false, true, false] -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
2023-03-08 18:53:46 +03:00
|
|
|
|
|
|
|
# bugfix: Sufficient data decl map
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-08 18:53:46 +03:00
|
|
|
unique type T = A
|
|
|
|
|
|
|
|
unit2t : Unit -> T
|
|
|
|
unit2t = cases
|
|
|
|
() -> A
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-08 18:53:46 +03:00
|
|
|
```
|
|
|
|
|
2023-07-19 20:45:05 +03:00
|
|
|
Pattern coverage checking needs the data decl map to contain all
|
|
|
|
transitive type dependencies of the scrutinee type. We do this
|
2023-03-08 18:53:46 +03:00
|
|
|
before typechecking begins in a roundabout way: fetching all
|
|
|
|
transitive type dependencies of references that appear in the expression.
|
|
|
|
|
|
|
|
This test ensures that we have fetched the `T` type although there is
|
|
|
|
no data decl reference to `T` in `witht`.
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-08 18:53:46 +03:00
|
|
|
witht : Unit
|
|
|
|
witht = match unit2t () with
|
|
|
|
x -> ()
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-08 18:53:46 +03:00
|
|
|
unique type V =
|
|
|
|
|
|
|
|
evil : Unit -> V
|
|
|
|
evil = bug ""
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-08 18:53:46 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-03-08 18:53:46 +03:00
|
|
|
withV : Unit
|
|
|
|
withV = match evil () with
|
|
|
|
x -> ()
|
|
|
|
```
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-13 21:11:39 +03:00
|
|
|
unique type SomeType = A
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-13 21:11:39 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-13 21:11:39 +03:00
|
|
|
unique type R = R SomeType
|
|
|
|
|
|
|
|
get x = match x with
|
|
|
|
R y -> y
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-03-13 21:11:39 +03:00
|
|
|
unique type R = { someType : SomeType }
|
|
|
|
```
|
2023-04-13 22:17:39 +03:00
|
|
|
|
|
|
|
# Ability handlers
|
|
|
|
|
|
|
|
## Exhaustive ability handlers are accepted
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
result : '{e, Abort} T -> {e} ()
|
|
|
|
result f = handle !f with cases
|
2024-08-26 20:37:19 +03:00
|
|
|
{ T.A } -> ()
|
2023-04-13 22:17:39 +03:00
|
|
|
{ B } -> ()
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
result : '{e, Abort} V -> {e} V
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 23:50:14 +03:00
|
|
|
impl : Request {Abort} V -> V
|
|
|
|
impl = cases
|
2023-04-13 22:17:39 +03:00
|
|
|
{ abort -> _ } -> bug "aborted"
|
2023-04-14 23:50:14 +03:00
|
|
|
handle !f with impl
|
2023-04-13 22:17:39 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Stream a where
|
|
|
|
emit : a -> {Stream a} Unit
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
handleMulti c =
|
|
|
|
impl xs = cases
|
|
|
|
{ r } -> (Some r, xs)
|
|
|
|
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
|
|
|
|
{ abort -> _ } -> (None, xs)
|
|
|
|
handle !c with impl []
|
|
|
|
```
|
2023-04-14 23:50:14 +03:00
|
|
|
|
|
|
|
## Non-exhaustive ability handlers are rejected
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-04-14 23:50:14 +03:00
|
|
|
abortWithMessage : Text -> {Abort} a
|
2023-04-13 22:17:39 +03:00
|
|
|
|
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
result : '{e, Abort} a -> {e} a
|
2023-04-13 22:17:39 +03:00
|
|
|
result f = handle !f with cases
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 21:59:31 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
unique type T = A | B
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
result : '{e, Abort} T -> {e} ()
|
2023-04-13 22:17:39 +03:00
|
|
|
result f = handle !f with cases
|
2024-08-26 20:37:19 +03:00
|
|
|
{ T.A } -> ()
|
2023-04-14 21:59:31 +03:00
|
|
|
{ abort -> _ } -> bug "aborted"
|
2023-04-13 22:17:39 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 04:27:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
|
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
result : '{e, Give T} r -> {e} r
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
2024-08-28 02:29:29 +03:00
|
|
|
{ give T.A -> resume } -> result resume
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Stream a where
|
|
|
|
emit : a -> {Stream a} Unit
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
handleMulti c =
|
|
|
|
impl : [a] -> Request {Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
impl xs = cases
|
|
|
|
{ r } -> (Some r, xs)
|
|
|
|
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
|
|
|
|
handle !c with impl []
|
|
|
|
```
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
## Redundant handler cases are rejected
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 04:27:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
unique type T = A | B
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
result : '{e, Give T} r -> {e} r
|
2023-04-14 04:27:31 +03:00
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> result resume
|
2024-08-29 21:12:25 +03:00
|
|
|
{ give T.A -> resume } -> result resume
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
## Exhaustive ability reinterpretations are accepted
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
abortWithMessage : Text -> {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e, Abort} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> abort
|
|
|
|
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
structural ability Abort a where
|
|
|
|
abort : {Abort a} r
|
|
|
|
abortWithMessage : a -> {Abort a} r
|
|
|
|
|
|
|
|
result : '{e, Abort V} a -> {e, Abort V} a
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Abort V} r -> {Abort V} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> abort
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
## Non-exhaustive ability reinterpretations are rejected
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
abortWithMessage : Text -> {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e, Abort} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
|
|
|
|
```
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
## Hacky workaround for uninhabited abilities
|
|
|
|
|
|
|
|
Although all of the constructors of an ability might be uninhabited,
|
|
|
|
the typechecker requires at least one be specified so that it can
|
|
|
|
determine that the ability should be discharged. So, the default
|
|
|
|
pattern match coverage checking behavior of prohibiting covering any
|
|
|
|
of the cases is problematic. Instead, the pattern match coverage
|
|
|
|
checker will require that at least one constructor be given, even if
|
|
|
|
they are all uninhabited.
|
|
|
|
|
|
|
|
The messages here aren't the best, but I don't think uninhabited
|
|
|
|
abilities will come up and get handlers written for them often.
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give2 _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> bug "impossible"
|
|
|
|
{ give2 _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison :error
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability GiveA a where
|
|
|
|
giveA : a -> {GiveA a} Unit
|
|
|
|
giveA2 : a -> {GiveA a} Unit
|
|
|
|
|
|
|
|
unique ability GiveB a where
|
|
|
|
giveB : a -> {GiveB a} Unit
|
|
|
|
giveB2 : a -> {GiveB a} Unit
|
|
|
|
|
|
|
|
result : '{e, GiveA V, GiveB V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {GiveA V, GiveB V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ giveA _ -> _ } -> bug "impossible"
|
|
|
|
{ giveA2 _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB2 _ -> _ } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-10-08 23:23:34 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability GiveA a where
|
|
|
|
giveA : a -> {GiveA a} Unit
|
|
|
|
giveA2 : a -> {GiveA a} Unit
|
|
|
|
|
|
|
|
unique ability GiveB a where
|
|
|
|
giveB : a -> {GiveB a} Unit
|
|
|
|
giveB2 : a -> {GiveB a} Unit
|
|
|
|
|
|
|
|
result : '{e, GiveA V, GiveB V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {GiveA V, GiveB V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ giveA2 _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB _ -> _ } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|