unison/unison-src/transcripts/destructuring-binds.md

Destructuring binds

scratch/main> builtins.merge

Here's a couple examples:

ex0 : Nat -> Nat
ex0 n =
  (a, _, (c,d)) = ("uno", "dos", (n, 7))
  c + d

ex1 : (a,b,(Nat,Nat)) -> Nat
ex1 tup =
  (a, b, (c,d)) = tup
  c + d

scratch/main> add
scratch/main> view ex0 ex1

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.

A destructuring bind is just syntax for a single branch pattern match. Notice that Unison detects this function as an alias of ex1:

ex2 : (a,b,(Nat,Nat)) -> Nat
ex2 tup = match tup with
  (a, b, (c,d)) -> c + d

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:

ex4 =
  (a,b) = (a Nat.+ b, 19)
  "Doesn't typecheck"

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.

ex5 : 'Text
ex5 _ = match 99 + 1 with
  12 -> "Hi"
  _ -> "Bye"

ex5a : 'Text
ex5a _ = match (99 + 1, "hi") with
  (x, "hi") -> "Not printed as a destructuring bind."
  _ -> "impossible"

scratch/main> add
scratch/main> view ex5 ex5a

Notice how it prints both an ordinary match.

Also, for clarity, the pretty-printer shows a single-branch match if the match shadows free variables of the scrutinee, for example:

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:

scratch/main> add
scratch/main> view ex6