A few words on destructured argument declarations

Sometimes one needs to express a function as a lambda expression, with an an ordered pair (p : α x β) as an argument. To use p, one will often have to destructure it: to analyze it as (a, b). With names for the two parts of (the term representing) the ordered pair, you can define such functions as fst (just return a), snd (just return b), and swap (return (b, a)).

Argument Not Analyzed

This function takes a pair; doesn't analyze it; and in this simple example, just returns, it. Polymorphic functions, capable of handling objects of any type, often handle object without ever inspecting them.

fun {α β} p => p : {α β : Type} → α × β → α × β
 fun {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} (
p: α × β
p : 
α: Type
α × 
β: Type
β) => 
p: α × β
p

Pair Analyzed As (a, b) By match Expression

If a function has to take as an argument a single product object, p, that's fine; you just destructure p explicitly using a match expression. Hare are examples using a lamdba expression for the ordered pair swap function, taking each (a,b) pair to (b,a).

fun {α β} p =>
  match p with
  | (a, b) => (b, a) : {α β : Type} → α × β → β × α
 λ {
α: Type
α 
β: Type
β : 
Type: Type 1
Type} 
         (
p: α × β
p : 
α: Type
α × 
β: Type
β)            -- pair object
         =>
        match 
p: α × β
p with            -- analyze p ...
        | (
a: α
a, 
b: β
b) =>             -- ... as (a, b)
          (
b: β
b, 
a: α
a)                -- return (b,a) 

-- Application of function. Expect ("Dolly", " Hello ")

("Dolly", " Hello ")

 (λ {
α: Type
α 
β: Type
β : 
Type: Type 1
Type}          -- function
         (
p: α × β
p : 
α: Type
α × 
β: Type
β) 
         =>
        match 
p: α × β
p with
        | (
a: α
a, 
b: β
b) => (
b: β
b, 
a: α
a)
      )                         -- end function
      (
" Hello ": String
" Hello ", 
"Dolly": String
"Dolly")      -- argument

Destructured Arguments

A great trick is to express a pair argument in already destructured form, (a,b). Here's the swap function written using this syntactic feature. Note that we have replaced p with (a, b). That's the trick.

fun {α β} x =>
  match x with
  | (a, b) => (b, a) : {α β : Type} → α × β → β × α
 fun 
        {
Warning: unused variable `α` [linter.unusedVariables]
 
Warning: unused variable `β` [linter.unusedVariables]
 : 
Type: Type 1
Type}          -- implicit type arguments
        ((
a: α
a, 
b: β
b) : α × β )     -- *destructured pair, (a, b)*
        => 
        (
b: β
b, 
a: α
a)                -- swap function is now trivial

-- And here's an example application

("Dolly", " Hello ")

 (λ {
Warning: unused variable `α` [linter.unusedVariables]
 
Warning: unused variable `β` [linter.unusedVariables]
 : 
Type: Type 1
Type}         -- Expect ("Dolly", " Hello ")
      (
a: α
a, 
b: β
b) 
      => 
      (
b: β
b, 
a: α
a))  
      (
" Hello ": String
" Hello ", 
"Dolly": String
"Dolly")

The TL;DR Takeaway

You can write function (lambda) expressions with ordered pairs objects as arguments, but *expressed in the their destructured form, (a, b). You can then write return values as functions of a and b.