# Local Definitions: let and where¶

There are two ways of declaring local definitions in Agda:

• let-expressions
• where-blocks

## let-expressions¶

A let-expression defines an abbreviation. In other words, the expression that we define in a let-expression can neither be recursive, nor can let bound functions be defined by pattern matching.

Example:

f : Nat
f = let h : Nat  Nat
h m = suc (suc m)
in  h zero + h (suc zero)

let-expressions have the general form

let f₁ : A₁₁  A₁ₙ  A₁
f₁ x₁ … xₙ = e₁
…
fₘ : Aₘ₁  Aₘₖ  Aₘ
fₘ x₁ … xₖ = eₘ
in  e’

where previous definitions are in scope in later definitions. The type signatures can be left out if Agda can infer them. After type-checking, the meaning of this is simply the substitution e’[f₁ := λ x₁ xₙ e; …; fₘ := λ x₁ xₖ eₘ]. Since Agda substitutes away let-bindings, they do not show up in terms Agda prints, nor in the goal display in interactive mode.

### Let binding record patterns¶

For a record

record R : Set where
constructor c
field
f : X
g : Y
h : Z

a let expression of the form

let (c x  y z) = t
in  u

will be translated internally to as

let x = f t
y = g t
z = h t
in  u

This is not allowed if R is declared coinductive.

## where-blocks¶

where-blocks are much more powerful than let-expressions, as they support arbitrary local definitions. A where can be attached to any function clause.

where-blocks have the general form

clause
where
decls

or

clause
module M where
decls

A simple instance is

g ps = e
where
f : A₁  Aₙ  A
f p₁₁ … p₁ₙ= e₁
…
…
f pₘ₁ … pₘₙ= eₘ

Here, the pᵢⱼ are patterns of the corresponding types and eᵢ is an expression that can contain occurrences of f. Functions defined with a where-expression must follow the rules for general definitions by pattern matching.

Example:

reverse : {A : Set}  List A  List A
reverse {A} xs = rev-append xs []
where
rev-append : List A  List A  List A
rev-append [] ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)

### Variable scope¶

The pattern variables of the parent clause of the where-block are in scope; in the previous example, these are A and xs. The variables bound by the type signature of the parent clause are not in scope. This is why we added the hidden binder {A}.

### Scope of the local declarations¶

The where-definitions are not visible outside of the clause that owns these definitions (the parent clause). If the where-block is given a name (form module M where), then the definitions are available as qualified by M, since module M is visible even outside of the parent clause. The special form of an anonymous module (module _ where) makes the definitions visible outside of the parent clause without qualification.

If the parent function of a named where-block (form module M where) is private, then module M is also private. However, the declarations inside M are not private unless declared so explicitly. Thus, the following example scope checks fine:

module Parent₁ where
private
parent = local
module Private where
local = Set
module Public = Private

test₁ = Parent₁.Public.local

Likewise, a private declaration for a parent function does not affect the privacy of local functions defined under a module _ where-block:

module Parent₂ where
private
parent = local
module _ where
local = Set

test₂ = Parent₂.local

They can be declared private explicitly, though:

module Parent₃ where
parent = local
module _ where
private
local = Set

Now, Parent₃.local is not in scope.

A private declaration for the parent of an ordinary where-block has no effect on the local definitions, of course. They are not even in scope.

## Proving properties¶

Sometimes one needs to refer to local definitions in proofs about the parent function. In this case, the module where variant is preferable.

reverse : {A : Set}  List A  List A
reverse {A} xs = rev-append xs []
module Rev where
rev-append : List A  List A  List A
rev-append [] ys = ys
rev-append (x :: xs) ys = rev-append xs (x :: ys)

This gives us access to the local function as

Rev.rev-append : {A : Set} (xs : List A)  List A  List A  List A

Alternatively, we can define local functions as private to the module we are working in; hence, they will not be visible in any module that imports this module but it will allow us to prove some properties about them.

private
rev-append : {A : Set}  List A  List A  List A
rev-append []        ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)

reverse' : {A : Set}  List A  List A
reverse' xs = rev-append xs []

## More Examples (for Beginners)¶

Using a let-expression:

tw-map : {A : Set}  List A  List (List A)
tw-map {A} xs = let twice : List A  List A
twice xs = xs ++ xs
in  map (\ x  twice [ x ]) xs

Same definition but with less type information:

tw-map' : {A : Set}  List A  List (List A)
tw-map' {A} xs = let twice : _
twice xs = xs ++ xs
in  map (\ x  twice [ x ]) xs

Same definition but with a where-expression

tw-map'' : {A : Set}  List A  List (List A)
tw-map'' {A} xs =  map (\ x  twice [ x ]) xs
where twice : List A  List A
twice xs = xs ++ xs

Even less type information using let:

g : Nat  List Nat
g zero    = [ zero ]
g (suc n) = let sing = [ suc n ]
in  sing ++ g n

Same definition using where:

g' : Nat  List Nat
g' zero = [ zero ]
g' (suc n) = sing ++ g' n
where  sing = [ suc n ]

More than one definition in a let:

h : Nat  Nat
h n = let add2 : Nat
add2 = suc (suc n)

twice : Nat  Nat
twice m = m * m

in twice add2

More than one definition in a where:

fibfact : Nat  Nat
fibfact n = fib n + fact n
where fib : Nat  Nat
fib zero = suc zero
fib (suc zero) = suc zero
fib (suc (suc n)) = fib (suc n) + fib n

fact : Nat  Nat
fact zero = suc zero
fact (suc n) = suc n * fact n

Combining let and where:

k : Nat  Nat
k n = let aux : Nat  Nat
aux m = pred (h m) + fibfact m
in aux (pred n)
where pred : Nat  Nat
pred zero = zero
pred (suc m) = m