2020-09-28 20:09:55 +03:00
# Destructuring binds
Here's a couple examples:
2024-07-10 17:46:18 +03:00
``` unison
2020-10-01 01:03:54 +03:00
ex0 : Nat -> Nat
ex0 n =
(a, _, (c,d)) = ("uno", "dos", (n, 7))
c + d
2020-09-28 20:09:55 +03:00
ex1 : (a,b,(Nat,Nat)) -> Nat
ex1 tup =
(a, b, (c,d)) = tup
c + d
```
2024-07-10 19:17:15 +03:00
``` ucm
2020-09-28 20:09:55 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2020-09-28 20:09:55 +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` :
2020-10-01 01:03:54 +03:00
ex0 : Nat -> Nat
2020-09-28 20:09:55 +03:00
ex1 : (a, b, (Nat, Nat)) -> Nat
```
2024-07-10 19:17:15 +03:00
``` ucm
2024-06-12 01:22:09 +03:00
scratch/main> add
2020-09-28 20:09:55 +03:00
⍟ I've added these definitions:
2020-10-01 01:03:54 +03:00
ex0 : Nat -> Nat
2020-09-28 20:09:55 +03:00
ex1 : (a, b, (Nat, Nat)) -> Nat
2024-06-12 01:22:09 +03:00
scratch/main> view ex0 ex1
2020-10-01 00:16:47 +03:00
2020-10-01 01:03:54 +03:00
ex0 : Nat -> Nat
ex0 n =
use Nat +
(a, _, (c, d)) = ("uno", "dos", (n, 7))
c + d
2020-10-01 00:16:47 +03:00
ex1 : (a, b, (Nat, Nat)) -> Nat
2023-07-21 09:12:22 +03:00
ex1 = cases (a, b, (c, d)) -> c Nat.+ d
2020-10-01 00:16:47 +03:00
2020-09-28 20:09:55 +03:00
```
2020-10-01 01:03:54 +03:00
Notice that `ex0` is printed using the `cases` syntax (but `ex1` is not). The pretty-printer currently prefers the `cases` syntax if definition can be printed using either destructuring bind or `cases` .
2020-09-28 20:09:55 +03:00
A destructuring bind is just syntax for a single branch pattern match. Notice that Unison detects this function as an alias of `ex1` :
2024-07-10 17:46:18 +03:00
``` unison
2020-09-28 20:09:55 +03:00
ex2 : (a,b,(Nat,Nat)) -> Nat
ex2 tup = match tup with
(a, b, (c,d)) -> c + d
```
2024-07-10 19:17:15 +03:00
``` ucm
2020-09-28 20:09:55 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2020-09-28 20:09:55 +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` :
ex2 : (a, b, (Nat, Nat)) -> Nat
(also named ex1)
```
## Corner cases
Destructuring binds can't be recursive: the left-hand side bound variables aren't available on the right hand side. For instance, this doesn't typecheck:
2024-07-10 17:46:18 +03:00
``` unison
2020-09-28 20:09:55 +03:00
ex4 =
(a,b) = (a Nat.+ b, 19)
"Doesn't typecheck"
```
2024-07-10 19:17:15 +03:00
``` ucm
2020-09-28 20:09:55 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2024-01-25 18:12:10 +03:00
I couldn't figure out what a refers to here:
2020-09-28 20:09:55 +03:00
2 | (a,b) = (a Nat.+ b, 19)
2024-01-26 20:53:29 +03:00
I think its type should be:
Nat
2022-07-13 05:08:33 +03:00
Some common causes of this error include:
2022-07-13 18:20:12 +03:00
* Your current namespace is too deep to contain the
2022-07-13 05:08:33 +03:00
definition in its subtree
* The definition is part of a library which hasn't been
added to this project
2024-01-25 18:12:10 +03:00
* You have a typo in the name
2020-09-28 20:09:55 +03:00
```
2020-10-01 01:03:54 +03:00
Even though the parser accepts any pattern on the LHS of a bind, it looks pretty weird to see things like `12 = x` , so we avoid showing a destructuring bind when the LHS is a "literal" pattern (like `42` or "hi"). Again these examples wouldn't compile with coverage checking.
2020-09-28 20:09:55 +03:00
2024-07-10 17:46:18 +03:00
``` unison
2020-10-01 01:03:54 +03:00
ex5 : 'Text
ex5 _ = match 99 + 1 with
2020-09-28 20:09:55 +03:00
12 -> "Hi"
2023-01-13 18:18:20 +03:00
_ -> "Bye"
2020-10-01 01:03:54 +03:00
ex5a : 'Text
ex5a _ = match (99 + 1, "hi") with
(x, "hi") -> "Not printed as a destructuring bind."
2023-01-13 18:18:20 +03:00
_ -> "impossible"
2020-09-28 20:09:55 +03:00
```
2024-07-10 19:17:15 +03:00
``` ucm
2020-10-01 01:03:54 +03:00
2023-12-22 14:55:24 +03:00
Loading changes detected in scratch.u.
2020-10-01 01:03:54 +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` :
ex5 : 'Text
ex5a : 'Text
```
2024-07-10 19:17:15 +03:00
``` ucm
2024-06-12 01:22:09 +03:00
scratch/main> add
2020-09-28 20:09:55 +03:00
⍟ I've added these definitions:
2020-10-01 01:03:54 +03:00
ex5 : 'Text
ex5a : 'Text
2020-09-28 20:09:55 +03:00
2024-06-12 01:22:09 +03:00
scratch/main> view ex5 ex5a
2020-09-28 20:09:55 +03:00
2020-10-01 01:03:54 +03:00
ex5 : 'Text
2023-07-21 09:12:22 +03:00
ex5 _ = match 99 Nat.+ 1 with
12 -> "Hi"
_ -> "Bye"
2020-10-01 01:03:54 +03:00
ex5a : 'Text
2023-07-21 09:12:22 +03:00
ex5a _ = match (99 Nat.+ 1, "hi") with
(x, "hi") -> "Not printed as a destructuring bind."
_ -> "impossible"
2020-09-28 20:09:55 +03:00
```
2020-10-01 01:03:54 +03:00
Notice how it prints both an ordinary match.
2020-09-28 20:09:55 +03:00
Also, for clarity, the pretty-printer shows a single-branch match if the match shadows free variables of the scrutinee, for example:
2024-07-10 17:46:18 +03:00
``` unison
2020-09-28 20:09:55 +03:00
ex6 x = match x with
(x, y) -> x Nat.+ y
```
For clarity, the pretty-printer leaves this alone, even though in theory it could be written `(x,y) = x; x + y` :
2024-07-10 19:17:15 +03:00
``` ucm
2024-06-12 01:22:09 +03:00
scratch/main> add
2020-09-28 20:09:55 +03:00
⍟ I've added these definitions:
ex6 : (Nat, Nat) -> Nat
2024-06-12 01:22:09 +03:00
scratch/main> view ex6
2020-09-28 20:09:55 +03:00
ex6 : (Nat, Nat) -> Nat
2023-07-21 09:12:22 +03:00
ex6 = cases (x, y) -> x Nat.+ y
2020-09-28 20:09:55 +03:00
```